Theorem: MvPowerSeries.comp_subst (DividedPowers/ForMathlib/MvPowerSeries/Substitutions.lean)

State before:
σ : Type u_1
inst✝¹⁸ : DecidableEq σ
A : Type u_2
inst✝¹⁷ : CommSemiring A
R : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : Algebra A R
τ : Type u_4
inst✝¹⁴ : DecidableEq τ
S : Type u_5
inst✝¹³ : CommRing S
inst✝¹² : Algebra A S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
T : Type u_6
inst✝⁹ : CommRing T
inst✝⁸ : UniformSpace T
inst✝⁷ : T2Space T
inst✝⁶ : CompleteSpace T
inst✝⁵ : UniformAddGroup T
inst✝⁴ : TopologicalRing T
inst✝³ : LinearTopology T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ε : MvPowerSeries τ S →ₐ[R] T
this✝ : UniformSpace R := ⊥
this : UniformSpace S := ⊥
hε : Continuous ⇑ε
⊢ ⇑ε ∘ subst a = ⇑(aeval ⋯)
Tactic:
rw [← comp_substAlgHom ha hε, AlgHom.coe_comp, coe_substAlgHom]
State after:
no goals