no goals
α : Type ?u.430
M₀ : Type u_1
G₀ : Type ?u.436
M₀' : Type ?u.439
G₀' : Type ?u.442
F : Type ?u.445
F' : Type ?u.448
inst✝ : MonoidWithZero M₀
u : M₀ˣ
a : M₀
h : a * ↑u = 0
⊢ a = 0
simpa using mul_eq_zero_of_left h ↑u⁻¹