awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
⊢ (∀ (d : Unit →₀ ℕ),
      Tendsto (β := R) (fun (i : ι) ↦ ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i) : R)) u
        (𝓝 ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) g) : Filter R)) ↔
    ∀ (d : ℕ),
      Tendsto (β := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) u
        (𝓝 ((coeff d : (a : R⟦X⟧) → R) g) : Filter R)
have apply : ∀ (a : Unit →₀ ℕ),
  Tendsto (β := R) (fun (i : ι) ↦ ((MvPowerSeries.coeff a : (a : MvPowerSeries Unit R) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff a : (a : MvPowerSeries Unit R) → R) g) : Filter R) ↔
    Tendsto (β := R)
      (fun (i : ι) ↦
        ((coeff
                ((LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ()) :
                    (a : Unit →₀ ℕ) → ℕ)
                  a) :
              (a : R⟦X⟧) → R)
            (f i) :
          R))
      u
      (𝓝
          ((coeff
                ((LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ()) :
                    (a : Unit →₀ ℕ) → ℕ)
                  a) :
              (a : R⟦X⟧) → R)
            g) :
        Filter R)
Tactic: apply (Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv.forall_congr
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ Tendsto (β := R) (fun (i : ι) ↦ ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) g) : Filter R) ↔
    Tendsto (β := R)
      (fun (i : ι) ↦
        ((coeff
                ((LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ()) :
                    (a : Unit →₀ ℕ) → ℕ)
                  d) :
              (a : R⟦X⟧) → R)
            (f i) :
          R))
      u
      (𝓝
          ((coeff
                ((LinearEquiv.toEquiv (modM := Finsupp.module Unit ℕ) (Finsupp.uniqueLinearEquiv ℕ ℕ ()) :
                    (a : Unit →₀ ℕ) → ℕ)
                  d) :
              (a : R⟦X⟧) → R)
            g) :
        Filter R)
have simp : Tendsto (β := R) (fun (i : ι) ↦ ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i) : R)) u
    (𝓝 ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) g) : Filter R) ↔
  Tendsto (β := R)
    (fun (i : ι) ↦ ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f i) : R)) u
    (𝓝 ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) g) : Filter R)
Tactic: simp only [LinearEquiv.coe_toEquiv, Finsupp.uniqueLinearEquiv_apply, coeff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ Tendsto (β := R) (fun (i : ι) ↦ ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) g) : Filter R) ↔
    Tendsto (β := R)
      (fun (i : ι) ↦ ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) g) : Filter R)
have a : Tendsto (β := R) (fun (i : ι) ↦ ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i) : R)) u
    (𝓝 ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) g) : Filter R) =
  Tendsto (β := R)
    (fun (i : ι) ↦ ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f i) : R)) u
    (𝓝 ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) g) : Filter R)
Tactic: apply iff_of_eq
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ Tendsto (β := R) (fun (i : ι) ↦ ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) g) : Filter R) =
    Tendsto (β := R)
      (fun (i : ι) ↦ ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) g) : Filter R)
have a : Eq (α := ι → R) (fun (i : ι) ↦ (MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i)) fun (i : ι) ↦
  (MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f i)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
a :
  Eq (α := ι → R) (fun (i : ι) ↦ (MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i)) fun (i : ι) ↦
    (MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f i)
⊢ Tendsto (β := R) (fun (i : ι) ↦ ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) g) : Filter R) =
    Tendsto (β := R)
      (fun (i : ι) ↦ ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f i) : R)) u
      (𝓝 ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) g) : Filter R)
have a₁ : d = Finsupp.single () ((d : (a : Unit) → ℕ) ())
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ Eq (α := ι → R) (fun (i : ι) ↦ (MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f i)) fun (i : ι) ↦
    (MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f i)
have a : ∀ (x : ι),
  Eq (α := R) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f x) : R)
    ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f x) : R)
Tactic: ext _
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
x : ι
⊢ Eq (α := R) ((MvPowerSeries.coeff d : (a : MvPowerSeries Unit R) → R) (f x) : R)
    ((MvPowerSeries.coeff (Finsupp.single () ((d : (a : Unit) → ℕ) ())) : (a : R⟦X⟧) → R) (f x) : R)
