awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_3
R : Type u_4
t u : TopologicalSpace R
htu : t ≤ u
⊢ LE.le (α := TopologicalSpace (MvPowerSeries σ R))
    (⨅ (i : σ →₀ ℕ),
      TopologicalSpace.induced (Y := (fun (a : σ →₀ ℕ) ↦ R) i) (fun (f : (i : σ →₀ ℕ) → (fun (a : σ →₀ ℕ) ↦ R) i) ↦ f i)
        ((fun (i : σ →₀ ℕ) ↦ t) i))
    (⨅ (i : σ →₀ ℕ),
      TopologicalSpace.induced (Y := (fun (a : σ →₀ ℕ) ↦ R) i) (fun (f : (i : σ →₀ ℕ) → (fun (a : σ →₀ ℕ) ↦ R) i) ↦ f i)
        ((fun (i : σ →₀ ℕ) ↦ u) i))

Tactic:
gcongr
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : T0Space R
⊢ T0Space (MvPowerSeries σ R)

Tactic:
Pi.instT0Space

Premises used: MvPowerSeries, MvPowerSeries.WithPiTopology.instTopologicalSpace._aux_1, Pi.instT0Space
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : T2Space R
⊢ T2Space (MvPowerSeries σ R)

Tactic:
Pi.t2Space

Premises used: Pi.t2Space, MvPowerSeries, MvPowerSeries.WithPiTopology.instTopologicalSpace._aux_1
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
d : σ →₀ ℕ
⊢ Continuous[instTopologicalSpace R, inst] (⇑(coeff d) : (a : MvPowerSeries σ R) → R)

Tactic:
continuous_pi_iff.mp continuous_id d

Premises used: MvPowerSeries, MvPowerSeries.WithPiTopology.instTopologicalSpace._aux_1, continuous_pi_iff, continuous_id, Iff.mp
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
⊢ Continuous[instTopologicalSpace R, inst] (⇑constantCoeff : (a : MvPowerSeries σ R) → R)

Tactic:
continuous_coeff (R := R) 0

Premises used: MvPowerSeries.WithPiTopology.continuous_coeff, MvPowerSeries, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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
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)
⊢ 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)

Tactic:
rw [nhds_pi, tendsto_pi]

