Theorem: MvPowerSeries.IsTopologicallyNilpotent.map (DividedPowers/ForMathlib/MvPowerSeries/Evaluation.lean)

State before:
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalRing R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalRing S
φ✝ : R →+* S
hφ✝ : Continuous ⇑φ✝
α : Type u_4
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : IsTopologicallyNilpotent a
⊢ IsTopologicallyNilpotent (φ a)
Tactic:
unfold IsTopologicallyNilpotent at ha ⊢
State after:
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalRing R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalRing S
φ✝ : R →+* S
hφ✝ : Continuous ⇑φ✝
α : Type u_4
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : Filter.Tendsto (fun n => a ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => φ a ^ n) Filter.atTop (nhds 0)

State before:
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalRing R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalRing S
φ✝ : R →+* S
hφ✝ : Continuous ⇑φ✝
α : Type u_4
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : Filter.Tendsto (fun n => a ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => φ a ^ n) Filter.atTop (nhds 0)
Tactic:
simp_rw [← map_pow]
State after:
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalRing R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalRing S
φ✝ : R →+* S
hφ✝ : Continuous ⇑φ✝
α : Type u_4
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : Filter.Tendsto (fun n => a ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => φ (a ^ n)) Filter.atTop (nhds 0)

State before:
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalRing R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalRing S
φ✝ : R →+* S
hφ✝ : Continuous ⇑φ✝
α : Type u_4
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : Filter.Tendsto (fun n => a ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun n => φ (a ^ n)) Filter.atTop (nhds 0)
Tactic:
apply Filter.Tendsto.comp _ ha
State after:
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalRing R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalRing S
φ✝ : R →+* S
hφ✝ : Continuous ⇑φ✝
α : Type u_4
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : Filter.Tendsto (fun n => a ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (⇑φ) (nhds 0) (nhds 0)

State before:
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalRing R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalRing S
φ✝ : R →+* S
hφ✝ : Continuous ⇑φ✝
α : Type u_4
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : Filter.Tendsto (fun n => a ^ n) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (⇑φ) (nhds 0) (nhds 0)
Tactic:
convert hφ.tendsto 0
State after:
case h.e'_5.h.e'_3
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalRing R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalRing S
φ✝ : R →+* S
hφ✝ : Continuous ⇑φ✝
α : Type u_4
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : Filter.Tendsto (fun n => a ^ n) Filter.atTop (nhds 0)
⊢ 0 = φ 0

State before:
case h.e'_5.h.e'_3
σ : Type u_1
inst✝¹⁰ : DecidableEq σ
R : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalRing R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalRing S
φ✝ : R →+* S
hφ✝ : Continuous ⇑φ✝
α : Type u_4
β : Type u_5
inst✝³ : CommRing α
inst✝² : CommRing β
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
φ : α →+* β
hφ : Continuous ⇑φ
a : α
ha : Filter.Tendsto (fun n => a ^ n) Filter.atTop (nhds 0)
⊢ 0 = φ 0
Tactic:
rw [map_zero]
State after:
no goals