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

State before:
a b c : ℤω
⊢ add a zero = a
Tactic:
cases' a with x y
State after:
case mk
b c : ℤω
x y : ℤ
⊢ add { x := x, y := y } zero = { x := x, y := y }

State before:
case mk
b c : ℤω
x y : ℤ
⊢ add { x := x, y := y } zero = { x := x, y := y }
Tactic:
simp only [add, zero, add_zero]
State after:
no goals