α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ Finsupp.multinomial (↑toFinsupp m) =
    Nat.choose (↑card m) (count a m) * Finsupp.multinomial (↑toFinsupp (filter (fun x => a ≠ x) m))
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ multinomial m = Nat.choose (↑card m) (count a m) * multinomial (filter ((fun x x_1 => x ≠ x_1) a) m)
dsimp only [multinomial]
case h.e'_3.h.e'_5.h.e'_1
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ ↑card m = Finsupp.sum (↑toFinsupp m) fun x => id

case h.e'_3.h.e'_5.h.e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ count a m = ↑(↑toFinsupp m) a

case h.e'_3.h.e'_6.h.e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ ↑toFinsupp (filter (fun x => a ≠ x) m) = Finsupp.update (↑toFinsupp m) a 0
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ Finsupp.multinomial (↑toFinsupp m) =
    Nat.choose (↑card m) (count a m) * Finsupp.multinomial (↑toFinsupp (filter (fun x => a ≠ x) m))
convert Finsupp.multinomial_update a _
no goals
case h.e'_3.h.e'_5.h.e'_1
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ ↑card m = Finsupp.sum (↑toFinsupp m) fun x => id
rw [← Finsupp.card_toMultiset, m.toFinsupp_toMultiset]
no goals
case h.e'_3.h.e'_5.h.e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ count a m = ↑(↑toFinsupp m) a
simp only [toFinsupp_apply]
case h.e'_3.h.e'_6.h.e'_2.h
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
⊢ ↑(↑toFinsupp (filter (fun x => a✝ ≠ x) m)) a = ↑(Finsupp.update (↑toFinsupp m) a✝ 0) a
case h.e'_3.h.e'_6.h.e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ ↑toFinsupp (filter (fun x => a ≠ x) m) = Finsupp.update (↑toFinsupp m) a 0
ext1 a
case h.e'_3.h.e'_6.h.e'_2.h
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
⊢ (if a✝ ≠ a then count a m else 0) = Function.update (↑(↑toFinsupp m)) a✝ 0 a
case h.e'_3.h.e'_6.h.e'_2.h
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
⊢ ↑(↑toFinsupp (filter (fun x => a✝ ≠ x) m)) a = ↑(Finsupp.update (↑toFinsupp m) a✝ 0) a
rw [toFinsupp_apply, count_filter, Finsupp.coe_update]
case h.e'_3.h.e'_6.h.e'_2.h.inl
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
h : a✝ ≠ a
⊢ count a m = Function.update (↑(↑toFinsupp m)) a✝ 0 a

case h.e'_3.h.e'_6.h.e'_2.h.inr
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
h : ¬a✝ ≠ a
⊢ 0 = Function.update (↑(↑toFinsupp m)) a✝ 0 a
case h.e'_3.h.e'_6.h.e'_2.h
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
⊢ (if a✝ ≠ a then count a m else 0) = Function.update (↑(↑toFinsupp m)) a✝ 0 a
split_ifs with h
no goals
case h.e'_3.h.e'_6.h.e'_2.h.inl
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
h : a✝ ≠ a
⊢ count a m = Function.update (↑(↑toFinsupp m)) a✝ 0 a
rw [Function.update_noteq h.symm, toFinsupp_apply]
no goals
case h.e'_3.h.e'_6.h.e'_2.h.inr
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
h : ¬a✝ ≠ a
⊢ 0 = Function.update (↑(↑toFinsupp m)) a✝ 0 a
rw [not_ne_iff.1 h, Function.update_same]