have a : d = Finsupp.single () ((d : (a : Unit) → ℕ) ())
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
x : ι
⊢ d = Finsupp.single () ((d : (a : Unit) → ℕ) ())
have a : Eq (α := ℕ) ((d : (a : Unit) → ℕ) default : ℕ)
  (((Finsupp.single () ((d : (a : Unit) → ℕ) ()) : Unit →₀ ℕ) : (a : Unit) → ℕ) default : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () ((d : (a : Unit) → ℕ) ())
have a : Eq (α := ℕ) ((d : (a : Unit) → ℕ) default : ℕ)
  (((Finsupp.single () ((d : (a : Unit) → ℕ) ()) : Unit →₀ ℕ) : (a : Unit) → ℕ) default : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : R⟦X⟧
⊢ Tendsto (fun (d : ℕ) ↦ (↑((trunc d : (a : R⟦X⟧) → Polynomial R) f) : R⟦X⟧)) atTop (𝓝 f)
have rw : ∀ (d : ℕ),
  Tendsto (β := R) (fun (i : ℕ) ↦ ((coeff d : (a : R⟦X⟧) → R) (↑((trunc i : (a : R⟦X⟧) → Polynomial R) f) : R⟦X⟧) : R))
    atTop (𝓝 ((coeff d : (a : R⟦X⟧) → R) f) : Filter R)
Tactic: rw [tendsto_iff_coeff_tendsto]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
g : R⟦X⟧
⊢ HasSum f g ↔
    ∀ (d : ℕ), HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) g : R)
have simp_rw : Tendsto (fun (s : Finset ι) ↦ ∑ b ∈ s, f b) (SummationFilter.unconditional ι).filter (𝓝 g) ↔
  ∀ (d : ℕ),
    Tendsto (β := R) (fun (s : Finset ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (∑ b ∈ s, f b) : R))
      (SummationFilter.unconditional ι).filter (𝓝 ((coeff d : (a : R⟦X⟧) → R) g) : Filter R)
Tactic: simp_rw [HasSum, ← map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
⊢ Summable f ↔ ∀ (d : ℕ), Summable.{u_1, u_2} (α := R) fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)
have simp_rw : (∃ (a : R⟦X⟧),
    ∀ (d : ℕ),
      HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) a : R)) ↔
  ∀ (d : ℕ), ∃ (a : R), HasSum (fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)) a
Tactic: simp_rw [Summable, hasSum_iff_hasSum_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
⊢ (∃ (a : R⟦X⟧),
      ∀ (d : ℕ),
        HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) a : R)) ↔
    ∀ (d : ℕ), ∃ (a : R), HasSum (fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)) a
have mp : (∃ (a : R⟦X⟧),
    ∀ (d : ℕ),
      HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) a : R)) →
  ∀ (d : ℕ), ∃ (a : R), HasSum (fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
mp :
  (∃ (a : R⟦X⟧),
      ∀ (d : ℕ),
        HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) a : R)) →
    ∀ (d : ℕ), ∃ (a : R), HasSum (fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)) a
⊢ (∃ (a : R⟦X⟧),
      ∀ (d : ℕ),
        HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) a : R)) ↔
    ∀ (d : ℕ), ∃ (a : R), HasSum (fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)) a
have mpr : (∀ (d : ℕ), ∃ (a : R), HasSum (fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)) a) →
  ∃ (a : R⟦X⟧),
    ∀ (d : ℕ), HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) a : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
h : ∀ (d : ℕ), ∃ (a : R), HasSum (fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)) a
⊢ ∃ (a : R⟦X⟧),
    ∀ (d : ℕ), HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) a : R)
have mpr : ∀ (a : (d : ℕ) → R) (h : ∀ (d : ℕ), HasSum (fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)) (a d)),
  ∃ (a : R⟦X⟧),
    ∀ (d : ℕ), HasSum (α := R) (fun (i : ι) ↦ ((coeff d : (a : R⟦X⟧) → R) (f i) : R)) ((coeff d : (a : R⟦X⟧) → R) a : R)
