Theorem: ℤω.my_add_left_neg (Mordell4/Eisenstein.lean)

State before:
a b c : ℤω
⊢ add (neg a) a = zero
Tactic:
cases a
State after:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ add (neg { x := x✝, y := y✝ }) { x := x✝, y := y✝ } = zero

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

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

State before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ { x := 0, y := 0 } = zero
Tactic:
tauto
State after:
no goals