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

State before:
m : ℕ
a : ℤ
⊢ [-a]_m = [0]_m ↔ [a]_m = [0]_m
Tactic:
apply Iff.intro _ (cc_neg_zero_of_cc_zero m a)
State after:
m : ℕ
a : ℤ
⊢ [-a]_m = [0]_m → [a]_m = [0]_m

State before:
m : ℕ
a : ℤ
⊢ [-a]_m = [0]_m → [a]_m = [0]_m
Tactic:
assume h1 : [-a]_m = [0]_m
State after:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
⊢ [a]_m = [0]_m

State before:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
⊢ [a]_m = [0]_m
Tactic:
have h2 : [-(-a)]_m = [0]_m := cc_neg_zero_of_cc_zero m (-a) h1
State after:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
h2 : [- -a]_m = [0]_m
⊢ [a]_m = [0]_m

State before:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
h2 : [- -a]_m = [0]_m
⊢ [a]_m = [0]_m
Tactic:
have h3 : -(-a) = a := by ring
State after:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
h2 : [- -a]_m = [0]_m
h3 : - -a = a
⊢ [a]_m = [0]_m

State before:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
h2 : [- -a]_m = [0]_m
h3 : - -a = a
⊢ [a]_m = [0]_m
Tactic:
rewrite [h3] at h2
State after:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
h2 : [a]_m = [0]_m
h3 : - -a = a
⊢ [a]_m = [0]_m

State before:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
h2 : [a]_m = [0]_m
h3 : - -a = a
⊢ [a]_m = [0]_m
Tactic:
show [a]_m = [0]_m from h2
State after:
no goals

State before:
m : ℕ
a : ℤ
h1 : [-a]_m = [0]_m
h2 : [- -a]_m = [0]_m
⊢ - -a = a
Tactic:
ring
State after:
no goals