-- 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 : Tendsto (fun n => (constantCoeff σ R) (f ^ n)) atTop (nhds 0)
⊢ IsNilpotent ((constantCoeff σ R) f)

Tactic:
simp only [tendsto_def] at this

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
⊢ 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 : ∃ a, ∀ (b : ℕ), a ≤ b → (constantCoeff σ R) f ^ b = 0
⊢ IsNilpotent ((constantCoeff σ R) f)

Tactic:
obtain ⟨m, hm⟩ := this

Result:
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)

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)
⊢ IsNilpotent ((constantCoeff σ R) f)

Tactic:
suffices Tendsto (fun n : ℕ => constantCoeff σ R (f ^ n)) atTop (nhds 0) by
  simp only [tendsto_def] at this
  specialize this {0} _
  suffices ∀ x : R, {x} ∈ nhds x by exact this 0
  rw [← discreteTopology_iff_singleton_mem_nhds]; infer_instance
  simp only [map_pow, mem_atTop_sets, ge_iff_le, Set.mem_preimage,
    Set.mem_singleton_iff] at this
  obtain ⟨m, hm⟩ := this
  use m
  apply hm m (le_refl m)

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)
⊢ Tendsto (fun n => (constantCoeff σ R) (f ^ n)) atTop (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
⊢ ∀ (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)

Tactic:
rw [← discreteTopology_iff_singleton_mem_nhds]

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
⊢ 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)

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

Tactic:
intro h

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)
⊢ 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
⊢ Tendsto (fun n => f ^ n) atTop (nhds 0) ↔ IsNilpotent ((constantCoeff σ R) f)

Tactic:
refine ⟨?_, tendsto_pow_zero_of_constantCoeff_nilpotent⟩

Result:
σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
⊢ 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)
⊢ Tendsto (⇑(constantCoeff σ R)) (Filter.map (HPow.hPow f) atTop) (nhds 0)

Tactic:
simp only [Tendsto, map_le_iff_le_comap] at h ⊢

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)
⊢ atTop ≤ comap (HPow.hPow f) (comap (⇑(constantCoeff σ R)) (nhds 0))

Proof state:
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

Tactic:
apply hm m (le_refl m)

Result:
no goals

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 : (fun n => (constantCoeff σ R) (f ^ n)) ⁻¹' {0} ∈ atTop
⊢ IsNilpotent ((constantCoeff σ R) f)

Tactic:
simp only [map_pow, mem_atTop_sets, ge_iff_le, Set.mem_preimage,
  Set.mem_singleton_iff] at this

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 : ∃ a, ∀ (b : ℕ), a ≤ b → (constantCoeff σ R) f ^ b = 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 : atTop ≤ comap (fun n => f ^ n) (nhds 0)
⊢ Filter.map (⇑(constantCoeff σ R)) (nhds 0) ≤ nhds 0

Tactic:
exact Continuous.continuousAt (continuous_constantCoeff R)

Result:
no goals

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)
⊢ Tendsto (fun n => (constantCoeff σ R) (f ^ n)) atTop (nhds 0)

Tactic:
simp only [← @comp_apply _ R ℕ, ← tendsto_map'_iff]

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)
⊢ Tendsto (⇑(constantCoeff σ R)) (Filter.map (HPow.hPow f) atTop) (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
this : ∀ (x : R), {x} ∈ nhds x
⊢ {0} ∈ nhds 0

Tactic:
exact this 0

Result:
no goals

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)
⊢ atTop ≤ comap (HPow.hPow f) (comap (⇑(constantCoeff σ R)) (nhds 0))

Tactic:
refine le_trans h (comap_mono ?_)

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)
⊢ nhds 0 ≤ comap (⇑(constantCoeff σ R)) (nhds 0)