awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
pos : ∀ (hx : x ∈ s), x ∣ (g : (a : ℕ) → ℕ) x
⊢ x ∣ (g : (a : ℕ) → ℕ) x
have neg : ∀ (hx : x ∉ s), x ∣ (g : (a : ℕ) → ℕ) x
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (hypothesis)
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 : ℕ
hx : x ∈ s
⊢ x ∣ (g : (a : ℕ) → ℕ) x
have hprod₁ : Ne (α := R)
  ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R)
      (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f x (j + 1) • HPow.hPow (α := R⟦X⟧) X (x * (j + 1)))) :
    R)
  (0 : R)
Tactic: specialize hprod x hx
Cleared hypotheses: hprod
-- 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
x : ℕ
hx : x ∈ s
hprod :
  Ne (α := R)
    ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R)
        (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f x (j + 1) • HPow.hPow (α := R⟦X⟧) X (x * (j + 1)))) :
      R)
    (0 : R)
⊢ x ∣ (g : (a : ℕ) → ℕ) x
have pos : ∀ (hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x),
  Eq (α := R)
    ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R)
        (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f x (j + 1) • HPow.hPow (α := R⟦X⟧) X (x * (j + 1)))) :
      R)
    (0 : R)
Tactic: contrapose hprod
Cleared hypotheses: hprod
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (hypothesis)
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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
⊢ Eq (α := R)
    ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R)
        (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f x (j + 1) • HPow.hPow (α := R⟦X⟧) X (x * (j + 1)))) :
      R)
    (0 : R)
have hx0 : x ≠ 0
Tactic: have hx0 : x ≠ 0 := fun h ↦ hs0 (h ▸ hx)
-- 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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
⊢ Eq (α := R)
    ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R)
        (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f x (j + 1) • HPow.hPow (α := R⟦X⟧) X (x * (j + 1)))) :
      R)
    (0 : R)
have pos : HAdd.hAdd (α := R) (β := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) 1 : R)
    (∑' (i : ℕ), (coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) (f x (i + 1) • HPow.hPow (α := R⟦X⟧) X (x * (i + 1))) :
      R) =
  0
Tactic: rw [map_add, (summable_genFun_term' f hx0).map_tsum _ (WithPiTopology.continuous_coeff _ _)]
-- 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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
⊢ HAdd.hAdd (α := R) (β := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) 1 : R)
      (∑' (i : ℕ),
          (coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) (f x (i + 1) • HPow.hPow (α := R⟦X⟧) X (x * (i + 1))) :
        R) =
    0
have pos : HAdd.hAdd (α := R) (β := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) 1 : R)
    (∑' (i : ℕ), (coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) (f x (i + 1) • HPow.hPow (α := R⟦X⟧) X (x * (i + 1))) :
      R) =
  HAdd.hAdd (α := R) 0 (∑' (i : ℕ), 0)
Tactic: rw [show (0 : R) = 0 + ∑' (i : ℕ), 0 by simp]
-- 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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
⊢ HAdd.hAdd (α := R) (β := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) 1 : R)
      (∑' (i : ℕ),
          (coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) (f x (i + 1) • HPow.hPow (α := R⟦X⟧) X (x * (i + 1))) :
        R) =
    HAdd.hAdd (α := R) 0 (∑' (i : ℕ), 0)
have pos : Eq.{u_1 + 1} (α := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) 1 : R) (0 : R)
Tactic: congrm (?_ + ∑' (i : ℕ), ?_)
-- 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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
pos : Eq.{u_1 + 1} (α := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) 1 : R) (0 : R)
⊢ HAdd.hAdd (α := R) (β := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) 1 : R)
      (∑' (i : ℕ),
          (coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) (f x (i + 1) • HPow.hPow (α := R⟦X⟧) X (x * (i + 1))) :
        R) =
    HAdd.hAdd (α := R) 0 (∑' (i : ℕ), 0)
have pos₁ : ∀ (i : ℕ),
  Eq (α := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) (f x (i + 1) • HPow.hPow (α := R⟦X⟧) X (x * (i + 1))) : R)
    (0 : R)
