no goals
α : Type ?u.1597
M₀ : Type u_1
G₀ : Type ?u.1603
M₀' : Type ?u.1606
G₀' : Type ?u.1609
F : Type ?u.1612
F' : Type ?u.1615
inst✝ : MonoidWithZero M₀
u : M₀ˣ
a : M₀
h : ↑u * a = 0
⊢ a = 0
simpa using mul_eq_zero_of_right (↑u⁻¹) h