awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
a : ∑ a ∈ s.inf fun (i : ι) ↦ (S i)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
⊢ Eq.{u_3 + 1} (α := G) (∑ a ∈ s.inf fun (i : ι) ↦ (S i)ᶜ, f a)
    (∑ t ∈ s.powerset, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a))
have a₁ : HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a) =
  HAdd.hAdd (α := G)
    (∑ t ∈ s.powerset with ¬t.Nonempty, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a))
    (∑ t ∈ s.powerset with t.Nonempty, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a))
Tactic: calc
    ∑ a ∈ s.inf fun i ↦ (S i)ᶜ, f a
      = ∑ a, f a - ∑ a ∈ s.biUnion S, f a := by
      rw [← Finset.compl_sup, sup_eq_biUnion, eq_sub_iff_add_eq, sum_compl_add_sum]
    _ = ∑ t ∈ s.powerset.filter (¬ ·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a
          + ∑ t ∈ s.powerset.filter (·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a := by
      simp [← sum_attach (filter ..), inclusion_exclusion_sum_biUnion, inf'_eq_inf, filter_eq',
        sub_eq_add_neg, pow_succ]
    _ = ∑ t ∈ s.powerset, (-1) ^ #t • ∑ a ∈ t.inf S, f a := sum_filter_not_add_sum_filter ..
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ Eq.{u_3 + 1} (α := G) (∑ a ∈ s.inf fun (i : ι) ↦ (S i)ᶜ, f a)
    (∑ t ∈ s.powerset, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a))
have a : ∑ a ∈ s.inf fun (i : ι) ↦ (S i)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
Tactic: classical
  calc
    ∑ a ∈ s.inf fun i ↦ (S i)ᶜ, f a
      = ∑ a, f a - ∑ a ∈ s.biUnion S, f a := by
      rw [← Finset.compl_sup, sup_eq_biUnion, eq_sub_iff_add_eq, sum_compl_add_sum]
    _ = ∑ t ∈ s.powerset.filter (¬ ·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a
          + ∑ t ∈ s.powerset.filter (·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a := by
      simp [← sum_attach (filter ..), inclusion_exclusion_sum_biUnion, inf'_eq_inf, filter_eq',
        sub_eq_add_neg, pow_succ]
    _ = ∑ t ∈ s.powerset, (-1) ^ #t • ∑ a ∈ t.inf S, f a := sum_filter_not_add_sum_filter ..
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
a : ∑ a ∈ s.inf fun (i : ι) ↦ (S i)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
⊢ Eq.{u_3 + 1} (α := G) (∑ a ∈ s.inf fun (i : ι) ↦ (S i)ᶜ, f a)
    (∑ t ∈ s.powerset, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a))
have a₁ : HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a) =
  HAdd.hAdd (α := G)
    (∑ t ∈ s.powerset with ¬t.Nonempty, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a))
    (∑ t ∈ s.powerset with t.Nonempty, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a))
