α : Type u_1
β : Type ?u.151491
γ : Type ?u.151494
δ : Type ?u.151497
inst✝ : MonoidWithZero α
a : α
h✝ : a ~ᵤ 0
u : αˣ
h : 0 * ↑u = a
⊢ a = 0
α : Type u_1
β : Type ?u.151491
γ : Type ?u.151494
δ : Type ?u.151497
inst✝ : MonoidWithZero α
a : α
h : a ~ᵤ 0
⊢ a = 0
let ⟨u, h⟩ := h.symm
no goals
α : Type u_1
β : Type ?u.151491
γ : Type ?u.151494
δ : Type ?u.151497
inst✝ : MonoidWithZero α
a : α
h✝ : a ~ᵤ 0
u : αˣ
h : 0 * ↑u = a
⊢ a = 0
simpa using h.symm