α : Type u_1
β : Type ?u.8631
ι : Type ?u.8634
inst✝ : DecidableEq α
s : Multiset α
x : α
this : ↑(↑(AddEquiv.symm toMultiset) s) x = ↑(Equiv.invFun toMultiset.toEquiv s) x
⊢ ↑(↑(AddEquiv.symm toMultiset) s) x = Multiset.count x s
α : Type u_1
β : Type ?u.8631
ι : Type ?u.8634
inst✝ : DecidableEq α
s : Multiset α
x : α
⊢ ↑(↑(AddEquiv.symm toMultiset) s) x = Multiset.count x s
have : Finsupp.toMultiset.symm s x = Finsupp.toMultiset.invFun s x := rfl
α : Type u_1
β : Type ?u.8631
ι : Type ?u.8634
inst✝ : DecidableEq α
s : Multiset α
x : α
this : ↑(↑(AddEquiv.symm toMultiset) s) x = ↑(Equiv.invFun toMultiset.toEquiv s) x
⊢ Multiset.count x s = Multiset.count x s
α : Type u_1
β : Type ?u.8631
ι : Type ?u.8634
inst✝ : DecidableEq α
s : Multiset α
x : α
this : ↑(↑(AddEquiv.symm toMultiset) s) x = ↑(Equiv.invFun toMultiset.toEquiv s) x
⊢ ↑(↑(AddEquiv.symm toMultiset) s) x = Multiset.count x s
simp_rw [this, toMultiset, coe_mk]
no goals
α : Type u_1
β : Type ?u.8631
ι : Type ?u.8634
inst✝ : DecidableEq α
s : Multiset α
x : α
this : ↑(↑(AddEquiv.symm toMultiset) s) x = ↑(Equiv.invFun toMultiset.toEquiv s) x
⊢ Multiset.count x s = Multiset.count x s
congr