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

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 : 0 + (-a) = -a := by ring
State after:
m : ℕ
a : ℤ
h1 : [a]_m = [0]_m
h2 : 0 + -a = -a
⊢ [-a]_m = [0]_m

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

State before:
m : ℕ
a : ℤ
h1 : [a]_m = [0]_m
h2 : 0 + -a = -a
h3 : a + -a = 0
⊢ [-a]_m = [0]_m
Tactic:
show [-a]_m = [0]_m from
  calc [-a]_m
    _ = [0 + (-a)]_m := by rw [h2]
    _ = [0]_m + [-a]_m := by rw [add_class]
    _ = [a]_m + [-a]_m := by rw [h1]
    _ = [a + (-a)]_m := by rw [add_class]
    _ = [0]_m := by rw [h3]
State after:
no goals

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

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

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

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

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

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

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