α : Type ?u.161759
β✝ : Type ?u.161762
γ : Type ?u.161765
δ : Type ?u.161768
β : Type u_1
inst✝ : CommMonoid β
a u : β
hu : IsUnit u
⊢ a * u ~ᵤ a
α : Type ?u.161759
β✝ : Type ?u.161762
γ : Type ?u.161765
δ : Type ?u.161768
β : Type u_1
inst✝ : CommMonoid β
a u : β
hu : IsUnit u
⊢ u * a ~ᵤ a
rw [mul_comm]
no goals
α : Type ?u.161759
β✝ : Type ?u.161762
γ : Type ?u.161765
δ : Type ?u.161768
β : Type u_1
inst✝ : CommMonoid β
a u : β
hu : IsUnit u
⊢ a * u ~ᵤ a
exact associated_mul_unit_left _ _ hu