-- Mathlib/Data/Nat/Choose/Multinomial.lean
theorem multinomial_coe_fill_of_not_mem {m : Fin (n + 1)} {s : Sym α (n - m)} {x : α} (hx : x ∉ s) :
    (fill x m s : Multiset α).multinomial = n.choose m * (s : Multiset α).multinomial

Proof state:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s) = ↑s

Tactic:
rw [coe_fill, coe_replicate, Multiset.filter_add]

Result:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 => x ≠ x_1) ↑s + Multiset.filter (fun x_1 => x ≠ x_1) (Multiset.replicate (↑m) x) = ↑s

Proof state:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ↑s + Multiset.filter (fun x_1 => x ≠ x_1) (Multiset.replicate (↑m) x) = ↑s

Tactic:
rw [add_right_eq_self]

Result:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 => x ≠ x_1) (Multiset.replicate (↑m) x) = 0

Proof state:
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
j : α
hj : j ∈ ↑s
h : x = j
⊢ x ∈ ↑s

Tactic:
simpa [h] using hj

Result:
no goals

Proof state:
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ (↑(fill x m s)).card.choose (Multiset.count x ↑(fill x m s)) *
      (Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s)).multinomial =
    n.choose ↑m * (↑s).multinomial

Tactic:
refine congrArg₂ _ ?_ ?_

Result:
case refine_1
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ (↑(fill x m s)).card.choose (Multiset.count x ↑(fill x m s)) = n.choose ↑m

case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ (Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s)).multinomial = (↑s).multinomial

Proof state:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ (Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s)).multinomial = (↑s).multinomial

Tactic:
refine congrArg _ ?_

Result:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s) = ↑s

Proof state:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ∀ a ∈ Multiset.replicate (↑m) x, ¬x ≠ a

Tactic:
exact fun j hj ↦ by simp [Multiset.mem_replicate.mp hj]

Result:
no goals

Proof state:
case refine_1
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ (↑(fill x m s)).card.choose (Multiset.count x ↑(fill x m s)) = n.choose ↑m

Tactic:
rw [card_coe, count_coe_fill_self_of_not_mem hx]

Result:
no goals

Proof state:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ∀ a ∈ ↑s, x ≠ a

Tactic:
exact fun j hj h ↦ hx <| by simpa [h] using hj

Result:
no goals

Proof state:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 => x ≠ x_1) ↑s + Multiset.filter (fun x_1 => x ≠ x_1) (Multiset.replicate (↑m) x) = ↑s

Tactic:
rw [Multiset.filter_eq_self.mpr]

Result:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ↑s + Multiset.filter (fun x_1 => x ≠ x_1) (Multiset.replicate (↑m) x) = ↑s

case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ∀ a ∈ ↑s, x ≠ a

Proof state:
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ s
⊢ (↑(fill x m s)).card.choose (Multiset.count x ↑(fill x m s)) *
      (Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s)).multinomial =
    n.choose ↑m * (↑s).multinomial

Tactic:
rw [← mem_coe] at hx

Result:
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ (↑(fill x m s)).card.choose (Multiset.count x ↑(fill x m s)) *
      (Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s)).multinomial =
    n.choose ↑m * (↑s).multinomial

Proof state:
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ s
⊢ (↑(fill x m s)).multinomial = n.choose ↑m * (↑s).multinomial

Tactic:
rw [Multiset.multinomial_filter_ne x]

Result:
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ s
⊢ (↑(fill x m s)).card.choose (Multiset.count x ↑(fill x m s)) *
      (Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s)).multinomial =
    n.choose ↑m * (↑s).multinomial

Proof state:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ Multiset.filter (fun x_1 => x ≠ x_1) (Multiset.replicate (↑m) x) = 0

Tactic:
rw [Multiset.filter_eq_nil]

Result:
case refine_2
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
⊢ ∀ a ∈ Multiset.replicate (↑m) x, ¬x ≠ a

Proof state:
n : ℕ
α : Type u_1
inst✝ : DecidableEq α
m : Fin (n + 1)
s : Sym α (n - ↑m)
x : α
hx : x ∉ ↑s
j : α
hj : j ∈ Multiset.replicate (↑m) x
⊢ ¬x ≠ j

Tactic:
simp [Multiset.mem_replicate.mp hj]

Result:
no goals