-- Mathlib/RingTheory/MvPowerSeries/PiTopology.lean
theorem tendsto_pow_of_constantCoeff_nilpotent_iff [CommRing R] [DiscreteTopology R] (f) :
    Tendsto (fun n : ℕ => f ^ n) atTop (nhds 0) ↔
      IsNilpotent (constantCoeff σ R f)

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
h : Tendsto (fun n => f ^ n) atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ R) (f ^ n)) ⁻¹' s ∈ atTop
⊢ DiscreteTopology R

σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
h : Tendsto (fun n => f ^ n) atTop (nhds 0)
this : (fun n => (constantCoeff σ R) (f ^ n)) ⁻¹' {0} ∈ atTop
⊢ IsNilpotent ((constantCoeff σ R) f)

Tactic:
infer_instance

Result:
σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
h : Tendsto (fun n => f ^ n) atTop (nhds 0)
this : (fun n => (constantCoeff σ R) (f ^ n)) ⁻¹' {0} ∈ atTop
⊢ IsNilpotent ((constantCoeff σ R) f)

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
h : Tendsto (fun n => f ^ n) atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ R) (f ^ n)) ⁻¹' s ∈ atTop
⊢ {0} ∈ nhds 0

σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
h : Tendsto (fun n => f ^ n) atTop (nhds 0)
this : (fun n => (constantCoeff σ R) (f ^ n)) ⁻¹' {0} ∈ atTop
⊢ IsNilpotent ((constantCoeff σ R) f)

Tactic:
suffices ∀ x : R, {x} ∈ nhds x by exact this 0

Result:
σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
h : Tendsto (fun n => f ^ n) atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ R) (f ^ n)) ⁻¹' s ∈ atTop
⊢ ∀ (x : R), {x} ∈ nhds x

σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
h : Tendsto (fun n => f ^ n) atTop (nhds 0)
this : (fun n => (constantCoeff σ R) (f ^ n)) ⁻¹' {0} ∈ atTop
⊢ IsNilpotent ((constantCoeff σ R) f)

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
h : atTop ≤ comap (fun n => f ^ n) (nhds 0)
⊢ nhds 0 ≤ comap (⇑(constantCoeff σ R)) (nhds 0)

Tactic:
rw [← map_le_iff_le_comap]

Result:
σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
h : atTop ≤ comap (fun n => f ^ n) (nhds 0)
⊢ Filter.map (⇑(constantCoeff σ R)) (nhds 0) ≤ nhds 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
h : Tendsto (fun n => f ^ n) atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ R) (f ^ n)) ⁻¹' s ∈ atTop
⊢ IsNilpotent ((constantCoeff σ R) f)

Tactic:
specialize this {0} _

Result:
σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
h : Tendsto (fun n => f ^ n) atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ R) (f ^ n)) ⁻¹' s ∈ atTop
⊢ {0} ∈ nhds 0

σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
h : Tendsto (fun n => f ^ n) atTop (nhds 0)
this : (fun n => (constantCoeff σ R) (f ^ n)) ⁻¹' {0} ∈ atTop
⊢ IsNilpotent ((constantCoeff σ R) f)

Proof state:
case intro
σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
h : Tendsto (fun n => f ^ n) atTop (nhds 0)
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → (constantCoeff σ R) f ^ b = 0
⊢ IsNilpotent ((constantCoeff σ R) f)

Tactic:
use m

Result:
case h
σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
h : Tendsto (fun n => f ^ n) atTop (nhds 0)
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → (constantCoeff σ R) f ^ b = 0
⊢ (constantCoeff σ R) f ^ m = 0