Premises used: nhds_pi, Filter.tendsto_pi
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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
⊢ (∀ (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:
forall_congr' (fun d => Iff.rfl)

Premises used: Iff.rfl, forall_congr'
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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
⊢ (∀ (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:
exact forall_congr' (fun d => Iff.rfl)

Premises used: Iff.rfl, forall_congr'
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : DecidableEq σ
inst_2 : CommSemiring R
f : MvPowerSeries σ R
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)
⊢ Tendsto (fun (d : σ →₀ ℕ) ↦ (↑((trunc' R d : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R))
    atTop (𝓝 f)

Tactic:
rw [tendsto_iff_coeff_tendsto]

Premises used: MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : DecidableEq σ
inst_2 : CommSemiring R
f : MvPowerSeries σ R
d n : σ →₀ ℕ
hdn : d ≤ n
⊢ 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)

Tactic:
simp [coeff_trunc', hdn]

Premises used: MvPowerSeries.coeff_trunc'
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : DecidableEq σ
inst_2 : CommSemiring R
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)

Tactic:
exact tendsto_atTop_of_eventually_const fun n (hdn : d ≤ n) ↦ (by simp [coeff_trunc', hdn])

Premises used: tendsto_atTop_of_eventually_const
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : DecidableEq σ
inst_2 : CommSemiring R
inst_3 : Nonempty σ
f : MvPowerSeries σ R
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)
⊢ Tendsto (fun (d : σ →₀ ℕ) ↦ (↑((trunc R d : (a : MvPowerSeries σ R) → MvPolynomial σ R) f) : MvPowerSeries σ R)) atTop
    (𝓝 f)

Tactic:
rw [tendsto_iff_coeff_tendsto]

Premises used: MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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 : σ →₀ ℕ
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)
⊢ 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

Premises used: Iff.mpr, trivial, exists_const
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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
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)
⊢ 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:
apply tendsto_atTop_of_eventually_const (i₀ := d + Finsupp.single s 1)

Premises used: tendsto_atTop_of_eventually_const
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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
hc : d < n
⊢ 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)

Tactic:
rw [MvPolynomial.coeff_coe, coeff_trunc, if_pos]

Premises used: if_pos, MvPolynomial.coeff_coe, MvPowerSeries.coeff_trunc
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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
apply : d < d + Finsupp.single s 1
⊢ d < n

Tactic:
apply lt_of_lt_of_le _ hn

Premises used: lt_of_lt_of_le
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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
⊢ LT.lt (α := ℕ) (0 : ℕ) ((Finsupp.single s 1 : (a : σ) → ℕ) s : ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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 < d + Finsupp.single s 1

Tactic:
simpa [Finsupp.lt_def] using ⟨s, by simp⟩

Premises used: Finsupp.lt_def
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : MvPowerSeries σ R
⊢ Membership.mem (γ := Set (MvPowerSeries σ R))
    (closure[instTopologicalSpace R] (Set.range (ι := MvPolynomial σ R) MvPolynomial.toMvPowerSeries)) f

Tactic:
mem_closure_of_tendsto (tendsto_trunc'_atTop f) <| .of_forall fun _ ↦ Set.mem_range_self _

Premises used: Set.mem_range_self, Filter.Eventually.of_forall, MvPowerSeries.WithPiTopology.tendsto_trunc'_atTop, MvPowerSeries.trunc', DFunLike.coe, mem_closure_of_tendsto
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : MvPowerSeries σ R
⊢ Membership.mem (γ := Set (MvPowerSeries σ R))
    (closure[instTopologicalSpace R] (Set.range (ι := MvPolynomial σ R) MvPolynomial.toMvPowerSeries)) f

Tactic:
exact mem_closure_of_tendsto (tendsto_trunc'_atTop f) <| .of_forall fun _ ↦ Set.mem_range_self _

Premises used: MvPowerSeries.WithPiTopology.tendsto_trunc'_atTop, mem_closure_of_tendsto
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : CommSemiring R
f : MvPowerSeries σ R
⊢ Membership.mem (γ := Set (MvPowerSeries σ R))
    (closure[instTopologicalSpace R] (Set.range (ι := MvPolynomial σ R) MvPolynomial.toMvPowerSeries)) f

Tactic:
classical
  exact mem_closure_of_tendsto (tendsto_trunc'_atTop f) <| .of_forall fun _ ↦ Set.mem_range_self _
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsTopologicalRing R
⊢ IsTopologicalRing (MvPowerSeries σ R)

Tactic:
{ instIsTopologicalSemiring σ R with
    continuous_neg := continuous_pi fun d ↦ Continuous.comp continuous_neg
      (continuous_coeff R d) }

Premises used: IsTopologicalRing.mk, MvPowerSeries.WithPiTopology.instIsTopologicalSemiring
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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)

Tactic:
simp only [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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

Tactic:
fun r ↦ (tendsto_iff_coeff_tendsto _ _ _).mpr fun d ↦ ?_

Premises used: Iff.mpr, ContinuousAt, nhds, MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto, DFunLike.coe, MvPowerSeries.C
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
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)
⊢ ∀ (x : R), ContinuousAt (Y := MvPowerSeries σ R) (⇑C : (a : R) → MvPowerSeries σ R) x

Tactic:
refine fun r ↦ (tendsto_iff_coeff_tendsto _ _ _).mpr fun d ↦ ?_

Premises used: Iff.mpr, MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
r : R
d : σ →₀ ℕ
simp : Tendsto (fun (i : R) ↦ if d = 0 then i else 0) (𝓝 r) (𝓝 (if d = 0 then r else 0))
⊢ 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:
simp only [coeff_C]

Premises used: MvPowerSeries.coeff_C
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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)
neg : ¬d = 0 → Tendsto (β := R) (fun (i : R) ↦ 0) (𝓝 r) (𝓝 0)
⊢ Tendsto (fun (i : R) ↦ if d = 0 then i else 0) (𝓝 r) (𝓝 (if d = 0 then r else 0))

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
r : R
d : σ →₀ ℕ
h : d = 0
⊢ Tendsto (fun (i : R) ↦ i) (𝓝 r) (𝓝 r)

Tactic:
tendsto_id

Premises used: Filter.tendsto_id
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
r : R
d : σ →₀ ℕ
h : d = 0
⊢ Tendsto (fun (i : R) ↦ i) (𝓝 r) (𝓝 r)

Tactic:
exact tendsto_id

Premises used: Filter.tendsto_id
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
r : R
d : σ →₀ ℕ
h : ¬d = 0
⊢ Tendsto (β := R) (fun (i : R) ↦ 0) (𝓝 r) (𝓝 0)

Tactic:
tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
r : R
d : σ →₀ ℕ
h : ¬d = 0
⊢ Tendsto (β := R) (fun (i : R) ↦ 0) (𝓝 r) (𝓝 0)

Tactic:
exact tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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)
neg neg₁ : ∀ (r : R) (d : σ →₀ ℕ), ¬d = 0 → Tendsto (β := R) (fun (i : R) ↦ 0) (𝓝 r) (𝓝 0)
⊢ Continuous[inst, instTopologicalSpace R] (⇑C : (a : R) → MvPowerSeries σ 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

Premises used: Iff.mpr, Filter.tendsto_id, tendsto_const_nhds, MvPowerSeries.coeff_C, MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto, continuous_iff_continuousAt
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
S : Type u_3
inst_1 : Semiring S
inst_2 : TopologicalSpace S
inst_3 : CommSemiring R
inst_4 : Algebra R S
inst_5 : ContinuousSMul R S
⊢ ContinuousSMul R (MvPowerSeries σ S)

Tactic:
instContinuousSMulForall

Premises used: MvPowerSeries, MvPowerSeries.WithPiTopology.instTopologicalSpace._aux_1, instContinuousSMulForall
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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)

Tactic:
simp only [tendsto_iff_coeff_tendsto, ← coeff_apply, coeff_X, coeff_zero]

Premises used: MvPowerSeries.coeff_zero, MvPowerSeries.coeff_X, MvPowerSeries.coeff_apply, MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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)

Tactic:
fun d ↦ tendsto_nhds_of_eventually_eq ?_

Premises used: tendsto_nhds_of_eventually_eq
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
refine : ∀ (d : σ →₀ ℕ), ∀ᶠ (x' : σ) in cofinite, Eq.{u_2 + 1} (α := R) (if d = Finsupp.single x' 1 then 1 else 0) 0
⊢ ∀ (d : σ →₀ ℕ), Tendsto.{u_1, u_2} (β := R) (fun (i : σ) ↦ if d = Finsupp.single i 1 then 1 else 0) cofinite (𝓝 0)

Tactic:
refine fun d ↦ tendsto_nhds_of_eventually_eq ?_

Premises used: tendsto_nhds_of_eventually_eq
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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
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
⊢ ∀ᶠ (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
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
d : σ →₀ ℕ
h : ∃ (i : σ), d = Finsupp.single i 1
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
⊢ ∀ᶠ (x' : σ) in cofinite, Eq.{u_2 + 1} (α := R) (if d = Finsupp.single x' 1 then 1 else 0) 0

Tactic:
obtain ⟨i, hi⟩ := h
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
d : σ →₀ ℕ
i : σ
hi : d = Finsupp.single i 1
h : ∀ (j : σ) (hj : j ≠ i), Eq.{u_2 + 1} (α := R) (if d = Finsupp.single j 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

Tactic:
filter_upwards [eventually_cofinite_ne i] with j hj

Premises used: Filter.eventually_cofinite_ne
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
Goal:
σ : Type u_1
R : Type u_2
inst : TopologicalSpace R
inst_1 : Semiring R
d : σ →₀ ℕ
i : σ
hi : d = Finsupp.single i 1
j : σ
hj : j ≠ i
⊢ Eq.{u_2 + 1} (α := R) (if d = Finsupp.single j 1 then 1 else 0) 0

Tactic:
simp [hi, Finsupp.single_eq_single_iff, hj.symm]

Premises used: Finsupp.single_eq_single_iff, Ne.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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

Tactic:
simpa only [ite_eq_right_iff] using
      Eventually.of_forall fun x h' ↦ (h x h').elim

Premises used: False.elim, Filter.Eventually.of_forall, ite_eq_right_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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
neg 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
⊢ Tendsto (β := MvPowerSeries σ R) (fun (x : σ) ↦ X x) 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

Premises used: MvPowerSeries.coeff_zero, Finsupp.single_eq_single_iff, MvPowerSeries.coeff_X, MvPowerSeries.coeff_apply, tendsto_nhds_of_eventually_eq, ite_eq_right_iff, MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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

Tactic:
obtain ⟨m, hm⟩ := hf
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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
simp_rw :
  ∀ (d : σ →₀ ℕ), Tendsto.{0, u_2} (β := R) (fun (i : ℕ) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f ^ i)) atTop (𝓝 0)
⊢ IsTopologicallyNilpotent f

Tactic:
simp_rw [IsTopologicallyNilpotent, tendsto_iff_coeff_tendsto, coeff_zero]

Premises used: MvPowerSeries.coeff_zero, IsTopologicallyNilpotent, MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
-- Module: Mathlib.RingTheory.MvPowerSeries.PiTopology
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
⊢ ∀ (d : σ →₀ ℕ), Tendsto.{0, u_2} (β := R) (fun (i : ℕ) ↦ (coeff d : (a : MvPowerSeries σ R) → R) (f ^ i)) atTop (𝓝 0)

Tactic:
fun d ↦ tendsto_atTop_of_eventually_const fun n hn ↦
    coeff_eq_zero_of_constantCoeff_nilpotent hm hn

Premises used: MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotent, tendsto_atTop_of_eventually_const