mod_cases tactic

The mod_cases tactic does case disjunction on e % n, where e : ℤ or e : ℕ, to yield n new subgoals corresponding to the possible values of e modulo n.

def Mathlib.Tactic.ModCases.IntMod.OnModCases (n : ℕ) (a : ℤ) (lb : ℕ) (p : Sort u_1) : Sort (imax 1 u_1)

OnModCases n a lb p represents a partial proof by cases that there exists 0 ≤ z < n such that a ≡ z (mod n). It asserts that if ∃ z, lb ≤ z < n ∧ a ≡ z (mod n) holds, then p (where p is the current goal).

Equations

• Mathlib.Tactic.ModCases.IntMod.OnModCases n a lb p = ((z : ℕ) → lb ≤ z ∧ z < n ∧ a ≡ ↑z [ZMOD ↑n] → p)

@[inline]

def Mathlib.Tactic.ModCases.IntMod.onModCases_start (p : Sort u_1) (a : ℤ) (n : ℕ) (hn : Nat.ble 1 n = true) (H : Mathlib.Tactic.ModCases.IntMod.OnModCases n a 0 p) : p

The first theorem we apply says that ∃ z, 0 ≤ z < n ∧ a ≡ z (mod n). The actual mathematical content of the proof is here.

Equations

• Mathlib.Tactic.ModCases.IntMod.onModCases_start p a n hn H = H (Int.toNat (a % ↑n)) ⋯

@[inline]

def Mathlib.Tactic.ModCases.IntMod.onModCases_stop (p : Sort u_1) (n : ℕ) (a : ℤ) : Mathlib.Tactic.ModCases.IntMod.OnModCases n a n p

The end point is that once we have reduced to ∃ z, n ≤ z < n ∧ a ≡ z (mod n) there are no more cases to consider.

Equations

• Mathlib.Tactic.ModCases.IntMod.onModCases_stop p n a x h = ⋯.elim

@[inline]

def Mathlib.Tactic.ModCases.IntMod.onModCases_succ {p : Sort u_1} {n : ℕ} {a : ℤ} (b : ℕ) (h : a ≡ OfNat.ofNat b [ZMOD OfNat.ofNat n] → p) (H : Mathlib.Tactic.ModCases.IntMod.OnModCases n a (Nat.add b 1) p) : Mathlib.Tactic.ModCases.IntMod.OnModCases n a b p

The successor case decomposes ∃ z, b ≤ z < n ∧ a ≡ z (mod n) into a ≡ b (mod n) ∨ ∃ z, b+1 ≤ z < n ∧ a ≡ z (mod n), and the a ≡ b (mod n) → p case becomes a subgoal.

Equations

• Mathlib.Tactic.ModCases.IntMod.onModCases_succ b h H z x = match x with | ⋯ => if e : b = z then h ⋯ else H z ⋯

partial def Mathlib.Tactic.ModCases.IntMod.proveOnModCases {u : Lean.Level} (n : Q(ℕ)) (a : Q(ℤ)) (b : Q(ℕ)) (p : Q(Sort u)) : Lean.MetaM (Q(Mathlib.Tactic.ModCases.IntMod.OnModCases «$n» «$a» «$b» «$p») × List Lean.MVarId)

Proves an expression of the form OnModCases n a b p where n and b are raw nat literals and b ≤ n. Returns the list of subgoals ?gi : a ≡ i [ZMOD n] → p.

def Mathlib.Tactic.ModCases.IntMod.modCases (h : Lean.TSyntax `Lean.binderIdent) (e : Q(ℤ)) (n : ℕ) : Lean.Elab.Tactic.TacticM Unit

Int case of mod_cases h : e % n.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.ModCases.NatMod.OnModCases (n : ℕ) (a : ℕ) (lb : ℕ) (p : Sort u_1) : Sort (imax 1 u_1)

OnModCases n a lb p represents a partial proof by cases that there exists 0 ≤ m < n such that a ≡ m (mod n). It asserts that if ∃ m, lb ≤ m < n ∧ a ≡ m (mod n) holds, then p (where p is the current goal).

Equations

• Mathlib.Tactic.ModCases.NatMod.OnModCases n a lb p = ((m : ℕ) → lb ≤ m ∧ m < n ∧ a ≡ m [MOD n] → p)

@[inline]

def Mathlib.Tactic.ModCases.NatMod.onModCases_start (p : Sort u_1) (a : ℕ) (n : ℕ) (hn : Nat.ble 1 n = true) (H : Mathlib.Tactic.ModCases.NatMod.OnModCases n a 0 p) : p

The first theorem we apply says that ∃ m, 0 ≤ m < n ∧ a ≡ m (mod n). The actual mathematical content of the proof is here.

Equations

• Mathlib.Tactic.ModCases.NatMod.onModCases_start p a n hn H = H (a % n) ⋯

@[inline]

def Mathlib.Tactic.ModCases.NatMod.onModCases_stop (p : Sort u_1) (n : ℕ) (a : ℕ) : Mathlib.Tactic.ModCases.NatMod.OnModCases n a n p

The end point is that once we have reduced to ∃ m, n ≤ m < n ∧ a ≡ m (mod n) there are no more cases to consider.

Equations

• Mathlib.Tactic.ModCases.NatMod.onModCases_stop p n a x h = ⋯.elim

@[inline]

def Mathlib.Tactic.ModCases.NatMod.onModCases_succ {p : Sort u_1} {n : ℕ} {a : ℕ} (b : ℕ) (h : a ≡ b [MOD n] → p) (H : Mathlib.Tactic.ModCases.NatMod.OnModCases n a (Nat.add b 1) p) : Mathlib.Tactic.ModCases.NatMod.OnModCases n a b p

The successor case decomposes ∃ m, b ≤ m < n ∧ a ≡ m (mod n) into a ≡ b (mod n) ∨ ∃ m, b+1 ≤ m < n ∧ a ≡ m (mod n), and the a ≡ b (mod n) → p case becomes a subgoal.

Equations

• Mathlib.Tactic.ModCases.NatMod.onModCases_succ b h H z x = match x with | ⋯ => if e : b = z then h ⋯ else H z ⋯

partial def Mathlib.Tactic.ModCases.NatMod.proveOnModCases {u : Lean.Level} (n : Q(ℕ)) (a : Q(ℕ)) (b : Q(ℕ)) (p : Q(Sort u)) : Lean.MetaM (Q(Mathlib.Tactic.ModCases.NatMod.OnModCases «$n» «$a» «$b» «$p») × List Lean.MVarId)

Proves an expression of the form OnModCases n a b p where n and b are raw nat literals and b ≤ n. Returns the list of subgoals ?gi : a ≡ i [MOD n] → p.

def Mathlib.Tactic.ModCases.NatMod.modCases (h : Lean.TSyntax `Lean.binderIdent) (e : Q(ℕ)) (n : ℕ) : Lean.Elab.Tactic.TacticM Unit

Nat case of mod_cases h : e % n.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.ModCases.«tacticMod_cases_:_%_» : Lean.ParserDescr

• The tactic mod_cases h : e % 3 will perform a case disjunction on e. If e : ℤ, then it will yield subgoals containing the assumptions h : e ≡ 0 [ZMOD 3], h : e ≡ 1 [ZMOD 3], h : e ≡ 2 [ZMOD 3] respectively. If e : ℕ instead, then it works similarly, except with [MOD 3] instead of [ZMOD 3].
• In general, mod_cases h : e % n works when n is a positive numeral and e is an expression of type ℕ or ℤ.
• If h is omitted as in mod_cases e % n, it will be default-named H.

Equations

• One or more equations did not get rendered due to their size.