-- Mathlib/Combinatorics/Enumerative/Bell.lean
theorem bell_mul_eq (m : Multiset ℕ) :
    m.bell * (m.map (fun j ↦ j !)).prod * ∏ j ∈ (m.toFinset.erase 0), (m.count j)!
      = m.sum !

Proof state:
case pos
m : Multiset ℕ
this : ?m.9930
hm : 0 ∈ m.toFinset
⊢ (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ x ∈ m.toFinset.erase 0, (x * count x m)!

Tactic:
exact this

Result:
no goals

Proof state:
m : Multiset ℕ
⊢ (∑ i ∈ m.toFinset, i * count i m)! *
      ((∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
        ((map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!)) =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !

Tactic:
rw [mul_comm]

Result:
m : Multiset ℕ
⊢ (∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
        ((map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) *
      (∑ i ∈ m.toFinset, i * count i m)! =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !

Proof state:
case hx
m : Multiset ℕ
⊢ ∏ x ∈ m.toFinset.erase 0,
      x ! ^ count x m * ((count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1)) =
    ∏ x ∈ m.toFinset.erase 0, (x * count x m)!

Tactic:
apply Finset.prod_congr rfl

Result:
case hx
m : Multiset ℕ
⊢ ∀ x ∈ m.toFinset.erase 0,
    x ! ^ count x m * ((count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1)) = (x * count x m)!

Proof state:
m : Multiset ℕ
⊢ m.bell * (map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)! = m.sum !

Tactic:
unfold bell

Result:
m : Multiset ℕ
⊢ ((Nat.multinomial m.toFinset fun k => k * count k m) *
          ∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
        (map (fun j => j !) m).prod *
      ∏ j ∈ m.toFinset.erase 0, (count j m)! =
    m.sum !

Proof state:
case hy.h
m : Multiset ℕ
⊢ ∑ i ∈ m.toFinset, i * count i m = m.sum

Tactic:
rw [Finset.sum_multiset_count]

Result:
case hy.h
m : Multiset ℕ
⊢ ∑ i ∈ m.toFinset, i * count i m = ∑ m_1 ∈ m.toFinset, count m_1 m • m_1

Proof state:
case neg
m : Multiset ℕ
this :
  (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ x ∈ m.toFinset.erase 0, (x * count x m)!
hm : 0 ∉ m.toFinset
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Tactic:
nth_rewrite 1 [← Finset.erase_eq_of_not_mem hm]

Result:
case neg
m : Multiset ℕ
this :
  (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ x ∈ m.toFinset.erase 0, (x * count x m)!
hm : 0 ∉ m.toFinset
⊢ (∏ m_1 ∈ m.toFinset.erase 0, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Proof state:
case pos
m : Multiset ℕ
this : ?m.9930
hm : 0 ∈ m.toFinset
⊢ (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) * 0! ^ count 0 m *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Tactic:
rw [← Finset.prod_erase_mul _ _ hm]

Result:
case pos
m : Multiset ℕ
this : ?m.9930
hm : 0 ∈ m.toFinset
⊢ (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) * 0! ^ count 0 m *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    (∏ x ∈ m.toFinset.erase 0, (x * count x m)!) * (0 * count 0 m)!

Proof state:
m : Multiset ℕ
⊢ ∏ i ∈ m.toFinset, (i * count i m)! ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
m : Multiset ℕ
⊢ ((Nat.multinomial m.toFinset fun k => k * count k m) *
          ∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
        (map (fun j => j !) m).prod *
      ∏ j ∈ m.toFinset.erase 0, (count j m)! =
    m.sum !

Tactic:
rw [← Nat.mul_right_inj (a := ∏ i ∈ m.toFinset, (i * count i m)!) (by positivity)]

Result:
m : Multiset ℕ
⊢ (∏ i ∈ m.toFinset, (i * count i m)!) *
      (((Nat.multinomial m.toFinset fun k => k * count k m) *
            ∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
          (map (fun j => j !) m).prod *
        ∏ j ∈ m.toFinset.erase 0, (count j m)!) =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !

Proof state:
case hx
m : Multiset ℕ
⊢ (∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
      ((map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Tactic:
rw [mul_comm, mul_assoc, ← Finset.prod_mul_distrib, Finset.prod_multiset_map_count]

Result:
case hx
m : Multiset ℕ
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Proof state:
m : Multiset ℕ
this : ?m.9930
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Tactic:
by_cases hm : 0 ∈ m.toFinset

Result:
case pos
m : Multiset ℕ
this : ?m.9930
hm : 0 ∈ m.toFinset
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

case neg
m : Multiset ℕ
this : ?m.9930
hm : 0 ∉ m.toFinset
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Proof state:
case hx
m : Multiset ℕ
⊢ ∀ x ∈ m.toFinset.erase 0,
    x ! ^ count x m * ((count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1)) = (x * count x m)!

Tactic:
intro x hx

Result:
case hx
m : Multiset ℕ
x : ℕ
hx : x ∈ m.toFinset.erase 0
⊢ x ! ^ count x m * ((count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1)) = (x * count x m)!

Proof state:
case pos
m : Multiset ℕ
this : ?m.9930
hm : 0 ∈ m.toFinset
⊢ (∏ m_1 ∈ m.toFinset, m_1 ! ^ count m_1 m) *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Tactic:
rw [← Finset.prod_erase_mul _ _ hm]

Result:
case pos
m : Multiset ℕ
this : ?m.9930
hm : 0 ∈ m.toFinset
⊢ (∏ x ∈ m.toFinset.erase 0, x ! ^ count x m) * 0! ^ count 0 m *
      ∏ x ∈ m.toFinset.erase 0, (count x m)! * ∏ j ∈ Finset.range (count x m), (j * x + x - 1).choose (x - 1) =
    ∏ i ∈ m.toFinset, (i * count i m)!

Proof state:
case hx.hx
m : Multiset ℕ
x : ℕ
hx : x ∈ m.toFinset.erase 0
⊢ x ≠ 0

Tactic:
simp only [Finset.mem_erase, ne_eq, mem_toFinset] at hx

Result:
case hx.hx
m : Multiset ℕ
x : ℕ
hx : ¬x = 0 ∧ x ∈ m
⊢ x ≠ 0

Proof state:
m : Multiset ℕ
⊢ (∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
        ((map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) *
      (∑ i ∈ m.toFinset, i * count i m)! =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !

Tactic:
apply congr_arg₂

Result:
case hx
m : Multiset ℕ
⊢ (∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
      ((map (fun j => j !) m).prod * ∏ j ∈ m.toFinset.erase 0, (count j m)!) =
    ∏ i ∈ m.toFinset, (i * count i m)!

case hy
m : Multiset ℕ
⊢ (∑ i ∈ m.toFinset, i * count i m)! = m.sum !