awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
u : Filter ι
g : MvPowerSeries σ R
⊢ Tendsto f u (𝓝 g) ↔
    ∀ (d : σ →₀ ℕ),
      Tendsto.{u_3, u_2} (β := R) (fun (i : ι) ↦ ((coeff d : (a : MvPowerSeries σ R) → R) (f i) : R)) u
        (𝓝 ((coeff d : (a : MvPowerSeries σ R) → R) g) : Filter R)
have rw : (∀ (i : σ →₀ ℕ), Tendsto (fun (x : ι) ↦ f x i) u (𝓝 (g i))) ↔
  ∀ (d : σ →₀ ℕ),
    Tendsto.{u_3, u_2} (β := R) (fun (i : ι) ↦ ((coeff d : (a : MvPowerSeries σ R) → R) (f i) : R)) u
      (𝓝 ((coeff d : (a : MvPowerSeries σ R) → R) g) : Filter R)
Tactic: rw [nhds_pi, tendsto_pi]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : DecidableEq σ
inst_2 : CommSemiring R
f : MvPowerSeries σ R
⊢ Tendsto (fun (d : σ →₀ ℕ) ↦ (↑((trunc' R d : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R))
    atTop (𝓝 f)
have rw : ∀ (d : σ →₀ ℕ),
  Tendsto.{u_1, u_2} (β := R)
    (fun (i : σ →₀ ℕ) ↦
      ((coeff d : (a : MvPowerSeries σ R) → R)
          (↑((trunc' R i : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R) :
        R))
    atTop (𝓝 ((coeff d : (a : MvPowerSeries σ R) → R) f) : Filter R)
Tactic: rw [tendsto_iff_coeff_tendsto]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : DecidableEq σ
inst_2 : CommSemiring R
inst_3 : Nonempty σ
f : MvPowerSeries σ R
⊢ Tendsto (fun (d : σ →₀ ℕ) ↦ (↑((trunc R d : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R)) atTop
    (𝓝 f)
have rw : ∀ (d : σ →₀ ℕ),
  Tendsto.{u_1, u_2} (β := R)
    (fun (i : σ →₀ ℕ) ↦
      ((coeff d : (a : MvPowerSeries σ R) → R)
          (↑((trunc R i : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R) :
        R))
    atTop (𝓝 ((coeff d : (a : MvPowerSeries σ R) → R) f) : Filter R)
Tactic: rw [tendsto_iff_coeff_tendsto]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : DecidableEq σ
inst_2 : CommSemiring R
inst_3 : Nonempty σ
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ Tendsto.{u_1, u_2} (β := R)
    (fun (i : σ →₀ ℕ) ↦
      ((coeff d : (a : MvPowerSeries σ R) → R)
          (↑((trunc R i : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R) :
        R))
    atTop (𝓝 ((coeff d : (a : MvPowerSeries σ R) → R) f) : Filter R)
have obtain : ∀ (s : σ),
  True →
    Tendsto.{u_1, u_2} (β := R)
      (fun (i : σ →₀ ℕ) ↦
        ((coeff d : (a : MvPowerSeries σ R) → R)
            (↑((trunc R i : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R) :
          R))
      atTop (𝓝 ((coeff d : (a : MvPowerSeries σ R) → R) f) : Filter R)
Tactic: obtain ⟨s, _⟩ := (exists_const σ).mpr trivial
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : DecidableEq σ
inst_2 : CommSemiring R
inst_3 : Nonempty σ
f : MvPowerSeries σ R
d : σ →₀ ℕ
s : σ
h : True
⊢ Tendsto.{u_1, u_2} (β := R)
    (fun (i : σ →₀ ℕ) ↦
      ((coeff d : (a : MvPowerSeries σ R) → R)
          (↑((trunc R i : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R) :
        R))
    atTop (𝓝 ((coeff d : (a : MvPowerSeries σ R) → R) f) : Filter R)
have apply : ∀ i ≥ d + Finsupp.single s 1,
  Eq.{u_2 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        (↑((trunc R i : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R) :
      R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
Tactic: apply tendsto_atTop_of_eventually_const (i₀ := d + Finsupp.single s 1)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : DecidableEq σ
inst_2 : CommSemiring R
inst_3 : Nonempty σ
f : MvPowerSeries σ R
d : σ →₀ ℕ
s : σ
h : True
n : σ →₀ ℕ
hn : n ≥ d + Finsupp.single s 1
⊢ Eq.{u_2 + 1} (α := R)
    ((coeff d : (a : MvPowerSeries σ R) → R)
        (↑((trunc R n : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R) :
      R)
    ((coeff d : (a : MvPowerSeries σ R) → R) f : R)
have hc : d < n
Tactic: rw [MvPolynomial.coeff_coe, coeff_trunc, if_pos]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : DecidableEq σ
inst_2 : CommSemiring R
inst_3 : Nonempty σ
f : MvPowerSeries σ R
d : σ →₀ ℕ
s : σ
h : True
n : σ →₀ ℕ
hn : n ≥ d + Finsupp.single s 1
⊢ d < n
have apply : d < d + Finsupp.single s 1
Tactic: apply lt_of_lt_of_le _ hn
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
⊢ Continuous[inst, instTopologicalSpace R] (⇑C : (a : R) → MvPowerSeries σ R)
have simp : ∀ (x : R), ContinuousAt (Y := MvPowerSeries σ R) (⇑C : (a : R) → MvPowerSeries σ R) x
Tactic: simp only [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
⊢ ∀ (x : R), ContinuousAt (Y := MvPowerSeries σ R) (⇑C : (a : R) → MvPowerSeries σ R) x
have refine : ∀ (r : R) (d : σ →₀ ℕ),
  Tendsto (β := R)
    (fun (i : R) ↦
      ((coeff d : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) i : MvPowerSeries σ R) : R))
    (𝓝 r)
    (𝓝 ((coeff d : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)) : Filter R)
Tactic: refine fun r ↦ (tendsto_iff_coeff_tendsto _ _ _).mpr fun d ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
r : R
d : σ →₀ ℕ
⊢ Tendsto (β := R)
    (fun (i : R) ↦
      ((coeff d : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) i : MvPowerSeries σ R) : R))
    (𝓝 r)
    (𝓝 ((coeff d : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)) : Filter R)
have simp : Tendsto (fun (i : R) ↦ if d = 0 then i else 0) (𝓝 r) (𝓝 (if d = 0 then r else 0))
Tactic: simp only [coeff_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
r : R
d : σ →₀ ℕ
⊢ Tendsto (fun (i : R) ↦ if d = 0 then i else 0) (𝓝 r) (𝓝 (if d = 0 then r else 0))
have pos : d = 0 → Tendsto (fun (i : R) ↦ i) (𝓝 r) (𝓝 r)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
r : R
d : σ →₀ ℕ
pos : d = 0 → Tendsto (fun (i : R) ↦ i) (𝓝 r) (𝓝 r)
⊢ Tendsto (fun (i : R) ↦ if d = 0 then i else 0) (𝓝 r) (𝓝 (if d = 0 then r else 0))
have neg : ¬d = 0 → Tendsto (β := R) (fun (i : R) ↦ 0) (𝓝 r) (𝓝 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
⊢ Continuous[inst, instTopologicalSpace R] (⇑C : (a : R) → MvPowerSeries σ R)
have simp : ∀ (x : R), ContinuousAt (Y := MvPowerSeries σ R) (⇑C : (a : R) → MvPowerSeries σ R) x
Tactic: classical
  simp only [continuous_iff_continuousAt]
  refine fun r ↦ (tendsto_iff_coeff_tendsto _ _ _).mpr fun d ↦ ?_
  simp only [coeff_C]
  split_ifs
  · exact tendsto_id
  · exact tendsto_const_nhds
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
simp : ∀ (x : R), ContinuousAt (Y := MvPowerSeries σ R) (⇑C : (a : R) → MvPowerSeries σ R) x
⊢ Continuous[inst, instTopologicalSpace R] (⇑C : (a : R) → MvPowerSeries σ R)
have simp₁ : ∀ (r : R) (d : σ →₀ ℕ),
  Tendsto (β := R)
    (fun (i : R) ↦
      ((coeff d : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) i : MvPowerSeries σ R) : R))
    (𝓝 r)
    (𝓝 ((coeff d : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)) : Filter R)
Tactic: classical
  simp only [continuous_iff_continuousAt]
  refine fun r ↦ (tendsto_iff_coeff_tendsto _ _ _).mpr fun d ↦ ?_
  simp only [coeff_C]
  split_ifs
  · exact tendsto_id
  · exact tendsto_const_nhds
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
simp : ∀ (x : R), ContinuousAt (Y := MvPowerSeries σ R) (⇑C : (a : R) → MvPowerSeries σ R) x
simp₁ :
  ∀ (r : R) (d : σ →₀ ℕ),
    Tendsto (β := R)
      (fun (i : R) ↦
        ((coeff d : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) i : MvPowerSeries σ R) : R))
      (𝓝 r)
      (𝓝 ((coeff d : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)) : Filter R)
⊢ Continuous[inst, instTopologicalSpace R] (⇑C : (a : R) → MvPowerSeries σ R)
have simp₂ : ∀ (r : R) (d : σ →₀ ℕ), Tendsto (fun (i : R) ↦ if d = 0 then i else 0) (𝓝 r) (𝓝 (if d = 0 then r else 0))
Tactic: classical
  simp only [continuous_iff_continuousAt]
  refine fun r ↦ (tendsto_iff_coeff_tendsto _ _ _).mpr fun d ↦ ?_
  simp only [coeff_C]
  split_ifs
  · exact tendsto_id
  · exact tendsto_const_nhds
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
simp : ∀ (x : R), ContinuousAt (Y := MvPowerSeries σ R) (⇑C : (a : R) → MvPowerSeries σ R) x
simp₁ :
  ∀ (r : R) (d : σ →₀ ℕ),
    Tendsto (β := R)
      (fun (i : R) ↦
        ((coeff d : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) i : MvPowerSeries σ R) : R))
      (𝓝 r)
      (𝓝 ((coeff d : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)) : Filter R)
simp₂ : ∀ (r : R) (d : σ →₀ ℕ), Tendsto (fun (i : R) ↦ if d = 0 then i else 0) (𝓝 r) (𝓝 (if d = 0 then r else 0))
⊢ Continuous[inst, instTopologicalSpace R] (⇑C : (a : R) → MvPowerSeries σ R)
have pos : ∀ (r : R) (d : σ →₀ ℕ), d = 0 → Tendsto (fun (i : R) ↦ i) (𝓝 r) (𝓝 r)
Tactic: classical
  simp only [continuous_iff_continuousAt]
  refine fun r ↦ (tendsto_iff_coeff_tendsto _ _ _).mpr fun d ↦ ?_
  simp only [coeff_C]
  split_ifs
  · exact tendsto_id
  · exact tendsto_const_nhds
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
simp : ∀ (x : R), ContinuousAt (Y := MvPowerSeries σ R) (⇑C : (a : R) → MvPowerSeries σ R) x
simp₁ :
  ∀ (r : R) (d : σ →₀ ℕ),
    Tendsto (β := R)
      (fun (i : R) ↦
        ((coeff d : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) i : MvPowerSeries σ R) : R))
      (𝓝 r)
      (𝓝 ((coeff d : (a : MvPowerSeries σ R) → R) ((C : (a : R) → MvPowerSeries σ R) r : MvPowerSeries σ R)) : Filter R)
simp₂ : ∀ (r : R) (d : σ →₀ ℕ), Tendsto (fun (i : R) ↦ if d = 0 then i else 0) (𝓝 r) (𝓝 (if d = 0 then r else 0))
pos : ∀ (r : R) (d : σ →₀ ℕ), d = 0 → Tendsto (fun (i : R) ↦ i) (𝓝 r) (𝓝 r)
⊢ Continuous[inst, instTopologicalSpace R] (⇑C : (a : R) → MvPowerSeries σ R)
have neg : ∀ (r : R) (d : σ →₀ ℕ), ¬d = 0 → Tendsto (β := R) (fun (i : R) ↦ 0) (𝓝 r) (𝓝 0)
Tactic: classical
  simp only [continuous_iff_continuousAt]
  refine fun r ↦ (tendsto_iff_coeff_tendsto _ _ _).mpr fun d ↦ ?_
  simp only [coeff_C]
  split_ifs
  · exact tendsto_id
  · exact tendsto_const_nhds
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
⊢ Tendsto (β := MvPowerSeries σ R) (fun (x : σ) ↦ X x) cofinite (𝓝 0)
have simp : ∀ (d : σ →₀ ℕ), Tendsto.{u_1, u_2} (β := R) (fun (i : σ) ↦ if d = Finsupp.single i 1 then 1 else 0) cofinite (𝓝 0)
Tactic: simp only [tendsto_iff_coeff_tendsto, ← coeff_apply, coeff_X, coeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
⊢ ∀ (d : σ →₀ ℕ), Tendsto.{u_1, u_2} (β := R) (fun (i : σ) ↦ if d = Finsupp.single i 1 then 1 else 0) cofinite (𝓝 0)
have refine : ∀ (d : σ →₀ ℕ), ∀ᶠ (x' : σ) in cofinite, Eq.{u_2 + 1} (α := R) (if d = Finsupp.single x' 1 then 1 else 0) 0
Tactic: refine fun d ↦ tendsto_nhds_of_eventually_eq ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
d : σ →₀ ℕ
⊢ ∀ᶠ (x' : σ) in cofinite, Eq.{u_2 + 1} (α := R) (if d = Finsupp.single x' 1 then 1 else 0) 0
have pos : ∀ (h : ∃ (i : σ), d = Finsupp.single i 1),
  ∀ᶠ (x' : σ) in cofinite, Eq.{u_2 + 1} (α := R) (if d = Finsupp.single x' 1 then 1 else 0) 0
Tactic: by_cases! h : ∃ i, d = Finsupp.single i 1
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
d : σ →₀ ℕ
pos :
  ∀ (h : ∃ (i : σ), d = Finsupp.single i 1),
    ∀ᶠ (x' : σ) in cofinite, Eq.{u_2 + 1} (α := R) (if d = Finsupp.single x' 1 then 1 else 0) 0
⊢ ∀ᶠ (x' : σ) in cofinite, Eq.{u_2 + 1} (α := R) (if d = Finsupp.single x' 1 then 1 else 0) 0
have neg : ∀ (h : ∀ (i : σ), d ≠ Finsupp.single i 1),
  ∀ᶠ (x' : σ) in cofinite, Eq.{u_2 + 1} (α := R) (if d = Finsupp.single x' 1 then 1 else 0) 0
Tactic: by_cases! h : ∃ i, d = Finsupp.single i 1
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
d : σ →₀ ℕ
h : ∃ (i : σ), d = Finsupp.single i 1
⊢ ∀ᶠ (x' : σ) in cofinite, Eq.{u_2 + 1} (α := R) (if d = Finsupp.single x' 1 then 1 else 0) 0
have pos : ∀ (i : σ) (hi : d = Finsupp.single i 1),
  ∀ᶠ (x' : σ) in cofinite, Eq.{u_2 + 1} (α := R) (if d = Finsupp.single x' 1 then 1 else 0) 0
Tactic: obtain ⟨i, hi⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
d : σ →₀ ℕ
i : σ
hi : d = Finsupp.single i 1
⊢ ∀ᶠ (x' : σ) in cofinite, Eq.{u_2 + 1} (α := R) (if d = Finsupp.single x' 1 then 1 else 0) 0
have h : ∀ (j : σ) (hj : j ≠ i), Eq.{u_2 + 1} (α := R) (if d = Finsupp.single j 1 then 1 else 0) 0
Tactic: filter_upwards [eventually_cofinite_ne i] with j hj
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
⊢ Tendsto (β := MvPowerSeries σ R) (fun (x : σ) ↦ X x) cofinite (𝓝 0)
have simp : ∀ (d : σ →₀ ℕ), Tendsto.{u_1, u_2} (β := R) (fun (i : σ) ↦ if d = Finsupp.single i 1 then 1 else 0) cofinite (𝓝 0)
Tactic: classical
  simp only [tendsto_iff_coeff_tendsto, ← coeff_apply, coeff_X, coeff_zero]
  refine fun d ↦ tendsto_nhds_of_eventually_eq ?_
  by_cases! h : ∃ i, d = Finsupp.single i 1
  · obtain ⟨i, hi⟩ := h
    filter_upwards [eventually_cofinite_ne i] with j hj
    simp [hi, Finsupp.single_eq_single_iff, hj.symm]
  · simpa only [ite_eq_right_iff] using
      Eventually.of_forall fun x h' ↦ (h x h').elim
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
simp :
  ∀ (d : σ →₀ ℕ), Tendsto.{u_1, u_2} (β := R) (fun (i : σ) ↦ if d = Finsupp.single i 1 then 1 else 0) cofinite (𝓝 0)
⊢ Tendsto (β := MvPowerSeries σ R) (fun (x : σ) ↦ X x) cofinite (𝓝 0)
have simp₁ : ∀ (d : σ →₀ ℕ), ∀ᶠ (x' : σ) in cofinite, Eq.{u_2 + 1} (α := R) (if d = Finsupp.single x' 1 then 1 else 0) 0
Tactic: classical
  simp only [tendsto_iff_coeff_tendsto, ← coeff_apply, coeff_X, coeff_zero]
  refine fun d ↦ tendsto_nhds_of_eventually_eq ?_
  by_cases! h : ∃ i, d = Finsupp.single i 1
  · obtain ⟨i, hi⟩ := h
    filter_upwards [eventually_cofinite_ne i] with j hj
    simp [hi, Finsupp.single_eq_single_iff, hj.symm]
  · simpa only [ite_eq_right_iff] using
      Eventually.of_forall fun x h' ↦ (h x h').elim
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
simp :
  ∀ (d : σ →₀ ℕ), Tendsto.{u_1, u_2} (β := R) (fun (i : σ) ↦ if d = Finsupp.single i 1 then 1 else 0) cofinite (𝓝 0)
simp₁ : ∀ (d : σ →₀ ℕ), ∀ᶠ (x' : σ) in cofinite, Eq.{u_2 + 1} (α := R) (if d = Finsupp.single x' 1 then 1 else 0) 0
⊢ Tendsto (β := MvPowerSeries σ R) (fun (x : σ) ↦ X x) cofinite (𝓝 0)
have pos : ∀ (d : σ →₀ ℕ) (h : ∃ (i : σ), d = Finsupp.single i 1),
  ∀ᶠ (x' : σ) in cofinite, Eq.{u_2 + 1} (α := R) (if d = Finsupp.single x' 1 then 1 else 0) 0
Tactic: classical
  simp only [tendsto_iff_coeff_tendsto, ← coeff_apply, coeff_X, coeff_zero]
  refine fun d ↦ tendsto_nhds_of_eventually_eq ?_
  by_cases! h : ∃ i, d = Finsupp.single i 1
  · obtain ⟨i, hi⟩ := h
    filter_upwards [eventually_cofinite_ne i] with j hj
    simp [hi, Finsupp.single_eq_single_iff, hj.symm]
  · simpa only [ite_eq_right_iff] using
      Eventually.of_forall fun x h' ↦ (h x h').elim
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
simp :
  ∀ (d : σ →₀ ℕ), Tendsto.{u_1, u_2} (β := R) (fun (i : σ) ↦ if d = Finsupp.single i 1 then 1 else 0) cofinite (𝓝 0)
simp₁ : ∀ (d : σ →₀ ℕ), ∀ᶠ (x' : σ) in cofinite, Eq.{u_2 + 1} (α := R) (if d = Finsupp.single x' 1 then 1 else 0) 0
pos :
  ∀ (d : σ →₀ ℕ) (h : ∃ (i : σ), d = Finsupp.single i 1),
    ∀ᶠ (x' : σ) in cofinite, Eq.{u_2 + 1} (α := R) (if d = Finsupp.single x' 1 then 1 else 0) 0
⊢ Tendsto (β := MvPowerSeries σ R) (fun (x : σ) ↦ X x) cofinite (𝓝 0)
have neg : ∀ (d : σ →₀ ℕ) (h : ∀ (i : σ), d ≠ Finsupp.single i 1),
  ∀ᶠ (x' : σ) in cofinite, Eq.{u_2 + 1} (α := R) (if d = Finsupp.single x' 1 then 1 else 0) 0
Tactic: classical
  simp only [tendsto_iff_coeff_tendsto, ← coeff_apply, coeff_X, coeff_zero]
  refine fun d ↦ tendsto_nhds_of_eventually_eq ?_
  by_cases! h : ∃ i, d = Finsupp.single i 1
  · obtain ⟨i, hi⟩ := h
    filter_upwards [eventually_cofinite_ne i] with j hj
    simp [hi, Finsupp.single_eq_single_iff, hj.symm]
  · simpa only [ite_eq_right_iff] using
      Eventually.of_forall fun x h' ↦ (h x h').elim
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : MvPowerSeries σ R
hf : IsNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
⊢ IsTopologicallyNilpotent f
have obtain : ∀ (m : ℕ) (hm : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0),
  IsTopologicallyNilpotent f
Tactic: obtain ⟨m, hm⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hm : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
⊢ IsTopologicallyNilpotent f
have simp_rw : ∀ (d : σ →₀ ℕ), Tendsto.{0, u_2} (β := R) (fun (i : ℕ) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f ^ i)) atTop (𝓝 0)
Tactic: simp_rw [IsTopologicallyNilpotent, tendsto_iff_coeff_tendsto, coeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : MvPowerSeries σ R
hf : IsNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
⊢ IsTopologicallyNilpotent f
have obtain : ∀ (m : ℕ) (hm : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0),
  IsTopologicallyNilpotent f
Tactic: classical
  obtain ⟨m, hm⟩ := hf
  simp_rw [IsTopologicallyNilpotent, tendsto_iff_coeff_tendsto, coeff_zero]
  exact fun d ↦ tendsto_atTop_of_eventually_const fun n hn ↦
    coeff_eq_zero_of_constantCoeff_nilpotent hm hn
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : MvPowerSeries σ R
hf : IsNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
obtain :
  ∀ (m : ℕ) (hm : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0),
    IsTopologicallyNilpotent f
⊢ IsTopologicallyNilpotent f
have obtain₁ : ∀ (m : ℕ) (hm : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0) (d : σ →₀ ℕ),
  Tendsto.{0, u_2} (β := R) (fun (i : ℕ) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f ^ i)) atTop (𝓝 0)
Tactic: classical
  obtain ⟨m, hm⟩ := hf
  simp_rw [IsTopologicallyNilpotent, tendsto_iff_coeff_tendsto, coeff_zero]
  exact fun d ↦ tendsto_atTop_of_eventually_const fun n hn ↦
    coeff_eq_zero_of_constantCoeff_nilpotent hm hn
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : MvPowerSeries σ R
hf : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ Tendsto (β := MvPowerSeries σ R) (fun (n : ℕ) ↦ f ^ n) atTop (𝓝 0)
have hf₁ : IsNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
Tactic: apply isTopologicallyNilpotent_of_constantCoeff_isNilpotent
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : MvPowerSeries σ R
hf : Eq.{u_2 + 1} (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) (0 : R)
⊢ IsNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
have hf₁ : IsNilpotent.{u_2} (R := R) 0
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : DiscreteTopology R
f : MvPowerSeries σ R
⊢ IsTopologicallyNilpotent f ↔ IsNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
have refine : ∀ (H : IsTopologicallyNilpotent f), IsNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
Tactic: refine ⟨fun H ↦ ?_, isTopologicallyNilpotent_of_constantCoeff_isNilpotent⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : DiscreteTopology R
f : MvPowerSeries σ R
H : IsTopologicallyNilpotent f
⊢ IsNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
have H₁ : IsTopologicallyNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
Tactic: replace H := H.map (continuous_constantCoeff R)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : DiscreteTopology R
f : MvPowerSeries σ R
H : IsTopologicallyNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
⊢ IsNilpotent.{u_2} (R := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
have H₁ : ∀ᶠ (x : ℕ) in atTop, HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) x = 0
Tactic: simp_rw [IsTopologicallyNilpotent, nhds_discrete, tendsto_pure] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.PiTopology (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
f : MvPowerSeries σ R
⊢ HasSum (fun (d : σ →₀ ℕ) ↦ (monomial d : (a : R) → MvPowerSeries σ R) ((coeff d : (a : MvPowerSeries σ R) → R) f)) f
have rw : ∀ (x : σ →₀ ℕ),
  HasSum (fun (i : σ →₀ ℕ) ↦ (monomial i : (a : R) → MvPowerSeries σ R) ((coeff i : (a : MvPowerSeries σ R) → R) f) x)
    (f x)
Tactic: rw [Pi.hasSum]