Theorem: ℤθ.my_add_left_neg (Mordell4/CubicRing.lean)

State before:
a b c : ℤθ
⊢ add (neg a) a = zero
Tactic:
cases a
State after:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ add (neg { f := f✝, g := g✝, h := h✝ }) { f := f✝, g := g✝, h := h✝ } = zero

State before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ add (neg { f := f✝, g := g✝, h := h✝ }) { f := f✝, g := g✝, h := h✝ } = zero
Tactic:
simp only [neg, add]
State after:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ { f := -f✝ + f✝, g := -g✝ + g✝, h := -h✝ + h✝ } = zero

State before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ { f := -f✝ + f✝, g := -g✝ + g✝, h := -h✝ + h✝ } = zero
Tactic:
simp only [add_left_neg]
State after:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ { f := 0, g := 0, h := 0 } = zero

State before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ { f := 0, g := 0, h := 0 } = zero
Tactic:
tauto
State after:
no goals