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

State before:
a b c : ℤθ
⊢ add a zero = a
Tactic:
cases' a with x y
State after:
case mk
b c : ℤθ
x y h✝ : ℤ
⊢ add { f := x, g := y, h := h✝ } zero = { f := x, g := y, h := h✝ }

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