-- Mathlib/Combinatorics/Enumerative/Bell.lean
theorem uniformBell_eq (m n : ℕ) : m.uniformBell n =
    ∏ p ∈ (Finset.range m), Nat.choose (p * n + n - 1) (n - 1)

Proof state:
case neg
m n : ℕ
hm : ¬m = 0
⊢ (multinomial {n} fun k => k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
by_cases hn : n = 0

Result:
case pos
m n : ℕ
hm : ¬m = 0
hn : n = 0
⊢ (multinomial {n} fun k => k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

case neg
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ (multinomial {n} fun k => k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Proof state:
m n : ℕ
⊢ m.uniformBell n = ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
unfold uniformBell bell

Result:
m n : ℕ
⊢ (multinomial (replicate m n).toFinset fun k => k * count k (replicate m n)) *
      ∏ k ∈ (replicate m n).toFinset.erase 0,
        ∏ j ∈ Finset.range (count k (replicate m n)), (j * k + k - 1).choose (k - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Proof state:
m n : ℕ
⊢ (multinomial (replicate m n).toFinset fun k => k * count k (replicate m n)) *
      ∏ k ∈ (replicate m n).toFinset.erase 0,
        ∏ j ∈ Finset.range (count k (replicate m n)), (j * k + k - 1).choose (k - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
rw [toFinset_replicate]

Result:
m n : ℕ
⊢ (multinomial (if m = 0 then ∅ else {n}) fun k => k * count k (replicate m n)) *
      ∏ k ∈ (if m = 0 then ∅ else {n}).erase 0,
        ∏ j ∈ Finset.range (count k (replicate m n)), (j * k + k - 1).choose (k - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Proof state:
case pos
m n : ℕ
hm : m = 0
⊢ (multinomial ∅ fun k => k * count k (replicate m n)) *
      ∏ x ∈ ∅.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
simp  [hm]

Result:
no goals

Proof state:
case pos
m n : ℕ
hm : ¬m = 0
hn : n = 0
⊢ (multinomial {n} fun k => k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
simp [hn]

Result:
no goals

Proof state:
case neg
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ (multinomial {n} fun k => k * count k (replicate m n)) *
      ∏ x ∈ {n}, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
simp [count_replicate]

Result:
no goals

Proof state:
case neg
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ (multinomial {n} fun k => k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
rw [show ({n} : Finset ℕ).erase 0 = {n} by simp [Ne.symm hn]]

Result:
case neg
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ (multinomial {n} fun k => k * count k (replicate m n)) *
      ∏ x ∈ {n}, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Proof state:
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ {n}.erase 0 = {n}

Tactic:
simp [Ne.symm hn]

Result:
no goals

Proof state:
m n : ℕ
⊢ (multinomial (if m = 0 then ∅ else {n}) fun k => k * count k (replicate m n)) *
      ∏ k ∈ (if m = 0 then ∅ else {n}).erase 0,
        ∏ j ∈ Finset.range (count k (replicate m n)), (j * k + k - 1).choose (k - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
split_ifs with hm

Result:
case pos
m n : ℕ
hm : m = 0
⊢ (multinomial ∅ fun k => k * count k (replicate m n)) *
      ∏ x ∈ ∅.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

case neg
m n : ℕ
hm : ¬m = 0
⊢ (multinomial {n} fun k => k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)