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

State before:
m : ℕ
a : ℤ
⊢ [a]_m = [0]_m ↔ ↑m ∣ a
Tactic:
obtain (k : Nat) (h1 : a = ↑k ∨ a = -↑k) from Int.eq_nat_or_neg a
State after:
m : ℕ
a : ℤ
k : ℕ
h1 : a = ↑k ∨ a = -↑k
⊢ [a]_m = [0]_m ↔ ↑m ∣ a

State before:
m : ℕ
a : ℤ
k : ℕ
h1 : a = ↑k ∨ a = -↑k
⊢ [a]_m = [0]_m ↔ ↑m ∣ a
Tactic:
by_cases on h1
State after:
case Case_1
m : ℕ
a : ℤ
k : ℕ
h1 : a = ↑k
⊢ [a]_m = [0]_m ↔ ↑m ∣ a

case Case_2
m : ℕ
a : ℤ
k : ℕ
h1 : a = -↑k
⊢ [a]_m = [0]_m ↔ ↑m ∣ a

State before:
case Case_1
m : ℕ
a : ℤ
k : ℕ
h1 : a = ↑k
⊢ [a]_m = [0]_m ↔ ↑m ∣ a
Tactic:
rewrite [h1, Int.coe_nat_dvd]
State after:
case Case_1
m : ℕ
a : ℤ
k : ℕ
h1 : a = ↑k
⊢ [↑k]_m = [0]_m ↔ m ∣ k

State before:
case Case_1
m : ℕ
a : ℤ
k : ℕ
h1 : a = ↑k
⊢ [↑k]_m = [0]_m ↔ m ∣ k
Tactic:
show [↑k]_m = [0]_m ↔ m ∣ k from cc_nat_zero_iff_dvd m k
State after:
no goals

State before:
case Case_2
m : ℕ
a : ℤ
k : ℕ
h1 : a = -↑k
⊢ [a]_m = [0]_m ↔ ↑m ∣ a
Tactic:
rewrite [h1, cc_neg_zero_iff_cc_zero, Int.dvd_neg, Int.coe_nat_dvd]
State after:
case Case_2
m : ℕ
a : ℤ
k : ℕ
h1 : a = -↑k
⊢ [↑k]_m = [0]_m ↔ m ∣ k

State before:
case Case_2
m : ℕ
a : ℤ
k : ℕ
h1 : a = -↑k
⊢ [↑k]_m = [0]_m ↔ m ∣ k
Tactic:
show [↑k]_m = [0]_m ↔ m ∣ k from cc_nat_zero_iff_dvd m k
State after:
no goals