Theorem: MvPowerSeries.EvalDomain.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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto (fun s => φ (a s)) Filter.cofinite (nhds 0)
Tactic:
apply Filter.Tendsto.comp
State after:
case hg
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto ⇑φ ?y (nhds 0)

case hf
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto (fun s => a s) Filter.cofinite ?y

case y
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter R

State before:
case hg
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto ⇑φ ?y (nhds 0)

case hf
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto (fun s => a s) Filter.cofinite ?y

case y
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter R
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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ 0 = φ 0

case hf
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto (fun s => a s) Filter.cofinite (nhds 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ 0 = φ 0

case hf
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto (fun s => a s) Filter.cofinite (nhds 0)
Tactic:
rw [RingHom.map_zero]
State after:
case hf
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto (fun s => a s) Filter.cofinite (nhds 0)

State before:
case hf
σ : 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 ⇑φ
a : σ → R
ha : EvalDomain a
⊢ Filter.Tendsto (fun s => a s) Filter.cofinite (nhds 0)
Tactic:
exact ha.tendsto_zero
State after:
no goals