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

State before:
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
hf : IsNilpotent ((constantCoeff σ α) f)
⊢ Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
Tactic:
classical
obtain ⟨m, hm⟩ := hf
simp_rw [tendsto_iff_coeff_tendsto, coeff_zero]
exact fun d =>  tendsto_atTop_of_eventually_const fun n hn =>
  coeff_eq_zero_of_constantCoeff_nilpotent f m hm d n hn
State after:
no goals

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

State before:
case intro
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
m : ℕ
hm : (constantCoeff σ α) f ^ m = 0
⊢ Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
Tactic:
simp_rw [tendsto_iff_coeff_tendsto, coeff_zero]
State after:
case intro
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
m : ℕ
hm : (constantCoeff σ α) f ^ m = 0
⊢ ∀ (d : σ →₀ ℕ), Filter.Tendsto (fun i => (coeff α d) (f ^ i)) Filter.atTop (nhds 0)

State before:
case intro
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
m : ℕ
hm : (constantCoeff σ α) f ^ m = 0
⊢ ∀ (d : σ →₀ ℕ), Filter.Tendsto (fun i => (coeff α d) (f ^ i)) Filter.atTop (nhds 0)
Tactic:
exact fun d =>  tendsto_atTop_of_eventually_const fun n hn =>
  coeff_eq_zero_of_constantCoeff_nilpotent f m hm d n hn
State after:
no goals