case h.h.a
α : Type u_1
β : Type ?u.249344
γ : Type ?u.249347
δ : Type ?u.249350
inst✝¹ : Monoid α
inst✝ : Unique αˣ
x✝¹ x✝ : α
⊢ x✝¹ ~ᵤ x✝ ↔ x✝¹ = x✝
α : Type u_1
β : Type ?u.249344
γ : Type ?u.249347
δ : Type ?u.249350
inst✝¹ : Monoid α
inst✝ : Unique αˣ
⊢ Associated = Eq
ext
no goals
case h.h.a
α : Type u_1
β : Type ?u.249344
γ : Type ?u.249347
δ : Type ?u.249350
inst✝¹ : Monoid α
inst✝ : Unique αˣ
x✝¹ x✝ : α
⊢ x✝¹ ~ᵤ x✝ ↔ x✝¹ = x✝
rw [associated_iff_eq]