α : Type u_1
a : α
f : α →₀ ℕ
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
α : Type u_1
a : α
f : α →₀ ℕ
⊢ multinomial f = choose (sum f fun x => id) (↑f a) * multinomial (update f a 0)
simp only [multinomial_eq]
case pos
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)

case neg
α : Type u_1
a : α
f : α →₀ ℕ
h : ¬a ∈ f.support
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
α : Type u_1
a : α
f : α →₀ ℕ
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
by_cases a ∈ f.support
case neg
α : Type u_1
a : α
f : α →₀ ℕ
h : ↑f a = 0
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
case neg
α : Type u_1
a : α
f : α →₀ ℕ
h : ¬a ∈ f.support
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
rw [not_mem_support_iff] at h
no goals
case neg
α : Type u_1
a : α
f : α →₀ ℕ
h : ↑f a = 0
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
rw [h, Nat.choose_zero_right, one_mul, ← h, update_self]
case pos
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ choose (∑ x in f.support, ↑f x) (↑f a) * Nat.multinomial (Finset.erase f.support a) ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (Finset.erase f.support a) ↑(update f a 0)
case pos
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ Nat.multinomial f.support ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (update f a 0).support ↑(update f a 0)
rw [← Finset.insert_erase h, Nat.multinomial_insert _ f (Finset.not_mem_erase a _),
  Finset.add_sum_erase _ f h, support_update_zero]
case pos.e_a
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ Nat.multinomial (Finset.erase f.support a) ↑f = Nat.multinomial (Finset.erase f.support a) ↑(update f a 0)
case pos
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ choose (∑ x in f.support, ↑f x) (↑f a) * Nat.multinomial (Finset.erase f.support a) ↑f =
    choose (sum f fun x => id) (↑f a) * Nat.multinomial (Finset.erase f.support a) ↑(update f a 0)
congr 1
no goals
case pos.e_a
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ Nat.multinomial (Finset.erase f.support a) ↑f = Nat.multinomial (Finset.erase f.support a) ↑(update f a 0)
exact
  Nat.multinomial_congr _ fun _ h => (Function.update_noteq (Finset.mem_erase.1 h).1 0 f).symm