Tactic: choose a h using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
⊢ Summable f
have inl : ∀ (hempty : IsEmpty ι), Summable f
Tactic: rcases isEmpty_or_nonempty ι with hempty | hempty
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
inl : ∀ (hempty : IsEmpty ι), Summable f
⊢ Summable f
have inr : ∀ (hempty : Nonempty ι), Summable f
Tactic: rcases isEmpty_or_nonempty ι with hempty | hempty
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ Summable f
have inr : ∀ (d : ℕ), Summable.{u_1, u_2} (α := R) fun (i : ι) ↦ (coeff d : (a : R⟦X⟧) → R) (f i)
Tactic: rw [summable_iff_summable_coeff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (hypothesis)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
hempty : Nonempty ι
n : ℕ
⊢ Summable.{u_1, u_2} (α := R) fun (i : ι) ↦ (coeff n : (a : R⟦X⟧) → R) (f i)
have h₁ : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
Tactic: simp_rw [ENat.tendsto_nhds_top_iff_natCast_lt, Filter.eventually_atTop] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
⊢ Summable.{u_1, u_2} (α := R) fun (i : ι) ↦ (coeff n : (a : R⟦X⟧) → R) (f i)
have inr : ∀ (i : ι) (hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order),
  Summable.{u_1, u_2} (α := R) fun (i : ι) ↦ (coeff n : (a : R⟦X⟧) → R) (f i)
Tactic: obtain ⟨i, hi⟩ := h n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
⊢ Summable.{u_1, u_2} (α := R) fun (i : ι) ↦ (coeff n : (a : R⟦X⟧) → R) (f i)
have inr : (support.{u_2, u_1} (M := R) fun (i : ι) ↦ (coeff n : (a : R⟦X⟧) → R) (f i)) ⊆ Set.Iic i
Tactic: refine summable_of_hasFiniteSupport <| (Set.finite_Iic i).subset ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
⊢ (support.{u_2, u_1} (M := R) fun (i : ι) ↦ (coeff n : (a : R⟦X⟧) → R) (f i)) ⊆ Set.Iic i
have inr : ∀ (x : ι), Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) (f x) : R) (0 : R) → x ≤ i
Tactic: simp_rw [Function.support_subset_iff, Set.mem_Iic]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
k : ι
hk : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) (f k) : R) (0 : R)
⊢ k ≤ i
have inr : ∀ (hk : i < k), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f k) : R) (0 : R)
Tactic: contrapose! hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
⊢ Summable.{u_1, u_2} (α := R⟦X⟧) fun (x : Finset ι) ↦ ∏ i ∈ x, f i
have inl : ∀ (hempty : IsEmpty ι), Summable.{u_1, u_2} (α := R⟦X⟧) fun (x : Finset ι) ↦ ∏ i ∈ x, f i
Tactic: rcases isEmpty_or_nonempty ι with hempty | hempty
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
inl : ∀ (hempty : IsEmpty ι), Summable.{u_1, u_2} (α := R⟦X⟧) fun (x : Finset ι) ↦ ∏ i ∈ x, f i
⊢ Summable.{u_1, u_2} (α := R⟦X⟧) fun (x : Finset ι) ↦ ∏ i ∈ x, f i
have inr : ∀ (hempty : Nonempty ι), Summable.{u_1, u_2} (α := R⟦X⟧) fun (x : Finset ι) ↦ ∏ i ∈ x, f i
Tactic: rcases isEmpty_or_nonempty ι with hempty | hempty
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
hempty : Nonempty ι
⊢ Summable.{u_1, u_2} (α := R⟦X⟧) fun (x : Finset ι) ↦ ∏ i ∈ x, f i
have inr : ∀ (n : ℕ), HasFiniteSupport.{u_2, u_1} (M := R) fun (i : Finset ι) ↦ (coeff n : (a : R⟦X⟧) → R) (∏ i ∈ i, f i)
Tactic: refine (summable_iff_summable_coeff _).mpr fun n ↦ summable_of_hasFiniteSupport ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (hypothesis)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
h : Tendsto (β := ℕ∞) (fun (i : ι) ↦ (f i).order) atTop (𝓝 ⊤)
hempty : Nonempty ι
n : ℕ
⊢ HasFiniteSupport.{u_2, u_1} (M := R) fun (i : Finset ι) ↦ (coeff n : (a : R⟦X⟧) → R) (∏ i ∈ i, f i)
have h₁ : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
Tactic: simp_rw [ENat.tendsto_nhds_top_iff_natCast_lt, eventually_atTop] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
⊢ HasFiniteSupport.{u_2, u_1} (M := R) fun (i : Finset ι) ↦ (coeff n : (a : R⟦X⟧) → R) (∏ i ∈ i, f i)
have inr : ∀ (i : ι) (hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order),
  HasFiniteSupport.{u_2, u_1} (M := R) fun (i : Finset ι) ↦ (coeff n : (a : R⟦X⟧) → R) (∏ i ∈ i, f i)
Tactic: obtain ⟨i, hi⟩ := h n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
⊢ HasFiniteSupport.{u_2, u_1} (M := R) fun (i : Finset ι) ↦ (coeff n : (a : R⟦X⟧) → R) (∏ i ∈ i, f i)
have inr : (support.{u_2, u_1} (M := R) fun (i : Finset ι) ↦ (coeff n : (a : R⟦X⟧) → R) (∏ i ∈ i, f i)) ⊆
  (↑(Finset.Iio i).powerset : Set (Finset ι))
