Theorem: MvPowerSeries.hasSum_eval₂ (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 : σ →₀ ℕ
f : MvPowerSeries σ R
⊢ HasSum (fun d => φ ((coeff R d) f) * d.prod fun s e => a s ^ e) (eval₂ φ a f)
Tactic:
convert (hasSum_of_monomials_self f).map (eval₂Hom hφ ha) (continuous_eval₂ hφ ha) with d
State after:
case h.e'_5.h
σ : 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✝ : σ →₀ ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ (φ ((coeff R d) f) * d.prod fun s e => a s ^ e) = (⇑(eval₂Hom hφ ha) ∘ fun d => (monomial R d) ((coeff R d) f)) d

State before:
case h.e'_5.h
σ : 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✝ : σ →₀ ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ (φ ((coeff R d) f) * d.prod fun s e => a s ^ e) = (⇑(eval₂Hom hφ ha) ∘ fun d => (monomial R d) ((coeff R d) f)) d
Tactic:
simp only [Function.comp_apply, coe_eval₂Hom, ← MvPolynomial.coe_monomial, eval₂_coe hφ ha, eval₂_monomial]
State after:
no goals