α : Type u_1
β : Type ?u.208063
γ : Type ?u.208066
δ : Type ?u.208069
inst✝ : MonoidWithZero α
a b : α
h : a ~ᵤ b
ha : a = 0
u : αˣ
hu : a * ↑u = b
⊢ b = 0
α : Type u_1
β : Type ?u.208063
γ : Type ?u.208066
δ : Type ?u.208069
inst✝ : MonoidWithZero α
a b : α
h : a ~ᵤ b
ha : a = 0
⊢ b = 0
let ⟨u, hu⟩ := h
no goals
α : Type u_1
β : Type ?u.208063
γ : Type ?u.208066
δ : Type ?u.208069
inst✝ : MonoidWithZero α
a b : α
h : a ~ᵤ b
ha : a = 0
u : αˣ
hu : a * ↑u = b
⊢ b = 0
simp [hu.symm, ha]
α : Type u_1
β : Type ?u.208063
γ : Type ?u.208066
δ : Type ?u.208069
inst✝ : MonoidWithZero α
a b : α
h : a ~ᵤ b
hb : b = 0
u : αˣ
hu : b * ↑u = a
⊢ a = 0
α : Type u_1
β : Type ?u.208063
γ : Type ?u.208066
δ : Type ?u.208069
inst✝ : MonoidWithZero α
a b : α
h : a ~ᵤ b
hb : b = 0
⊢ a = 0
let ⟨u, hu⟩ := h.symm
no goals
α : Type u_1
β : Type ?u.208063
γ : Type ?u.208066
δ : Type ?u.208069
inst✝ : MonoidWithZero α
a b : α
h : a ~ᵤ b
hb : b = 0
u : αˣ
hu : b * ↑u = a
⊢ a = 0
simp [hu.symm, hb]