Tactic: classical
  calc
    ∑ a ∈ s.inf fun i ↦ (S i)ᶜ, f a
      = ∑ a, f a - ∑ a ∈ s.biUnion S, f a := by
      rw [← Finset.compl_sup, sup_eq_biUnion, eq_sub_iff_add_eq, sum_compl_add_sum]
    _ = ∑ t ∈ s.powerset.filter (¬ ·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a
          + ∑ t ∈ s.powerset.filter (·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a := by
      simp [← sum_attach (filter ..), inclusion_exclusion_sum_biUnion, inf'_eq_inf, filter_eq',
        sub_eq_add_neg, pow_succ]
    _ = ∑ t ∈ s.powerset, (-1) ^ #t • ∑ a ∈ t.inf S, f a := sum_filter_not_add_sum_filter ..
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
c : Composition n
⊢ (↑c.blocks : Multiset ℕ).sum = n
have rw : c.blocks.sum = n
Tactic: rw [Multiset.sum_coe, c.blocks_sum]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
c : Composition n
rw : c.blocks.sum = n
⊢ (↑c.blocks : Multiset ℕ).sum = n
have rw₁ : n = n
Tactic: rw [Multiset.sum_coe, c.blocks_sum]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
b : Multiset ℕ
hb₁ : ∀ {i : ℕ}, i ∈ b → 0 < i
hb₂ : b.sum = n
⊢ ∃ (a : Composition n), ofComposition n a = { parts := b, parts_pos := @hb₁, parts_sum := hb₂ }
have h : ∀ (b : List ℕ) (hb₁ : ∀ {i : ℕ}, i ∈ ⟦b⟧ → 0 < i) (hb₂ : sum ⟦b⟧ = n),
  ∃ (a : Composition n), ofComposition n a = { parts := ⟦b⟧, parts_pos := @hb₁, parts_sum := hb₂ }
Tactic: induction b using Quotient.inductionOn with | _ b => ?_
Cleared hypotheses: b, hb₁, hb₂
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (hypothesis)
Goal:
n : ℕ
l : Multiset ℕ
hl : l.sum = n
⊢ (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
have lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0
Tactic: have lz : (l.filter (· = 0)).sum = 0 := by simp [sum_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
l : Multiset ℕ
hl : l.sum = n
lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0
⊢ (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
have rwa : ∀ (hl : (filter (fun (x : ℕ) ↦ x = 0) l + filter (fun (a : ℕ) ↦ ¬a = 0) l).sum = n)
  (lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0), (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
Tactic: rwa [← filter_add_not (· = 0) l, sum_add, lz, zero_add] at hl
Cleared hypotheses: hl, lz
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
l : Multiset ℕ
hl : l.sum = n
lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0
rwa :
  ∀ (hl : (filter (fun (x : ℕ) ↦ x = 0) l + filter (fun (a : ℕ) ↦ ¬a = 0) l).sum = n)
    (lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0), (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
⊢ (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
have rwa₁ : ∀ (hl : (filter (fun (x : ℕ) ↦ x = 0) l).sum + (filter (fun (a : ℕ) ↦ ¬a = 0) l).sum = n)
  (lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0), (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
Tactic: rwa [← filter_add_not (· = 0) l, sum_add, lz, zero_add] at hl
Cleared hypotheses: hl, lz
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
l : Multiset ℕ
hl : l.sum = n
lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0
rwa :
  ∀ (hl : (filter (fun (x : ℕ) ↦ x = 0) l + filter (fun (a : ℕ) ↦ ¬a = 0) l).sum = n)
    (lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0), (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
rwa₁ :
  ∀ (hl : (filter (fun (x : ℕ) ↦ x = 0) l).sum + (filter (fun (a : ℕ) ↦ ¬a = 0) l).sum = n)
    (lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0), (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
⊢ (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
have rwa₂ : ∀ (hl : 0 + (filter (fun (a : ℕ) ↦ ¬a = 0) l).sum = n) (lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0),
  (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
Tactic: rwa [← filter_add_not (· = 0) l, sum_add, lz, zero_add] at hl
Cleared hypotheses: hl, lz
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
l : Multiset ℕ
hl : l.sum = n
lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0
rwa :
  ∀ (hl : (filter (fun (x : ℕ) ↦ x = 0) l + filter (fun (a : ℕ) ↦ ¬a = 0) l).sum = n)
    (lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0), (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
rwa₁ :
  ∀ (hl : (filter (fun (x : ℕ) ↦ x = 0) l).sum + (filter (fun (a : ℕ) ↦ ¬a = 0) l).sum = n)
    (lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0), (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
rwa₂ :
  ∀ (hl : 0 + (filter (fun (a : ℕ) ↦ ¬a = 0) l).sum = n) (lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0),
    (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
⊢ (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
have rwa₃ : ∀ (hl : (filter (fun (a : ℕ) ↦ ¬a = 0) l).sum = n) (lz : (filter (fun (x : ℕ) ↦ x = 0) l).sum = 0),
  (filter (fun (x : ℕ) ↦ x ≠ 0) l).sum = n
Tactic: rwa [← filter_add_not (· = 0) l, sum_add, lz, zero_add] at hl
Cleared hypotheses: hl, lz
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
σ : Type u_1
s : Sym σ n
inst : DecidableEq σ
⊢ sum (map (fun (a : σ) ↦ count a (↑s : Multiset σ)) (↑s : Multiset σ).dedup) = n
have change : ∑ a ∈ (↑s : Multiset σ).toFinset, count a (↑s : Multiset σ) = n
Tactic: change ∑ a ∈ s.1.toFinset, count a s.1 = n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
σ : Type u_1
s : Sym σ n
inst : DecidableEq σ
⊢ ∑ a ∈ (↑s : Multiset σ).toFinset, count a (↑s : Multiset σ) = n
have rw : (↑s : Multiset σ).card = n
Tactic: rw [toFinset_sum_count_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ ofSym.{u_2} (σ := τ) (Sym.map (⇑e : (a : σ) → τ) s) = ofSym s
have simp : Eq (α := Multiset ℕ)
  (map (fun (x : τ) ↦ count x (map (⇑e : (a : σ) → τ) (↑s : Multiset σ)))
    (dedup (map (⇑e : (a : σ) → τ) (↑s : Multiset σ))))
  (map (fun (x : σ) ↦ count x (↑s : Multiset σ)) (↑s : Multiset σ).dedup)
Tactic: simp only [ofSym, Sym.val_eq_coe, Sym.coe_map, mk.injEq]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ Eq (α := Multiset ℕ)
    (map (fun (x : τ) ↦ count x (map (⇑e : (a : σ) → τ) (↑s : Multiset σ)))
      (dedup (map (⇑e : (a : σ) → τ) (↑s : Multiset σ))))
    (map (fun (x : σ) ↦ count x (↑s : Multiset σ)) (↑s : Multiset σ).dedup)
have rw : Eq (α := Multiset ℕ)
  (map (fun (x : τ) ↦ count x (map (⇑e : (a : σ) → τ) (↑s : Multiset σ)))
    (map (⇑e : (a : σ) → τ) (↑s : Multiset σ).dedup))
  (map (fun (x : σ) ↦ count x (↑s : Multiset σ)) (↑s : Multiset σ).dedup)
Tactic: rw [Multiset.dedup_map_of_injective e.injective]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ Eq (α := Multiset ℕ)
    (map (fun (x : τ) ↦ count x (map (⇑e : (a : σ) → τ) (↑s : Multiset σ)))
      (map (⇑e : (a : σ) → τ) (↑s : Multiset σ).dedup))
    (map (fun (x : σ) ↦ count x (↑s : Multiset σ)) (↑s : Multiset σ).dedup)
have simp : Eq (α := Multiset ℕ)
  (map
    (fun (x : σ) ↦
      count.{u_2} (α := τ) ((e : (a : σ) → τ) x : τ) (map (⇑e : (a : σ) → τ) (↑s : Multiset σ) : Multiset τ))
    (↑s : Multiset σ).dedup)
  (map (fun (x : σ) ↦ count x (↑s : Multiset σ)) (↑s : Multiset σ).dedup)
Tactic: simp only [map_map, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ Eq (α := Multiset ℕ)
    (map
      (fun (x : σ) ↦
        count.{u_2} (α := τ) ((e : (a : σ) → τ) x : τ) (map (⇑e : (a : σ) → τ) (↑s : Multiset σ) : Multiset τ))
      (↑s : Multiset σ).dedup)
    (map (fun (x : σ) ↦ count x (↑s : Multiset σ)) (↑s : Multiset σ).dedup)
have e_f : Eq.{u_1 + 1} (α := σ → ℕ)
  (fun (x : σ) ↦ count.{u_2} (α := τ) ((e : (a : σ) → τ) x : τ) (map (⇑e : (a : σ) → τ) (↑s : Multiset σ) : Multiset τ))
  fun (x : σ) ↦ count x (↑s : Multiset σ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ Eq.{u_1 + 1} (α := σ → ℕ)
    (fun (x : σ) ↦
      count.{u_2} (α := τ) ((e : (a : σ) → τ) x : τ) (map (⇑e : (a : σ) → τ) (↑s : Multiset σ) : Multiset τ))
    fun (x : σ) ↦ count x (↑s : Multiset σ)
have e_f : ∀ (i : σ),
  count.{u_2} (α := τ) ((e : (a : σ) → τ) i : τ) (map (⇑e : (a : σ) → τ) (↑s : Multiset σ) : Multiset τ) =
    count i (↑s : Multiset σ)
Tactic: funext i
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
i : σ
⊢ count.{u_2} (α := τ) ((e : (a : σ) → τ) i : τ) (map (⇑e : (a : σ) → τ) (↑s : Multiset σ) : Multiset τ) =
    count i (↑s : Multiset σ)
have e_f : count.{u_2} (α := τ) ((e : (a : σ) → τ) i : τ) (map (⇑e : (a : σ) → τ) (↑s : Multiset σ) : Multiset τ) =
  count.{u_2} (α := τ) ((e : (a : σ) → τ) i : τ) (map (⇑e : (a : σ) → τ) (↑s : Multiset σ) : Multiset τ)
Tactic: rw [← Multiset.count_map_eq_count' e _ e.injective]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n_1 : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
n : ℕ
p : n.Partition
m : ℕ
⊢ m ∈ p.parts.toFinset ↔ count m p.parts * m ≠ 0
have suffices : m ∈ p.parts → m ≠ 0
Tactic: suffices m ∈ p.parts → m ≠ 0 by simpa
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (hypothesis)
Goal:
n : ℕ
p q : n.Partition
h :
  Eq (α := ℕ →₀ ℕ)
    ((fun (p : n.Partition) ↦
        ({ support := p.parts.toFinset, toFun := fun (m : ℕ) ↦ count m p.parts * m, mem_support_toFun := ⋯ } : ℕ →₀ ℕ))
      p)
    ((fun (p : n.Partition) ↦
        ({ support := p.parts.toFinset, toFun := fun (m : ℕ) ↦ count m p.parts * m, mem_support_toFun := ⋯ } : ℕ →₀ ℕ))
      q)
⊢ p = q
have h₁ : p.parts.toFinset = q.parts.toFinset ∧
  Eq (α := ℕ → ℕ) (fun (m : ℕ) ↦ count m p.parts * m) fun (m : ℕ) ↦ count m q.parts * m
Tactic: rw [Finsupp.mk.injEq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (hypothesis)
Goal:
n : ℕ
p q : n.Partition
h :
  p.parts.toFinset = q.parts.toFinset ∧
    Eq (α := ℕ → ℕ) (fun (m : ℕ) ↦ count m p.parts * m) fun (m : ℕ) ↦ count m q.parts * m
⊢ p = q
have hfinset : p.parts.toFinset = q.parts.toFinset
Tactic: obtain ⟨hfinset, hcount⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (hypothesis)
Goal:
n : ℕ
p q : n.Partition
h :
  p.parts.toFinset = q.parts.toFinset ∧
    Eq (α := ℕ → ℕ) (fun (m : ℕ) ↦ count m p.parts * m) fun (m : ℕ) ↦ count m q.parts * m
hfinset : p.parts.toFinset = q.parts.toFinset
⊢ p = q
have hcount : Eq (α := ℕ → ℕ) (fun (m : ℕ) ↦ count m p.parts * m) fun (m : ℕ) ↦ count m q.parts * m
Tactic: obtain ⟨hfinset, hcount⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
p q : n.Partition
hfinset : p.parts.toFinset = q.parts.toFinset
hcount : Eq (α := ℕ → ℕ) (fun (m : ℕ) ↦ count m p.parts * m) fun (m : ℕ) ↦ count m q.parts * m
⊢ p = q
have rw : ∀ (a : ℕ), count a p.parts = count a q.parts
Tactic: rw [Nat.Partition.ext_iff, Multiset.ext]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
p q : n.Partition
hfinset : p.parts.toFinset = q.parts.toFinset
hcount : Eq (α := ℕ → ℕ) (fun (m : ℕ) ↦ count m p.parts * m) fun (m : ℕ) ↦ count m q.parts * m
m : ℕ
⊢ count m p.parts = count m q.parts
have inl : count 0 p.parts = count 0 q.parts
Tactic: obtain rfl | h0 := Nat.eq_zero_or_pos m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
p q : n.Partition
hfinset : p.parts.toFinset = q.parts.toFinset
hcount : Eq (α := ℕ → ℕ) (fun (m : ℕ) ↦ count m p.parts * m) fun (m : ℕ) ↦ count m q.parts * m
m : ℕ
inl : count 0 p.parts = count 0 q.parts
⊢ count m p.parts = count m q.parts
have inr : ∀ (h0 : m > 0), count m p.parts = count m q.parts
Tactic: obtain rfl | h0 := Nat.eq_zero_or_pos m
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (hypothesis)
Goal:
n : ℕ
p : n.Partition
⊢ Membership.mem (γ := Finset (ℕ →₀ ℕ)) ((Finset.Icc 1 n).finsuppAntidiag n) p.toFinsuppAntidiag
have hp : p.parts.toFinset ⊆ Finset.Icc 1 n
Tactic: have hp : p.parts.toFinset ⊆ Finset.Icc 1 n := by
    grind
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
⊢ Membership.mem (γ := Finset (ℕ →₀ ℕ)) ((Finset.Icc 1 n).finsuppAntidiag n) p.toFinsuppAntidiag
have suffices : ∑ m ∈ Finset.Icc 1 n, count m p.parts * m = n
Tactic: suffices ∑ m ∈ Finset.Icc 1 n, Multiset.count m p.parts * m = n by simpa [toFinsuppAntidiag, hp]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
⊢ ∑ m ∈ Finset.Icc 1 n, count m p.parts * m = n
have h : p.parts.sum = ∑ m ∈ Finset.Icc 1 n, count m p.parts * m
Tactic: convert! ← p.parts_sum
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
⊢ p.parts.sum = ∑ m ∈ Finset.Icc 1 n, count m p.parts * m
have h : Eq (α := ℕ) (∑ m ∈ p.parts.toFinset, count m p.parts • m) (∑ m ∈ Finset.Icc 1 n, count m p.parts * m)
Tactic: rw [Finset.sum_multiset_count]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
⊢ Eq (α := ℕ) (∑ m ∈ p.parts.toFinset, count m p.parts • m) (∑ m ∈ Finset.Icc 1 n, count m p.parts * m)
have h : ∀ x ∈ Finset.Icc 1 n, x ∉ p.parts.toFinset → count x p.parts • x = 0
Tactic: apply Finset.sum_subset hp
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
⊢ ∀ x ∈ Finset.Icc 1 n, x ∉ p.parts.toFinset → count x p.parts • x = 0
have h : ∀ (x : ℕ), 1 ≤ x → x ≤ n → x ∉ p.parts → x ∉ p.parts ∨ x = 0
Tactic: suffices ∀ (x : ℕ), 1 ≤ x → x ≤ n → x ∉ p.parts → x ∉ p.parts ∨ x = 0 by simpa
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (hypothesis)
Goal:
p : Partition 1
⊢ p.parts = {1}
have h : p.parts = replicate p.parts.card 1
Tactic: have h : p.parts = replicate (card p.parts) 1 := eq_replicate_card.2 fun x hx =>
    ((le_sum_of_mem hx).trans_eq p.parts_sum).antisymm (p.parts_pos hx)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (hypothesis)
Goal:
p : Partition 1
h : p.parts = replicate p.parts.card 1
⊢ p.parts = {1}
have h' : p.parts.card = 1
Tactic: have h' : card p.parts = 1 := by simpa using (congrArg sum h.symm).trans p.parts_sum
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
p : Partition 1
h : p.parts = replicate p.parts.card 1
h' : p.parts.card = 1
⊢ p.parts = {1}
have rw : Eq (α := Multiset ℕ) (replicate p.parts.card 1) {1}
Tactic: rw [h, h', replicate_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
p : Partition 1
h : p.parts = replicate p.parts.card 1
h' : p.parts.card = 1
rw : Eq (α := Multiset ℕ) (replicate p.parts.card 1) {1}
⊢ p.parts = {1}
have rw₁ : Eq (α := Multiset ℕ) (replicate 1 1) {1}
Tactic: rw [h, h', replicate_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
p : Partition 1
h : p.parts = replicate p.parts.card 1
h' : p.parts.card = 1
rw : Eq (α := Multiset ℕ) (replicate p.parts.card 1) {1}
rw₁ : Eq (α := Multiset ℕ) (replicate 1 1) {1}
⊢ p.parts = {1}
have rw₂ : Eq (α := Multiset ℕ) {1} {1}
Tactic: rw [h, h', replicate_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
σ : Type u_1
inst : DecidableEq σ
s : Sym σ 1
⊢ ofSym s = indiscrete 1
have parts : ∀ (a : ℕ), count a (ofSym s).parts = count a (parts (n := 1) (indiscrete 1))
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
⊢ countRestricted n 2 = distincts n
have congrm : ∀ (x : n.Partition), (∀ i ∈ x.parts, count i x.parts < 2) ↔ x.parts.Nodup
Tactic: congrm Finset.univ.filter fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Basic (goal)
Goal:
n : ℕ
x : n.Partition
⊢ (∀ i ∈ x.parts, count i x.parts < 2) ↔ x.parts.Nodup
have rw : (∀ i ∈ x.parts, count i x.parts < 2) ↔ ∀ (a : ℕ), count a x.parts ≤ 1
Tactic: rw [Multiset.nodup_iff_count_le_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → ℕ → R
i : ℕ
⊢ Filter.Tendsto (β := ℕ∞) (fun (j : ℕ) ↦ (f (i + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))).order)
    Filter.atTop (nhds ⊤)
have refine : ∀ (n b : ℕ), b ≥ n → (↑n : ℕ∞) < (f (i + 1) (b + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (b + 1))).order
Tactic: refine ENat.tendsto_nhds_top_iff_natCast_lt.mpr (fun n ↦ Filter.eventually_atTop.mpr ⟨n, ?_⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : m ≥ n
⊢ (↑n : ℕ∞) < (f (i + 1) (m + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (m + 1))).order
have grw : (↑n : ℕ∞) <
  order.{u_1} (R := R) ((C : (a : R) → R⟦X⟧) (f (i + 1) (m + 1))) + (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (m + 1))).order
Tactic: grw [PowerSeries.smul_eq_C_mul, ← le_order_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : m ≥ n
⊢ (↑n : ℕ∞) <
    order.{u_1} (R := R) ((C : (a : R) → R⟦X⟧) (f (i + 1) (m + 1))) +
      (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (m + 1))).order
have refine : (↑n : ℕ∞) < (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (m + 1))).order
Tactic: refine lt_add_of_nonneg_of_lt (by simp) ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : m ≥ n
⊢ (↑n : ℕ∞) < (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (m + 1))).order
have a : Nontrivial R
Tactic: nontriviality R using Subsingleton.eq_zero
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : m ≥ n
h : Nontrivial R
⊢ (↑n : ℕ∞) < (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (m + 1))).order
have rw : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑((i + 1) * (m + 1)) : ℕ∞)
Tactic: rw [order_X_pow]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : m ≥ n
h : Nontrivial R
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑((i + 1) * (m + 1)) : ℕ∞)
have norm_cast : n < (i + 1) * (m + 1)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
f : ℕ → ℕ → R
i : ℕ
⊢ Summable.{u_1, 0} (α := R⟦X⟧) fun (j : ℕ) ↦ f (i + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))
have h : Filter.Tendsto (β := ℕ∞) (fun (i_1 : ℕ) ↦ (f (i + 1) (i_1 + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (i_1 + 1))).order)
  Filter.atTop (nhds ⊤)
Tactic: apply WithPiTopology.summable_of_tendsto_order_atTop_nhds_top
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
f : ℕ → ℕ → R
i : ℕ
hi : i ≠ 0
⊢ Summable.{u_1, 0} (α := R⟦X⟧) fun (j : ℕ) ↦ f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1))
have obtain : ∀ (a : ℕ) (hi : a + 1 ≠ 0),
  Summable.{u_1, 0} (α := R⟦X⟧) fun (j : ℕ) ↦ f (a + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((a + 1) * (j + 1))
Tactic: obtain ⟨a, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
hprod :
  ∀ i ∈ s,
    Ne (α := R)
      ((coeff ((g : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R)
          (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1)))) :
        R)
      (0 : R)
x : ℕ
⊢ x ∣ (g : (a : ℕ) → ℕ) x
have pos : ∀ (hx : x ∈ s), x ∣ (g : (a : ℕ) → ℕ) x
Tactic: by_cases hx : x ∈ s