Theorem: MvPowerSeries.hasSum_aeval (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
f : MvPowerSeries σ R
⊢ HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((aeval ha) f)
Tactic:
have := hasSum_eval₂ (continuous_algebraMap R S) ha f
State after:
σ : 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
f : MvPowerSeries σ R
this : HasSum (fun d => (algebraMap R S) ((coeff R d) f) * d.prod fun s e => a s ^ e) (eval₂ (algebraMap R S) a f)
⊢ HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((aeval ha) f)

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
f : MvPowerSeries σ R
this : HasSum (fun d => (algebraMap R S) ((coeff R d) f) * d.prod fun s e => a s ^ e) (eval₂ (algebraMap R S) a f)
⊢ HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((aeval ha) f)
Tactic:
simp_rw [← smul_eq_mul, algebraMap_smul] at this
State after:
σ : 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
f : MvPowerSeries σ R
this : HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) (eval₂ (algebraMap R S) a f)
⊢ HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((aeval ha) f)

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
f : MvPowerSeries σ R
this : HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) (eval₂ (algebraMap R S) a f)
⊢ HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((aeval ha) f)
Tactic:
rw [coe_aeval]
State after:
σ : 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
f : MvPowerSeries σ R
this : HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) (eval₂ (algebraMap R S) a f)
⊢ HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) (eval₂ (algebraMap R S) a f)

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
f : MvPowerSeries σ R
this : HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) (eval₂ (algebraMap R S) a f)
⊢ HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) (eval₂ (algebraMap R S) a f)
Tactic:
exact this
State after:
no goals