Tactic: congrm (?_ + ∑' (i : ℕ), ?_)
-- 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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
⊢ Eq.{u_1 + 1} (α := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) 1 : R) (0 : R)
have pos : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ)
Tactic: suffices g x ≠ 0 by simp [this]
-- 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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
⊢ Ne (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ)
have pos : ∀ (hprod : Eq (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ)), x ∣ (g : (a : ℕ) → ℕ) x
Tactic: contrapose hprod
Cleared hypotheses: hprod
-- 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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
i : ℕ
⊢ Eq (α := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) (f x (i + 1) • HPow.hPow (α := R⟦X⟧) X (x * (i + 1))) : R)
    (0 : R)
have pos : HSMul.hSMul (β := R) (f x (i + 1)) (if (g : (a : ℕ) → ℕ) x = x * (i + 1) then 1 else 0) = 0
Tactic: rw [map_smul, coeff_X_pow]
-- 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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
i : ℕ
⊢ HSMul.hSMul (β := R) (f x (i + 1)) (if (g : (a : ℕ) → ℕ) x = x * (i + 1) then 1 else 0) = 0
have pos : Eq.{u_1 + 1} (α := R) (if (g : (a : ℕ) → ℕ) x = x * (i + 1) then 1 else 0) 0
Tactic: apply smul_eq_zero_of_right
-- 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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
i : ℕ
⊢ Eq.{u_1 + 1} (α := R) (if (g : (a : ℕ) → ℕ) x = x * (i + 1) then 1 else 0) 0
have pos : (g : (a : ℕ) → ℕ) x ≠ x * (i + 1)
Tactic: suffices g x ≠ x * (i + 1) by simp [this]
-- 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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
i : ℕ
⊢ (g : (a : ℕ) → ℕ) x ≠ x * (i + 1)
have pos : ∀ (hprod : (g : (a : ℕ) → ℕ) x = x * (i + 1)), x ∣ (g : (a : ℕ) → ℕ) x
Tactic: contrapose hprod
Cleared hypotheses: hprod
-- 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 : ℕ
hx : x ∉ s
⊢ x ∣ (g : (a : ℕ) → ℕ) x
have neg : Eq (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ)
Tactic: suffices g x = 0 by simp [this]
-- 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 : ℕ
hx : x ∉ s
⊢ Eq (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ)
have neg : ∀ (hx : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ)), x ∈ s
Tactic: contrapose! hx
Cleared hypotheses: hx
-- 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
hg' : g ∉ Set.range (ι := d.Partition) toFinsuppAntidiag
this :
  ∃ i ∈ s,
    Eq (α := 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)
⊢ Eq.{u_1 + 1} (α := R)
    (∏ i ∈ s,
      (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)))))
    0
have obtain : ∀ (i : ℕ) (hi : i ∈ s)
  (hi' :
    Eq (α := 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)),
  Eq.{u_1 + 1} (α := R)
    (∏ i ∈ s,
      (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)))))
    0
Tactic: obtain ⟨i, hi, hi'⟩ := this
Cleared hypotheses: this
-- 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
hg' : g ∉ Set.range (ι := d.Partition) toFinsuppAntidiag
⊢ Eq.{u_1 + 1} (α := R)
    (∏ i ∈ s,
      (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)))))
    0
have suffices : ∃ i ∈ s,
  Eq (α := 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)
Tactic: suffices ∃ i ∈ s, (coeff (g i)) ((1 : R⟦X⟧) + ∑' j, f i (j + 1) • X ^ (i * (j + 1))) = 0 by
    obtain ⟨i, hi, hi'⟩ := this
    apply prod_eq_zero hi 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
hg' : g ∉ Set.range (ι := d.Partition) toFinsuppAntidiag
⊢ ∃ i ∈ s,
    Eq (α := 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)
have contrapose! : ∀
  (hprod :
    ∀ (i : ℕ) (_ : 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)),
  g ∈ Set.range (ι := d.Partition) toFinsuppAntidiag
Tactic: contrapose! hg' with hprod
Cleared hypotheses: hg'
-- 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 : ℕ) (_ : 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)
i : ℕ
⊢ Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ↔ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i
have refine_1 : ∀ (h : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ)), i ≠ 0
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, by grind⟩
-- 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 : ℕ) (_ : 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)
i : ℕ
refine_1 : ∀ (h : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ)), i ≠ 0
⊢ Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ↔ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i
have refine_2 : ∀ (h : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ)), i ≤ (g : (a : ℕ) → ℕ) i
Tactic: refine ⟨fun h ↦ ⟨?_, ?_⟩, by grind⟩
-- 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 : ℕ) (_ : 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)
i : ℕ
h : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ)
⊢ i ≠ 0
have refine_1 : ∀ (h : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ)), 0 ∈ s
Tactic: contrapose hs0 with rfl
Cleared hypotheses: hs0, i, h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (hypothesis)
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 : ℕ) (_ : 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)
⊢ ∃ (y : d.Partition), y.toFinsuppAntidiag = g
have hgne0 : ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ↔ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i
Tactic: have hgne0 (i : ℕ) : g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i := by
    refine ⟨fun h ↦ ⟨?_, ?_⟩, by grind⟩
    · contrapose hs0 with rfl
      exact mem_of_subset (mem_finsuppAntidiag.mp hg).2 (by simpa using h)
    · exact Nat.le_of_dvd (Nat.pos_of_ne_zero h) <| aux_dvd_of_coeff_ne_zero hs0 hg hprod _
