Theorem: MvPowerSeries.aeval_coe (DividedPowers/ForMathlib/MvPowerSeries/Evaluation.lean)

State before:
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
p : MvPolynomial σ R
⊢ (aeval ha) ↑p = (MvPolynomial.aeval a) p
Tactic:
simp only [coe_aeval, eval₂_coe (continuous_algebraMap R S) ha, aeval_def]
State after:
no goals