Theorem: MvPowerSeries.tendsto_pow_of_constantCoeff_nilpotent_iff (DividedPowers/ForMathlib/MvPowerSeries/Topology.lean)

State before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
⊢ Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0) ↔ IsNilpotent ((constantCoeff σ α) f)
Tactic:
refine' ⟨_, tendsto_pow_zero_of_constantCoeff_nilpotent ⟩
State after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
⊢ Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0) → IsNilpotent ((constantCoeff σ α) f)

State before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
⊢ Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0) → IsNilpotent ((constantCoeff σ α) f)
Tactic:
intro h
State after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
⊢ IsNilpotent ((constantCoeff σ α) f)

State before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
suffices Filter.Tendsto (fun n : ℕ => constantCoeff σ α (f ^ n)) Filter.atTop (nhds 0) by
  simp only [Filter.tendsto_def] at this
  specialize this {0} _
  suffices  ∀ x : α, {x} ∈ nhds x by exact this 0
  rw [← discreteTopology_iff_singleton_mem_nhds]; infer_instance
  simp only [map_pow, Filter.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)
State after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => (constantCoeff σ α) (f ^ n)) Filter.atTop (nhds 0)

State before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => (constantCoeff σ α) (f ^ n)) Filter.atTop (nhds 0)
Tactic:
simp only [← @comp_apply _ α ℕ]
State after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => (⇑(constantCoeff σ α) ∘ HPow.hPow f) n) Filter.atTop (nhds 0)

State before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => (⇑(constantCoeff σ α) ∘ HPow.hPow f) n) Filter.atTop (nhds 0)
Tactic:
rw [← Filter.tendsto_map'_iff]
State after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (⇑(constantCoeff σ α)) (Filter.map (HPow.hPow f) Filter.atTop) (nhds 0)

State before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (⇑(constantCoeff σ α)) (Filter.map (HPow.hPow f) Filter.atTop) (nhds 0)
Tactic:
simp only [Filter.Tendsto, Filter.map_le_iff_le_comap] at h ⊢
State after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.atTop ≤ Filter.comap (fun n => f ^ n) (nhds 0)
⊢ Filter.atTop ≤ Filter.comap (HPow.hPow f) (Filter.comap (⇑(constantCoeff σ α)) (nhds 0))

State before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.atTop ≤ Filter.comap (fun n => f ^ n) (nhds 0)
⊢ Filter.atTop ≤ Filter.comap (HPow.hPow f) (Filter.comap (⇑(constantCoeff σ α)) (nhds 0))
Tactic:
apply le_trans h
State after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.atTop ≤ Filter.comap (fun n => f ^ n) (nhds 0)
⊢ Filter.comap (fun n => f ^ n) (nhds 0) ≤ Filter.comap (HPow.hPow f) (Filter.comap (⇑(constantCoeff σ α)) (nhds 0))

State before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.atTop ≤ Filter.comap (fun n => f ^ n) (nhds 0)
⊢ Filter.comap (fun n => f ^ n) (nhds 0) ≤ Filter.comap (HPow.hPow f) (Filter.comap (⇑(constantCoeff σ α)) (nhds 0))
Tactic:
apply Filter.comap_mono
State after:
case a
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.atTop ≤ Filter.comap (fun n => f ^ n) (nhds 0)
⊢ nhds 0 ≤ Filter.comap (⇑(constantCoeff σ α)) (nhds 0)

State before:
case a
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.atTop ≤ Filter.comap (fun n => f ^ n) (nhds 0)
⊢ nhds 0 ≤ Filter.comap (⇑(constantCoeff σ α)) (nhds 0)
Tactic:
rw [← Filter.map_le_iff_le_comap]
State after:
case a
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.atTop ≤ Filter.comap (fun n => f ^ n) (nhds 0)
⊢ Filter.map (⇑(constantCoeff σ α)) (nhds 0) ≤ nhds 0

State before:
case a
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.atTop ≤ Filter.comap (fun n => f ^ n) (nhds 0)
⊢ Filter.map (⇑(constantCoeff σ α)) (nhds 0) ≤ nhds 0
Tactic:
apply continuous_constantCoeff.continuousAt
State after:
no goals

State before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : Filter.Tendsto (fun n => (constantCoeff σ α) (f ^ n)) Filter.atTop (nhds 0)
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
simp only [Filter.tendsto_def] at this
State after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
⊢ IsNilpotent ((constantCoeff σ α) f)

State before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
specialize this {0} _
State after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
⊢ {0} ∈ nhds 0

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

State before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
⊢ {0} ∈ nhds 0

σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' {0} ∈ Filter.atTop
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
suffices  ∀ x : α, {x} ∈ nhds x by exact this 0
State after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
⊢ ∀ (x : α), {x} ∈ nhds x

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

State before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
⊢ ∀ (x : α), {x} ∈ nhds x

σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' {0} ∈ Filter.atTop
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
rw [← discreteTopology_iff_singleton_mem_nhds]
State after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
⊢ DiscreteTopology α

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

State before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
⊢ DiscreteTopology α

σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' {0} ∈ Filter.atTop
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
infer_instance
State after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' {0} ∈ Filter.atTop
⊢ IsNilpotent ((constantCoeff σ α) f)

State before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' {0} ∈ Filter.atTop
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
simp only [map_pow, Filter.mem_atTop_sets, ge_iff_le, Set.mem_preimage,
  Set.mem_singleton_iff] at this
State after:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∃ a, ∀ (b : ℕ), a ≤ b → (constantCoeff σ α) f ^ b = 0
⊢ IsNilpotent ((constantCoeff σ α) f)

State before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this : ∃ a, ∀ (b : ℕ), a ≤ b → (constantCoeff σ α) f ^ b = 0
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
obtain ⟨m, hm⟩ := this
State after:
case intro
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → (constantCoeff σ α) f ^ b = 0
⊢ IsNilpotent ((constantCoeff σ α) f)

State before:
case intro
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → (constantCoeff σ α) f ^ b = 0
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
use m
State after:
case h
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → (constantCoeff σ α) f ^ b = 0
⊢ (constantCoeff σ α) f ^ m = 0

State before:
case h
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → (constantCoeff σ α) f ^ b = 0
⊢ (constantCoeff σ α) f ^ m = 0
Tactic:
apply hm m (le_refl m)
State after:
no goals

State before:
σ : Type u_2
α : Type u_1
inst✝⁴ : DecidableEq σ
inst✝³ : TopologicalSpace α
inst✝² : CommRing α
inst✝¹ : TopologicalRing α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
h : Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
this✝ : ∀ s ∈ nhds 0, (fun n => (constantCoeff σ α) (f ^ n)) ⁻¹' s ∈ Filter.atTop
this : ∀ (x : α), {x} ∈ nhds x
⊢ {0} ∈ nhds 0
Tactic:
exact this 0
State after:
no goals