Theorem: ℤω.my_zero_mul (Mordell4/Eisenstein.lean)

State before:
a b c : ℤω
⊢ mul zero a = zero
Tactic:
cases a
State after:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul zero { x := x✝, y := y✝ } = zero

State before:
case mk
b c : ℤω
x✝ y✝ : ℤ
⊢ mul zero { x := x✝, y := y✝ } = zero
Tactic:
simp [zero,mul]
State after:
no goals