awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ x ! * (c + 1) * x ! ^ c * c ! *
      ((∏ x_1 ∈ Finset.range c, (x_1 * x + x - 1).choose (x - 1)) * (c * x + x - 1).choose (x - 1)) =
    (x ! ^ c * c ! * ∏ j ∈ Finset.range c, (j * x + x - 1).choose (x - 1)) * (c * x + x - 1).choose (x - 1) * x ! *
      (c + 1)

Tactic:
ring
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
x : ℕ
hx : x ≠ 0
c : ℕ
rw :
  (x * c)! * (c * x + x - 1).choose (x - 1) * x ! * (c + 1) = (c + 1) * (c * x + x - 1).choose (x - 1) * (x * c)! * x !
⊢ (x ! ^ c * c ! * ∏ j ∈ Finset.range c, (j * x + x - 1).choose (x - 1)) * (c * x + x - 1).choose (x - 1) * x ! *
      (c + 1) =
    (c + 1) * (c * x + x - 1).choose (x - 1) * (x * c)! * x !

Tactic:
rw [bell_mul_eq_lemma hx]
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (x * c)! * (c * x + x - 1).choose (x - 1) * x ! * (c + 1) = (c + 1) * (c * x + x - 1).choose (x - 1) * (x * c)! * x !

Tactic:
ring
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
x : ℕ
hx : x ≠ 0
c : ℕ
rw : (x * c + x)! = (x * (c + 1))!
⊢ (c + 1) * (c * x + x - 1).choose (x - 1) * (x * c)! * x ! = (x * (c + 1))!

Tactic:
rw [← Nat.choose_mul_add hx, mul_comm c x, Nat.add_choose_mul_factorial_mul_factorial]

Premises used: mul_comm, Nat.add_choose_mul_factorial_mul_factorial, Nat.choose_mul_add
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (x * c + x)! = (x * (c + 1))!

Tactic:
ring_nf
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
⊢ Ne (α := ℕ) (∏ i ∈ m.toFinset, (i * count i m)!) 0

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
rw :
  (∏ 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)) *
          prod (map (fun (j : ℕ) ↦ j !) m) *
        ∏ j ∈ m.toFinset.erase 0, (count j m)!) =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !
⊢ ((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)) *
        prod (map (fun (j : ℕ) ↦ j !) m) *
      ∏ 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)]

Premises used: Nat.mul_right_inj
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
simp :
  (((∏ 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)) *
        prod (map (fun (j : ℕ) ↦ j !) m) *
      ∏ j ∈ m.toFinset.erase 0, (count j m)! =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !
⊢ (∏ 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)) *
          prod (map (fun (j : ℕ) ↦ j !) m) *
        ∏ j ∈ m.toFinset.erase 0, (count j m)!) =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !

Tactic:
simp only [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
rw :
  ((∑ 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)) *
        prod (map (fun (j : ℕ) ↦ j !) m) *
      ∏ j ∈ m.toFinset.erase 0, (count j m)! =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !
⊢ (((∏ 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)) *
        prod (map (fun (j : ℕ) ↦ j !) m) *
      ∏ j ∈ m.toFinset.erase 0, (count j m)! =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !

Tactic:
rw [Nat.multinomial_spec]

Premises used: Nat.multinomial_spec
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
simp :
  (∑ 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)) *
        HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!)) =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !
⊢ ((∑ 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)) *
        prod (map (fun (j : ℕ) ↦ j !) m) *
      ∏ j ∈ m.toFinset.erase 0, (count j m)! =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !

Tactic:
simp only [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
rw :
  (∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
        HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!) *
      (∑ i ∈ m.toFinset, i * count i m)! =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !
⊢ (∑ 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)) *
        HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!)) =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
hx :
  (∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
      HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!) =
    ∏ i ∈ m.toFinset, (i * count i m)!
hy : (∑ i ∈ m.toFinset, i * count i m)! = m.sum !
⊢ (∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
        HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ 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₂

Premises used: congr_arg₂
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
hx :
  HMul.hMul (α := ℕ) (∏ 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)!
⊢ (∏ k ∈ m.toFinset.erase 0, ∏ j ∈ Finset.range (count k m), (j * k + k - 1).choose (k - 1)) *
      HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ 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]

Premises used: Finset.prod_multiset_map_count, Finset.prod_mul_distrib, mul_assoc, mul_comm
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
this :
  HMul.hMul (α := ℕ) (∏ 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)!
