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

State before:
a b c : ℤθ
⊢ mul a one = a
Tactic:
cases a
State after:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝, g := g✝, h := h✝ } one = { f := f✝, g := g✝, h := h✝ }

State before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝, g := g✝, h := h✝ } one = { f := f✝, g := g✝, h := h✝ }
Tactic:
simp [mul, one]
State after:
no goals