Theorem: ℤα.my_add_left_neg (Mordell4/Rt7Ring.lean)

State before:
a b c : ℤα
⊢ add (neg a) a = zero
Tactic:
cases a
State after:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ add (neg { z := z✝, w := w✝ }) { z := z✝, w := w✝ } = zero

State before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ add (neg { z := z✝, w := w✝ }) { z := z✝, w := w✝ } = zero
Tactic:
simp only [neg, add]
State after:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ { z := -z✝ + z✝, w := -w✝ + w✝ } = zero

State before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ { z := -z✝ + z✝, w := -w✝ + w✝ } = zero
Tactic:
simp only [add_left_neg]
State after:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ { z := 0, w := 0 } = zero

State before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ { z := 0, w := 0 } = zero
Tactic:
tauto
State after:
no goals