Tactic: apply (Finset.Iio i).powerset.finite_toSet.subset
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
⊢ (support.{u_2, u_1} (M := R) fun (i : Finset ι) ↦ (coeff n : (a : R⟦X⟧) → R) (∏ i ∈ i, f i)) ⊆
    (↑(Finset.Iio i).powerset : Set (Finset ι))
have inr : ∀ (s : Finset ι),
  Ne.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (∏ i ∈ s, f i) : R) (0 : R) → (↑s : Set ι) ⊆ Set.Iio i
Tactic: suffices ∀ s : Finset ι, coeff n (∏ i ∈ s, f i) ≠ 0 → ↑s ⊆ Set.Iio i by simpa
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
s : Finset ι
hs : Ne.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (∏ i ∈ s, f i) : R) (0 : R)
⊢ (↑s : Set ι) ⊆ Set.Iio i
have inr : ∀ (hs : ¬(↑s : Set ι) ⊆ Set.Iio i), Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (∏ i ∈ s, f i) : R) (0 : R)
Tactic: contrapose hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
s : Finset ι
hs : ¬(↑s : Set ι) ⊆ Set.Iio i
⊢ Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (∏ i ∈ s, f i) : R) (0 : R)
have inr : ∀ (x : ι) (hxs : x ∈ (↑s : Set ι)) (hxi : x ∉ Set.Iio i),
  Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (∏ i ∈ s, f i) : R) (0 : R)
Tactic: obtain ⟨x, hxs, hxi⟩ := Set.not_subset.mp hs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (hypothesis)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
s : Finset ι
hs : ¬(↑s : Set ι) ⊆ Set.Iio i
x : ι
hxs : x ∈ (↑s : Set ι)
hxi : x ∉ Set.Iio i
⊢ Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (∏ i ∈ s, f i) : R) (0 : R)
have hxi₁ : i ≤ x
Tactic: rw [Set.mem_Iio, not_lt] at hxi
Cleared hypotheses: hxi
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommSemiring R
ι : Type u_2
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ (a : ι), ∀ b ≥ a, (↑n : ℕ∞) < (f b).order
i : ι
hi : ∀ b ≥ i, (↑n : ℕ∞) < (f b).order
s : Finset ι
hs : ¬(↑s : Set ι) ⊆ Set.Iio i
x : ι
hxs : x ∈ (↑s : Set ι)
hxi : i ≤ x
⊢ Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (∏ i ∈ s, f i) : R) (0 : R)
have inr : (f x).order ≤ ∑ i ∈ s, (f i).order
Tactic: refine coeff_of_lt_order _ <| (hi x hxi).trans_le <| le_trans ?_ (le_order_prod _ _)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
⊢ Multipliable.{u_2, 0} (α := R⟦X⟧) fun (n : ℕ) ↦ 1 - HPow.hPow (α := R⟦X⟧) X (n + 1)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
h : Nontrivial R
⊢ Multipliable.{u_2, 0} (α := R⟦X⟧) fun (n : ℕ) ↦ 1 - HPow.hPow (α := R⟦X⟧) X (n + 1)
have simp_rw : Multipliable.{u_2, 0} (α := R⟦X⟧) fun (n : ℕ) ↦ 1 + -HPow.hPow (α := R⟦X⟧) X (n + 1)
Tactic: simp_rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
h : Nontrivial R
⊢ Multipliable.{u_2, 0} (α := R⟦X⟧) fun (n : ℕ) ↦ 1 + -HPow.hPow (α := R⟦X⟧) X (n + 1)
have h : Tendsto (β := ℕ∞) (fun (i : ℕ) ↦ (-HPow.hPow (α := R⟦X⟧) X (i + 1)).order) atTop (𝓝 ⊤)
Tactic: apply multipliable_one_add_of_tendsto_order_atTop_nhds_top
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.PiTopology (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
h : Nontrivial R
⊢ Tendsto (β := ℕ∞) (fun (i : ℕ) ↦ (-HPow.hPow (α := R⟦X⟧) X (i + 1)).order) atTop (𝓝 ⊤)
have h : ∀ (n b : ℕ), b ≥ n → (↑n : ℕ∞) < (-HPow.hPow (α := R⟦X⟧) X (b + 1)).order
Tactic: refine ENat.tendsto_nhds_top_iff_natCast_lt.mpr (fun n ↦ Filter.eventually_atTop.mpr ⟨n, ?_⟩)