Theorem: ℤα.my_zsmul_zero' (Mordell4/Rt7Ring.lean)

State before:
a b c : ℤα
⊢ ∀ (a : ℤα), zsmul 0 a = zero
Tactic:
intro a
State after:
a✝ b c a : ℤα
⊢ zsmul 0 a = zero

State before:
a✝ b c a : ℤα
⊢ zsmul 0 a = zero
Tactic:
unfold zsmul
State after:
a✝ b c a : ℤα
⊢ { z := 0 * a.z, w := 0 * a.w } = zero

State before:
a✝ b c a : ℤα
⊢ { z := 0 * a.z, w := 0 * a.w } = zero
Tactic:
rw [MulZeroClass.zero_mul]
State after:
a✝ b c a : ℤα
⊢ { z := 0, w := 0 * a.w } = zero

State before:
a✝ b c a : ℤα
⊢ { z := 0, w := 0 * a.w } = zero
Tactic:
rw [MulZeroClass.zero_mul]
State after:
a✝ b c a : ℤα
⊢ { z := 0, w := 0 } = zero

State before:
a✝ b c a : ℤα
⊢ { z := 0, w := 0 } = zero
Tactic:
rw [← zero]
State after:
no goals