awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Basic (goal)
Goal:
V : Type u_1
inst : DecidableEq V
inst_1 : Fintype V
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := V → V → Bool) (β := Digraph V) (⇑Digraph.mk' : (a : V → V → Bool) → Digraph V)
have refine : Surjective.{u_1 + 1, u_1 + 1} (α := V → V → Bool) (β := Digraph V) (⇑Digraph.mk' : (a : V → V → Bool) → Digraph V)
Tactic: classical
    refine ⟨Embedding.injective _, ?_⟩
    intro G
    use fun v w ↦ G.Adj v w
    ext v w
    simp
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Basic (goal)
Goal:
V : Type u_1
inst : DecidableEq V
inst_1 : Fintype V
refine :
  Surjective.{u_1 + 1, u_1 + 1} (α := V → V → Bool) (β := Digraph V) (⇑Digraph.mk' : (a : V → V → Bool) → Digraph V)
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := V → V → Bool) (β := Digraph V) (⇑Digraph.mk' : (a : V → V → Bool) → Digraph V)
have refine₁ : ∀ (G : Digraph V), ∃ (a : V → V → Bool), (Digraph.mk' : (a : V → V → Bool) → Digraph V) a = G
Tactic: classical
    refine ⟨Embedding.injective _, ?_⟩
    intro G
    use fun v w ↦ G.Adj v w
    ext v w
    simp
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Basic (goal)
Goal:
V : Type u_1
inst : DecidableEq V
inst_1 : Fintype V
refine :
  Surjective.{u_1 + 1, u_1 + 1} (α := V → V → Bool) (β := Digraph V) (⇑Digraph.mk' : (a : V → V → Bool) → Digraph V)
refine₁ : ∀ (G : Digraph V), ∃ (a : V → V → Bool), (Digraph.mk' : (a : V → V → Bool) → Digraph V) a = G
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := V → V → Bool) (β := Digraph V) (⇑Digraph.mk' : (a : V → V → Bool) → Digraph V)
have h : ∀ (G : Digraph V), ((Digraph.mk' : (a : V → V → Bool) → Digraph V) fun (v w : V) ↦ decide (G.Adj v w)) = G
Tactic: classical
    refine ⟨Embedding.injective _, ?_⟩
    intro G
    use fun v w ↦ G.Adj v w
    ext v w
    simp
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Basic (goal)
Goal:
V : Type u_1
inst : DecidableEq V
inst_1 : Fintype V
refine :
  Surjective.{u_1 + 1, u_1 + 1} (α := V → V → Bool) (β := Digraph V) (⇑Digraph.mk' : (a : V → V → Bool) → Digraph V)
refine₁ : ∀ (G : Digraph V), ∃ (a : V → V → Bool), (Digraph.mk' : (a : V → V → Bool) → Digraph V) a = G
h : ∀ (G : Digraph V), ((Digraph.mk' : (a : V → V → Bool) → Digraph V) fun (v w : V) ↦ decide (G.Adj v w)) = G
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := V → V → Bool) (β := Digraph V) (⇑Digraph.mk' : (a : V → V → Bool) → Digraph V)
have h₁ : ∀ (G : Digraph V) (v w : V),
  Digraph.Adj ((Digraph.mk' : (a : V → V → Bool) → Digraph V) fun (v w : V) ↦ decide (G.Adj v w)) v w ↔ G.Adj v w
Tactic: classical
    refine ⟨Embedding.injective _, ?_⟩
    intro G
    use fun v w ↦ G.Adj v w
    ext v w
    simp
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u_2
G_1 : Digraph V
a b : V
G : Digraph V
v w : V
h : (Digraph.completeDigraph V).Adj v w
⊢ (G ⊔ Gᶜ).Adj v w
have tauto : ¬G.Adj v w → Gᶜ.Adj v w
Tactic: tauto
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u_2
G : Digraph V
a b : V
ι_1 : Type u_2
κ : ι_1 → Type u_2
f : (a : ι_1) → κ a → Digraph V
⊢ Eq.{u_2 + 1} (α := Digraph V) (⨅ (a : ι_1), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι_1) → κ a), ⨅ (a : ι_1), f a (g a))
have Adj : ∀ (x x_1 : V), Adj (⨅ (a : ι_1), ⨆ (b : κ a), f a b) x x_1 ↔ Adj (⨆ (g : (a : ι_1) → κ a), ⨅ (a : ι_1), f a (g a)) x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u_2
G_1 : Digraph V
a b : V
inst : IsEmpty V
G : Digraph V
⊢ G = ⊥
have Adj : G.Adj = Adj ⊥
Tactic: ext1
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u_2
G : Digraph V
a b : V
inst : Nonempty V
⊢ Nontrivial.{u_2} (Digraph V)
have h : Ne.{u_2 + 1} (α := Digraph V) ⊥ ⊤
Tactic: use ⊥, ⊤
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Basic (goal)
Goal:
ι : Sort u_1
V : Type u_2
G : Digraph V
a b : V
inst : Nonempty V
⊢ Ne.{u_2 + 1} (α := Digraph V) ⊥ ⊤
have h : ∀ (v : V), Ne.{u_2 + 1} (α := Digraph V) ⊥ ⊤
Tactic: have v := Classical.arbitrary V
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Orientation (goal)
Goal:
V : Type u_1
⊢ Eq.{u_1 + 1} (α := SimpleGraph V) (toSimpleGraphInclusive ⊤) ⊤
have Adj : ∀ (x x_1 : V), SimpleGraph.Adj (toSimpleGraphInclusive ⊤) x x_1 ↔ SimpleGraph.Adj ⊤ x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Orientation (goal)
Goal:
V : Type u_1
⊢ Eq.{u_1 + 1} (α := SimpleGraph V) (toSimpleGraphStrict ⊤) ⊤
have Adj : ∀ (x x_1 : V), SimpleGraph.Adj (toSimpleGraphStrict ⊤) x x_1 ↔ SimpleGraph.Adj ⊤ x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Orientation (goal)
Goal:
V : Type u_1
⊢ Eq.{u_1 + 1} (α := SimpleGraph V) (toSimpleGraphInclusive ⊥) ⊥
have Adj : ∀ (x x_1 : V), SimpleGraph.Adj (toSimpleGraphInclusive ⊥) x x_1 ↔ SimpleGraph.Adj ⊥ x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Orientation (goal)
Goal:
V : Type u_1
x x_1 : V
h_1 : SimpleGraph.Adj (toSimpleGraphInclusive ⊥) x x_1
left : x ≠ x_1
h : Adj ⊥ x x_1 ∨ Adj ⊥ x_1 x
⊢ SimpleGraph.Adj ⊥ x x_1
have inl : ∀ (h : Adj ⊥ x x_1), SimpleGraph.Adj ⊥ x x_1
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Orientation (goal)
Goal:
V : Type u_1
x x_1 : V
h_1 : SimpleGraph.Adj (toSimpleGraphInclusive ⊥) x x_1
left : x ≠ x_1
h : Adj ⊥ x x_1 ∨ Adj ⊥ x_1 x
inl : ∀ (h : Adj ⊥ x x_1), SimpleGraph.Adj ⊥ x x_1
⊢ SimpleGraph.Adj ⊥ x x_1
have inr : ∀ (h : Adj ⊥ x_1 x), SimpleGraph.Adj ⊥ x x_1
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Orientation (goal)
Goal:
V : Type u_1
⊢ Eq.{u_1 + 1} (α := SimpleGraph V) (toSimpleGraphStrict ⊥) ⊥
have Adj : ∀ (x x_1 : V), SimpleGraph.Adj (toSimpleGraphStrict ⊥) x x_1 ↔ SimpleGraph.Adj ⊥ x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Orientation (hypothesis)
Goal:
V : Type u_1
x x_1 : V
h_1 : SimpleGraph.Adj (toSimpleGraphStrict ⊥) x x_1
left : x ≠ x_1
h : Adj ⊥ x x_1 ∧ Adj ⊥ x_1 x
⊢ SimpleGraph.Adj ⊥ x x_1
have left : Adj ⊥ x x_1
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Digraph.Orientation (hypothesis)
Goal:
V : Type u_1
x x_1 : V
h_1 : SimpleGraph.Adj (toSimpleGraphStrict ⊥) x x_1
left_1 : x ≠ x_1
h : Adj ⊥ x x_1 ∧ Adj ⊥ x_1 x
left : Adj ⊥ x x_1
⊢ SimpleGraph.Adj ⊥ x x_1
have right : Adj ⊥ x_1 x
Tactic: tauto
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ x ! ^ (c + 1) * (c + 1)! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1) =
    x ! * (c + 1) * x ! ^ c * c ! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1)
have rw : x ! ^ c * x ! * ((c + 1) * c !) * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1) =
  x ! * (c + 1) * x ! ^ c * c ! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1)
Tactic: rw [factorial_succ, pow_succ]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ x ! * (c + 1) * x ! ^ c * c ! * ∏ j ∈ Finset.range (c + 1), (j * 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)
have rw : 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: rw [Finset.prod_range_succ]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (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 !
have 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 !
Tactic: rw [bell_mul_eq_lemma hx]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (c + 1) * (c * x + x - 1).choose (x - 1) * (x * c)! * x ! = (x * (c + 1))!
have rw : (x * c + x)! = (x * (c + 1))!
Tactic: rw [← Nat.choose_mul_add hx, mul_comm c x, Nat.add_choose_mul_factorial_mul_factorial]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
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)) *
        prod (map (fun (j : ℕ) ↦ j !) m) *
      ∏ j ∈ m.toFinset.erase 0, (count j m)! =
    m.sum !
have 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 !
Tactic: rw [← Nat.mul_right_inj (a := ∏ i ∈ m.toFinset, (i * count i m)!) (by positivity)]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
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)) *
          prod (map (fun (j : ℕ) ↦ j !) m) *
        ∏ j ∈ m.toFinset.erase 0, (count j m)!) =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !
have 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 !
Tactic: simp only [← mul_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
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)) *
        prod (map (fun (j : ℕ) ↦ j !) m) *
      ∏ j ∈ m.toFinset.erase 0, (count j m)! =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !
have 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 !
Tactic: rw [Nat.multinomial_spec]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
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)) *
        prod (map (fun (j : ℕ) ↦ j !) m) *
      ∏ j ∈ m.toFinset.erase 0, (count j m)! =
    (∏ i ∈ m.toFinset, (i * count i m)!) * m.sum !
have 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 !
Tactic: simp only [mul_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
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)) *
        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 !
