-- 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:
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:
simp only [mul_assoc]

Result:
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 !

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

Tactic:
apply congr_arg

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

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.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)!

Tactic:
nth_rewrite 3 [← 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.erase 0, (i * count i m)!

Proof state:
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)!

Tactic:
rw [← mul_assoc, bell_mul_eq_lemma]

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

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

Tactic:
simp only [ne_eq, hx.1, not_false_eq_true]

Result:
no goals

Proof state:
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 !

Tactic:
rw [Nat.multinomial_spec]

Result:
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 !

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.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.erase 0, (i * count i m)!

Tactic:
exact this

Result:
no goals

Proof state:
case hx
m : Multiset ℕ
⊢ (∏ 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:
rw [← Finset.prod_mul_distrib]

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 ∈ m.toFinset.erase 0, (x * count x m)!

Proof state:
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 !

Tactic:
simp only [← mul_assoc]

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 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)!

Tactic:
simp only [factorial_zero, one_pow, mul_one, zero_mul]

Result:
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)!

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

Tactic:
simp only [smul_eq_mul, mul_comm]

Result:
no goals