α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ choose (succ (f a) + succ (f b)) (succ (f a)) =
    choose (succ (f a) + if b = a then succ (f a) else f b) (succ (f a)) + choose (f a + succ (f b)) (f a)
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ multinomial {a, b} (Function.update (Function.update f a (succ (f a))) b (succ (f b))) =
    multinomial {a, b} (Function.update f a (succ (f a))) + multinomial {a, b} (Function.update f b (succ (f b)))
simp only [binomial_eq_choose, Function.update_apply,
  h, Ne.def, ite_true, ite_false]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ choose (succ (f a) + succ (f b)) (succ (f a)) =
    choose (succ (f a) + f b) (succ (f a)) + choose (f a + succ (f b)) (f a)
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ choose (succ (f a) + succ (f b)) (succ (f a)) =
    choose (succ (f a) + if b = a then succ (f a) else f b) (succ (f a)) + choose (f a + succ (f b)) (f a)
rw [if_neg h.symm]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ choose (f a + succ (f b)) (f a) + choose (f a + succ (f b)) (succ (f a)) =
    choose (f a + succ (f b)) (succ (f a)) + choose (f a + succ (f b)) (f a)
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ choose (succ (f a) + succ (f b)) (succ (f a)) =
    choose (succ (f a) + f b) (succ (f a)) + choose (f a + succ (f b)) (f a)
rw [add_succ, choose_succ_succ, succ_add_eq_succ_add]
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ choose (f a + succ (f b)) (f a) + choose (f a + succ (f b)) (succ (f a)) =
    choose (f a + succ (f b)) (succ (f a)) + choose (f a + succ (f b)) (f a)
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ choose (f a + succ (f b)) (f a) + choose (f a + succ (f b)) (succ (f a)) =
    choose (f a + succ (f b)) (succ (f a)) + choose (f a + succ (f b)) (f a)
simp only
no goals
α : Type u_1
s : Finset α
f : α → ℕ
a b : α
n : ℕ
inst✝ : DecidableEq α
h : a ≠ b
⊢ choose (f a + succ (f b)) (f a) + choose (f a + succ (f b)) (succ (f a)) =
    choose (f a + succ (f b)) (succ (f a)) + choose (f a + succ (f b)) (f a)
ring