α : Type u_1
β : Type ?u.35843
γ : Type ?u.35846
δ : Type ?u.35849
inst✝ : CommMonoid α
p q : Multiset α
⊢ Multiset.Rel Associated p q ↔ Multiset.Rel (fun a b => Associates.mk a = Associates.mk b) p q
α : Type u_1
β : Type ?u.35843
γ : Type ?u.35846
δ : Type ?u.35849
inst✝ : CommMonoid α
p q : Multiset α
⊢ Multiset.Rel Associated p q ↔ Multiset.map Associates.mk p = Multiset.map Associates.mk q
rw [← Multiset.rel_eq, Multiset.rel_map]
no goals
α : Type u_1
β : Type ?u.35843
γ : Type ?u.35846
δ : Type ?u.35849
inst✝ : CommMonoid α
p q : Multiset α
⊢ Multiset.Rel Associated p q ↔ Multiset.Rel (fun a b => Associates.mk a = Associates.mk b) p q
simp only [mk_eq_mk_iff_associated]