have 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 !
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m : Multiset ℕ
⊢ (∏ 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 !
have 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)!
Tactic: apply congr_arg₂
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
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)!
⊢ (∏ 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 !
have hy : (∑ i ∈ m.toFinset, i * count i m)! = m.sum !
Tactic: apply congr_arg₂
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m : Multiset ℕ
⊢ (∏ 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)!
have 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)!
Tactic: rw [mul_comm, mul_assoc, ← Finset.prod_mul_distrib, Finset.prod_multiset_map_count]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
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)!
⊢ 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)!
have 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)!
Tactic: by_cases hm : 0 ∈ m.toFinset
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
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)!
⊢ 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)!
have 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)!
Tactic: by_cases hm : 0 ∈ m.toFinset
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
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, 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)!
have 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)!
Tactic: rw [← Finset.prod_erase_mul _ _ hm]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
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
⊢ (∏ 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)!
have 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)!
Tactic: rw [← Finset.prod_erase_mul _ _ hm]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
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, 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)!
have 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)!
Tactic: nth_rewrite 1 [← Finset.erase_eq_of_notMem hm]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m : Multiset ℕ
⊢ 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)!
have 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)!
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
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m : Multiset ℕ
⊢ 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)!
have 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)!)
Tactic: rw [← Finset.prod_mul_distrib]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m : Multiset ℕ
⊢ 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)!)
have 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: apply Finset.prod_congr rfl
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
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)!
have hx₁ : x ≠ 0
Tactic: rw [← mul_assoc, bell_mul_eq_lemma]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (hypothesis)
Goal:
m : Multiset ℕ
x : ℕ
hx : x ∈ m.toFinset.erase 0
⊢ x ≠ 0
have hx₁ : ¬x = 0 ∧ x ∈ m
Tactic: simp only [Finset.mem_erase, ne_eq, mem_toFinset] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m : Multiset ℕ
⊢ (∑ i ∈ m.toFinset, i * count i m)! = m.sum !
have hy : ∑ i ∈ m.toFinset, i * count i m = m.sum
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m : Multiset ℕ
⊢ ∑ i ∈ m.toFinset, i * count i m = m.sum
have hy : Eq (α := ℕ) (∑ i ∈ m.toFinset, i * count i m) (∑ m_1 ∈ m.toFinset, count m_1 m • m_1)
Tactic: rw [Finset.sum_multiset_count]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m : Multiset ℕ
⊢ m.bell = m.sum ! / HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!)
have rw : m.bell * HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!) = m.sum !
Tactic: rw [← Nat.mul_left_inj, Nat.div_mul_cancel _]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m : Multiset ℕ
rw : m.bell * HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!) = m.sum !
⊢ m.bell = m.sum ! / HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!)
have rw₁ : HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!) ∣ m.sum !
Tactic: rw [← Nat.mul_left_inj, Nat.div_mul_cancel _]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
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 !
⊢ m.bell = m.sum ! / HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!)
have rw₂ : HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!) ≠ 0
Tactic: rw [← Nat.mul_left_inj, Nat.div_mul_cancel _]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m : Multiset ℕ
⊢ m.bell * HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!) = m.sum !
have rw : m.bell * prod (map (fun (j : ℕ) ↦ j !) m) * ∏ j ∈ m.toFinset.erase 0, (count j m)! = m.sum !
Tactic: rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m : Multiset ℕ
⊢ HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!) ∣ m.sum !
have 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)!)
Tactic: rw [← bell_mul_eq, mul_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m : Multiset ℕ
⊢ HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!) ≠ 0
have rw : 0 < HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!)
Tactic: rw [← Nat.pos_iff_ne_zero]