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

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

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