no goals
α : Type u_1
β : Type ?u.216897
γ : Type ?u.216900
δ : Type ?u.216903
inst✝ : Monoid α
a b : α
h : a ~ᵤ b
u : αˣ
hu : a * ↑u = b
x✝ : IsUnit a
v : αˣ
hv : ↑v = a
⊢ ↑(v * u) = b
simp [hv, hu.symm]