Theorem: MvPowerSeries.Continuous.on_scalars (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 ⇑φ
ε : MvPowerSeries σ R →+* S
hε : Continuous ⇑ε
⊢ Continuous ⇑(ε.comp (C σ R))
Tactic:
simp only [RingHom.coe_comp]
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 ⇑φ
ε : MvPowerSeries σ R →+* S
hε : Continuous ⇑ε
⊢ Continuous (⇑ε ∘ ⇑(C σ R))

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 ⇑φ
ε : MvPowerSeries σ R →+* S
hε : Continuous ⇑ε
⊢ Continuous (⇑ε ∘ ⇑(C σ R))
Tactic:
exact Continuous.comp hε MvPowerSeries.continuous_C
State after:
no goals