Theorem: ℤθ.my_zsmul_zero' (Mordell4/CubicRing.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 : ℤθ
⊢ { f := 0 * a.f, g := 0 * a.g, h := 0 * a.h } = zero

State before:
a✝ b c a : ℤθ
⊢ { f := 0 * a.f, g := 0 * a.g, h := 0 * a.h } = zero
Tactic:
rw [MulZeroClass.zero_mul]
State after:
a✝ b c a : ℤθ
⊢ { f := 0, g := 0 * a.g, h := 0 * a.h } = zero

State before:
a✝ b c a : ℤθ
⊢ { f := 0, g := 0 * a.g, h := 0 * a.h } = zero
Tactic:
rw [MulZeroClass.zero_mul]
State after:
a✝ b c a : ℤθ
⊢ { f := 0, g := 0, h := 0 * a.h } = zero

State before:
a✝ b c a : ℤθ
⊢ { f := 0, g := 0, h := 0 * a.h } = zero
Tactic:
rw [MulZeroClass.zero_mul]
State after:
a✝ b c a : ℤθ
⊢ { f := 0, g := 0, h := 0 } = zero

State before:
a✝ b c a : ℤθ
⊢ { f := 0, g := 0, h := 0 } = zero
Tactic:
rw [← zero]
State after:
no goals