Theorem: HTPI.cc_nat_zero_iff_dvd (HTPILib/Chap7.lean)

State before:
m k : ℕ
⊢ [↑k]_0 = [0]_0 ↔ 0 ∣ k
Tactic:
have h : (0 : Int) = (↑(0 : Nat) : Int) := by rfl
State after:
m k : ℕ
h : 0 = ↑0
⊢ [↑k]_0 = [0]_0 ↔ 0 ∣ k

State before:
m k : ℕ
h : 0 = ↑0
⊢ [↑k]_0 = [0]_0 ↔ 0 ∣ k
Tactic:
rewrite [cc_mod_0, cc_mod_0, h, Nat.cast_inj]
State after:
m k : ℕ
h : 0 = ↑0
⊢ k = 0 ↔ 0 ∣ k

State before:
m k : ℕ
h : 0 = ↑0
⊢ k = 0 ↔ 0 ∣ k
Tactic:
apply Iff.intro
State after:
case mp
m k : ℕ
h : 0 = ↑0
⊢ k = 0 → 0 ∣ k

case mpr
m k : ℕ
h : 0 = ↑0
⊢ 0 ∣ k → k = 0

State before:
m k : ℕ
⊢ 0 = ↑0
Tactic:
rfl
State after:
no goals

State before:
case mp
m k : ℕ
h : 0 = ↑0
⊢ k = 0 → 0 ∣ k
Tactic:
assume h1 : k = 0
State after:
case mp
m k : ℕ
h : 0 = ↑0
h1 : k = 0
⊢ 0 ∣ k

State before:
case mp
m k : ℕ
h : 0 = ↑0
h1 : k = 0
⊢ 0 ∣ k
Tactic:
rewrite [h1]
State after:
case mp
m k : ℕ
h : 0 = ↑0
h1 : k = 0
⊢ 0 ∣ 0

State before:
case mp
m k : ℕ
h : 0 = ↑0
h1 : k = 0
⊢ 0 ∣ 0
Tactic:
show 0 ∣ 0 from dvd_self 0
State after:
no goals

State before:
case mpr
m k : ℕ
h : 0 = ↑0
⊢ 0 ∣ k → k = 0
Tactic:
assume h1 : 0 ∣ k
State after:
case mpr
m k : ℕ
h : 0 = ↑0
h1 : 0 ∣ k
⊢ k = 0

State before:
case mpr
m k : ℕ
h : 0 = ↑0
h1 : 0 ∣ k
⊢ k = 0
Tactic:
obtain (c : Nat) (h2 : k = 0 * c) from h1
State after:
case mpr
m k : ℕ
h : 0 = ↑0
h1 : 0 ∣ k
c : ℕ
h2 : k = 0 * c
⊢ k = 0

State before:
case mpr
m k : ℕ
h : 0 = ↑0
h1 : 0 ∣ k
c : ℕ
h2 : k = 0 * c
⊢ k = 0
Tactic:
rewrite [h2]
State after:
case mpr
m k : ℕ
h : 0 = ↑0
h1 : 0 ∣ k
c : ℕ
h2 : k = 0 * c
⊢ 0 * c = 0

State before:
case mpr
m k : ℕ
h : 0 = ↑0
h1 : 0 ∣ k
c : ℕ
h2 : k = 0 * c
⊢ 0 * c = 0
Tactic:
ring
State after:
no goals

State before:
m k n : ℕ
⊢ [↑k]_(n + 1) = [0]_(n + 1) ↔ n + 1 ∣ k
Tactic:
rewrite [cc_eq_iff_val_eq, val_nat_eq_mod, val_zero]
State after:
m k n : ℕ
⊢ k % (n + 1) = 0 ↔ n + 1 ∣ k

State before:
m k n : ℕ
⊢ k % (n + 1) = 0 ↔ n + 1 ∣ k
Tactic:
show k % (n + 1) = 0 ↔ n + 1 ∣ k from
  (Nat.dvd_iff_mod_eq_zero (n + 1) k).symm
State after:
no goals