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

State before:
a b c : ℤα
⊢ mul a one = a
Tactic:
cases a
State after:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ mul { z := z✝, w := w✝ } one = { z := z✝, w := w✝ }

State before:
case mk
b c : ℤα
z✝ w✝ : ℤ
⊢ mul { z := z✝, w := w✝ } one = { z := z✝, w := w✝ }
Tactic:
simp [mul, one]
State after:
no goals