-- 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 : ℕ) (_ : 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)
hgne0 : ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ↔ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i
⊢ ∃ (y : d.Partition), y.toFinsuppAntidiag = g
have refine_1 : ∀ (a : ℕ), a ∈ g.support ↔ Ne (α := ℕ) ((fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i) a) 0
Tactic: refine ⟨Nat.Partition.mk (Finsupp.mk g.support (fun i ↦ g i / i) ?_).toMultiset ?_ ?_, ?_⟩
-- 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 : ℕ) (_ : 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)
hgne0 : ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ↔ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i
refine_1 : ∀ (a : ℕ), a ∈ g.support ↔ Ne (α := ℕ) ((fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i) a) 0
⊢ ∃ (y : d.Partition), y.toFinsuppAntidiag = g
have refine_2 : ∀ {i : ℕ},
  Membership.mem (γ := Multiset ℕ)
      ((Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
          { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
            mem_support_toFun := sorry } :
        Multiset ℕ)
      i →
    0 < i
Tactic: refine ⟨Nat.Partition.mk (Finsupp.mk g.support (fun i ↦ g i / i) ?_).toMultiset ?_ ?_, ?_⟩
-- 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 : ℕ) (_ : 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)
hgne0 : ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ↔ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i
refine_1 : ∀ (a : ℕ), a ∈ g.support ↔ Ne (α := ℕ) ((fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i) a) 0
refine_2 :
  ∀ {i : ℕ},
    Membership.mem (γ := Multiset ℕ)
        ((Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
            { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
              mem_support_toFun := ⋯ } :
          Multiset ℕ)
        i →
      0 < i
⊢ ∃ (y : d.Partition), y.toFinsuppAntidiag = g
have refine_3 : Multiset.sum
    ((Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
      { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
        mem_support_toFun := sorry }) =
  d
Tactic: refine ⟨Nat.Partition.mk (Finsupp.mk g.support (fun i ↦ g i / i) ?_).toMultiset ?_ ?_, ?_⟩
-- 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 : ℕ) (_ : 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)
hgne0 : ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ↔ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i
refine_1 : ∀ (a : ℕ), a ∈ g.support ↔ Ne (α := ℕ) ((fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i) a) 0
refine_2 :
  ∀ {i : ℕ},
    Membership.mem (γ := Multiset ℕ)
        ((Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
            { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
              mem_support_toFun := ⋯ } :
          Multiset ℕ)
        i →
      0 < i
refine_3 :
  Multiset.sum
      ((Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
        { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
          mem_support_toFun := ⋯ }) =
    d
⊢ ∃ (y : d.Partition), y.toFinsuppAntidiag = g
have refine_4 : toFinsuppAntidiag (n := d)
    {
      parts :=
        (Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
          { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
            mem_support_toFun := sorry : ℕ →₀ ℕ },
      parts_pos := sorry, parts_sum := sorry : d.Partition } =
  g
Tactic: refine ⟨Nat.Partition.mk (Finsupp.mk g.support (fun i ↦ g i / i) ?_).toMultiset ?_ ?_, ?_⟩
-- 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 : ℕ) (_ : 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)
hgne0 : ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ↔ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i
⊢ ∀ {i : ℕ},
    Membership.mem (γ := Multiset ℕ)
        ((Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
            { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
              mem_support_toFun := ⋯ } :
          Multiset ℕ)
        i →
      0 < i
have refine_2 : ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) → i ≠ 0
Tactic: suffices ∀ i, g i ≠ 0 → i ≠ 0 by simpa [Nat.pos_iff_ne_zero]