α : Type u_1
β : Type ?u.399080
γ : Type ?u.399083
inst✝ : DecidableEq α
s t : Multiset α
_l₁ _l₂ : List α
⊢ _l₁ ≈ _l₂ ↔ ∀ (a : α), List.count a _l₁ = List.count a _l₂
α : Type u_1
β : Type ?u.399080
γ : Type ?u.399083
inst✝ : DecidableEq α
s t : Multiset α
_l₁ _l₂ : List α
⊢ _l₁ ≈ _l₂ ↔ ∀ (a : α), count a (Quotient.mk (isSetoid α) _l₁) = count a (Quotient.mk (isSetoid α) _l₂)
simp only [quot_mk_to_coe, coe_filter, mem_coe, coe_count, decide_eq_true_eq]
no goals
α : Type u_1
β : Type ?u.399080
γ : Type ?u.399083
inst✝ : DecidableEq α
s t : Multiset α
_l₁ _l₂ : List α
⊢ _l₁ ≈ _l₂ ↔ ∀ (a : α), List.count a _l₁ = List.count a _l₂
apply perm_iff_count