no goals
α : Type u_1
β : Type ?u.295731
γ : Type ?u.295734
δ : Type ?u.295737
inst✝ : CommMonoid α
a : α
⊢ IsUnit (Associates.mk a) ↔ a ~ᵤ 1
rw [isUnit_iff_eq_one, one_eq_mk_one, mk_eq_mk_iff_associated]