Theorem: Poland1998P4.lemma3 (Compfiles/Poland1998P4.lean)

State before:
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
⊢ ∃ i < 7, a' (N0 + i) = 0
Tactic:
have hp : Fact (Nat.Prime 7) := ⟨by norm_num⟩
State after:
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
⊢ ∃ i < 7, a' (N0 + i) = 0

State before:
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
⊢ ∃ i < 7, a' (N0 + i) = 0
Tactic:
let ii := - (a' N0) / k
State after:
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
⊢ ∃ i < 7, a' (N0 + i) = 0

State before:
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
⊢ ∃ i < 7, a' (N0 + i) = 0
Tactic:
use ii.val
State after:
case h
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
⊢ ii.val < 7 ∧ a' (N0 + ii.val) = 0

State before:
case h
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
⊢ ii.val < 7 ∧ a' (N0 + ii.val) = 0
Tactic:
constructor
State after:
case h.left
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
⊢ ii.val < 7

case h.right
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
⊢ a' (N0 + ii.val) = 0

State before:
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
⊢ Nat.Prime 7
Tactic:
norm_num
State after:
no goals

State before:
case h.left
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
⊢ ii.val < 7
Tactic:
exact ZMod.val_lt ii
State after:
no goals

State before:
case h.right
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
⊢ a' (N0 + ii.val) = 0
Tactic:
have := hN ii.val (ZMod.val_lt ii)
State after:
case h.right
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
this : a' (N0 + ii.val) = a' N0 + k * ↑ii.val
⊢ a' (N0 + ii.val) = 0

State before:
case h.right
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
this : a' (N0 + ii.val) = a' N0 + k * ↑ii.val
⊢ a' (N0 + ii.val) = 0
Tactic:
rw [this, ZMod.natCast_val, ZMod.cast_id', id_def, mul_div_cancel₀ _ hk]
State after:
case h.right
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
this : a' (N0 + ii.val) = a' N0 + k * ↑ii.val
⊢ a' N0 + -a' N0 = 0

State before:
case h.right
N0 : ℕ
k : ZMod 7
hk : k ≠ 0
hN : ∀ i < 7, a' (N0 + i) = a' N0 + k * ↑i
hp : Fact (Nat.Prime 7)
ii : ZMod 7 := -a' N0 / k
this : a' (N0 + ii.val) = a' N0 + k * ↑ii.val
⊢ a' N0 + -a' N0 = 0
Tactic:
exact add_neg_self (a' N0)
State after:
no goals