α : Type ?u.166351
β✝ : Type ?u.166354
γ : Type ?u.166357
δ : Type ?u.166360
β : Type u_1
inst✝ : CommMonoid β
u a b : β
hu : IsUnit u
⊢ a * u ~ᵤ b ↔ a ~ᵤ b
α : Type ?u.166351
β✝ : Type ?u.166354
γ : Type ?u.166357
δ : Type ?u.166360
β : Type u_1
inst✝ : CommMonoid β
u a b : β
hu : IsUnit u
⊢ u * a ~ᵤ b ↔ a ~ᵤ b
rw [mul_comm]
no goals
α : Type ?u.166351
β✝ : Type ?u.166354
γ : Type ?u.166357
δ : Type ?u.166360
β : Type u_1
inst✝ : CommMonoid β
u a b : β
hu : IsUnit u
⊢ a * u ~ᵤ b ↔ a ~ᵤ b
exact associated_mul_isUnit_left_iff hu