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

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

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