no goals
α : Type ?u.682
M₀ : Type u_1
G₀ : Type ?u.688
M₀' : Type ?u.691
G₀' : Type ?u.694
F : Type ?u.697
F' : Type ?u.700
inst✝ : MulZeroClass M₀
a✝ b✝ a b : M₀
h : a ≠ 0 → b = 0
ha : a = 0
⊢ a * b = 0
rw [ha, zero_mul]
no goals
α : Type ?u.682
M₀ : Type u_1
G₀ : Type ?u.688
M₀' : Type ?u.691
G₀' : Type ?u.694
F : Type ?u.697
F' : Type ?u.700
inst✝ : MulZeroClass M₀
a✝ b✝ a b : M₀
h : a ≠ 0 → b = 0
ha : ¬a = 0
⊢ a * b = 0
rw [h ha, mul_zero]