pos :
  ∀ (hm : 0 ∈ m.toFinset),
    HMul.hMul (α := ℕ) (∏ 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)!
neg :
  ∀ (hm : 0 ∉ m.toFinset),
    HMul.hMul (α := ℕ) (∏ 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)!
⊢ HMul.hMul (α := ℕ) (∏ 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

Premises used: Multiset.toFinset
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
this :
  HMul.hMul (α := ℕ) (∏ 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
pos :
  (∏ 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)!
⊢ HMul.hMul (α := ℕ) (∏ 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]

Premises used: Finset.prod_erase_mul
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
this :
  HMul.hMul (α := ℕ) (∏ 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
pos :
  (∏ 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)!
⊢ (∏ 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]

Premises used: Finset.prod_erase_mul
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
this :
  HMul.hMul (α := ℕ) (∏ 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
pos :
  HMul.hMul (α := ℕ) (∏ 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)!
⊢ (∏ 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]

Premises used: one_pow, MulZeroClass.zero_mul, Nat.factorial_zero, mul_one
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
this :
  HMul.hMul (α := ℕ) (∏ 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
⊢ HMul.hMul (α := ℕ) (∏ 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:
this
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
this :
  HMul.hMul (α := ℕ) (∏ 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
⊢ HMul.hMul (α := ℕ) (∏ 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
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
this :
  HMul.hMul (α := ℕ) (∏ 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
neg :
  HMul.hMul (α := ℕ) (∏ 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)!
⊢ HMul.hMul (α := ℕ) (∏ 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_notMem hm]

Premises used: Finset.erase_eq_of_notMem
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
this :
  HMul.hMul (α := ℕ) (∏ 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
neg :
  HMul.hMul (α := ℕ) (∏ 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)!
⊢ HMul.hMul (α := ℕ) (∏ 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_notMem hm]

Premises used: Finset.erase_eq_of_notMem
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
this :
  HMul.hMul (α := ℕ) (∏ 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
⊢ HMul.hMul (α := ℕ) (∏ 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:
this
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
this :
  HMul.hMul (α := ℕ) (∏ 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
⊢ HMul.hMul (α := ℕ) (∏ 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
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
hx :
  HMul.hMul (α := ℕ) (∏ 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)!
⊢ HMul.hMul (α := ℕ) (∏ 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:
suffices this : _ by
      by_cases hm : 0 ∈ m.toFinset
      · rw [← Finset.prod_erase_mul _ _ hm]
        rw [← Finset.prod_erase_mul _ _ hm]
        simp only [factorial_zero, one_pow, mul_one, zero_mul]
        exact this
      · nth_rewrite 1 [← Finset.erase_eq_of_notMem hm]
        nth_rewrite 3 [← Finset.erase_eq_of_notMem hm]
        exact this
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
hx :
  Eq (α := ℕ)
    (∏ 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)!)
⊢ HMul.hMul (α := ℕ) (∏ 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]

Premises used: Finset.prod_mul_distrib
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
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)!
⊢ Eq (α := ℕ)
    (∏ 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

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
x : ℕ
hx : x ∈ m.toFinset.erase 0
hx₁ : x ≠ 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]

Premises used: mul_assoc, _private.0.Multiset.bell_mul_eq_lemma
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
x : ℕ
hx : x ∈ m.toFinset.erase 0
⊢ ¬x = 0 ∧ x ∈ m

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

Premises used: ne_eq, Finset.mem_erase, Multiset.mem_toFinset
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
x : ℕ
hx : ¬x = 0 ∧ x ∈ m
⊢ x ≠ 0

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

Premises used: ne_eq, And.left, not_false_eq_true
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
hy : ∑ i ∈ m.toFinset, i * count i m = m.sum
⊢ (∑ i ∈ m.toFinset, i * count i m)! = m.sum !

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
hy : Eq (α := ℕ) (∑ i ∈ m.toFinset, i * count i m) (∑ m_1 ∈ m.toFinset, count m_1 m • m_1)
⊢ ∑ i ∈ m.toFinset, i * count i m = m.sum

Tactic:
rw [Finset.sum_multiset_count]

Premises used: Finset.sum_multiset_count
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
⊢ Eq (α := ℕ) (∑ 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]

Premises used: mul_comm, smul_eq_mul
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
rw : m.bell * HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!) = m.sum !
rw₁ : HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!) ∣ m.sum !
rw₂ : HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!) ≠ 0
⊢ m.bell = m.sum ! / HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!)

Tactic:
rw [← Nat.mul_left_inj, Nat.div_mul_cancel _]

Premises used: Nat.div_mul_cancel, Nat.mul_left_inj
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
rw : m.bell * prod (map (fun (j : ℕ) ↦ j !) m) * ∏ j ∈ m.toFinset.erase 0, (count j m)! = m.sum !
⊢ m.bell * HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!) = m.sum !

Tactic:
rw [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
⊢ m.bell * prod (map (fun (j : ℕ) ↦ j !) m) * ∏ j ∈ m.toFinset.erase 0, (count j m)! = m.sum !

Tactic:
bell_mul_eq m

Premises used: Multiset.bell_mul_eq
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
⊢ m.bell * prod (map (fun (j : ℕ) ↦ j !) m) * ∏ j ∈ m.toFinset.erase 0, (count j m)! = m.sum !

Tactic:
exact bell_mul_eq m

Premises used: Multiset.bell_mul_eq
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
rw :
  HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!) ∣
    m.bell * HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!)
⊢ HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!) ∣ m.sum !

Tactic:
rw [← bell_mul_eq, mul_assoc]

Premises used: mul_assoc, Multiset.bell_mul_eq
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
⊢ HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!) ∣
    m.bell * HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!)

Tactic:
apply Nat.dvd_mul_left

Premises used: Nat.dvd_mul_left
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
rw : 0 < HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!)
⊢ HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!) ≠ 0

Tactic:
rw [← Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
hn : LT.lt (α := ℕ) 0 (prod (map (fun (j : ℕ) ↦ j !) m))
hm : LT.lt (α := ℕ) 0 (∏ j ∈ m.toFinset.erase 0, (count j m)!)
⊢ 0 < HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!)

Tactic:
apply Nat.mul_pos

Premises used: Nat.mul_pos
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
hn : ∀ a ∈ m, 0 < a !
⊢ LT.lt (α := ℕ) 0 (prod (map (fun (j : ℕ) ↦ j !) m))

Tactic:
simp only [CanonicallyOrderedAdd.multiset_prod_pos, mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]

Premises used: and_imp, CanonicallyOrderedAdd.multiset_prod_pos, Multiset.mem_map, forall_exists_index, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
⊢ ∀ a ∈ m, 0 < a !

Tactic:
fun _ _ ↦ Nat.factorial_pos _

Premises used: Nat.factorial_pos
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
⊢ ∀ a ∈ m, 0 < a !

Tactic:
exact fun _ _ ↦ Nat.factorial_pos _

Premises used: Nat.factorial_pos
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
hm : ∀ i ∈ m.toFinset.erase 0, 0 < (count i m)!
⊢ LT.lt (α := ℕ) 0 (∏ j ∈ m.toFinset.erase 0, (count j m)!)

Tactic:
apply Finset.prod_pos

Premises used: Finset.prod_pos
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
⊢ ∀ i ∈ m.toFinset.erase 0, 0 < (count i m)!

Tactic:
fun _ _ ↦ Nat.factorial_pos _

Premises used: Multiset.count, Nat.factorial_pos
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : Multiset ℕ
⊢ ∀ i ∈ m.toFinset.erase 0, 0 < (count i m)!

Tactic:
exact fun _ _ ↦ Nat.factorial_pos _

Premises used: Nat.factorial_pos
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
rw :
  (multinomial (if m = 0 then ∅ else {n}) fun (k : ℕ) ↦ k * count k (replicate m n)) *
      ∏ k ∈ Finset.erase (if m = 0 then ∅ else {n}) 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)
⊢ (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]

Premises used: Multiset.toFinset_replicate
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
pos :
  ∀ (hm : m = 0),
    (multinomial ∅ fun (k : ℕ) ↦ k * count k (replicate m n)) *
        ∏ x ∈ Finset.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)
neg :
  ∀ (hm : ¬m = 0),
    (multinomial {n} fun (k : ℕ) ↦ k * count k (replicate m n)) *
        ∏ x ∈ Finset.erase {n} 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)
⊢ (multinomial (if m = 0 then ∅ else {n}) fun (k : ℕ) ↦ k * count k (replicate m n)) *
      ∏ k ∈ Finset.erase (if m = 0 then ∅ else {n}) 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