α : Type ?u.20128
s : Finset α
f : α → ℕ
a✝ b✝ : α
n a b c : ℕ
⊢ (Matrix.vecCons a ![b, c] 0 + Matrix.vecCons a ![b, c] 1 + Matrix.vecCons a ![b, c] 2)! /
      ((Matrix.vecCons a ![b, c] 0)! * (Matrix.vecCons a ![b, c] 1)! * (Matrix.vecCons a ![b, c] 2)!) =
    (a + b + c)! / (a ! * b ! * c !)
α : Type ?u.20128
s : Finset α
f : α → ℕ
a✝ b✝ : α
n a b c : ℕ
⊢ multinomial Finset.univ ![a, b, c] = (a + b + c)! / (a ! * b ! * c !)
rw [multinomial, Fin.sum_univ_three, Fin.prod_univ_three]
no goals
α : Type ?u.20128
s : Finset α
f : α → ℕ
a✝ b✝ : α
n a b c : ℕ
⊢ (Matrix.vecCons a ![b, c] 0 + Matrix.vecCons a ![b, c] 1 + Matrix.vecCons a ![b, c] 2)! /
      ((Matrix.vecCons a ![b, c] 0)! * (Matrix.vecCons a ![b, c] 1)! * (Matrix.vecCons a ![b, c] 2)!) =
    (a + b + c)! / (a ! * b ! * c !)
rfl