Theorem: MvPowerSeries.comp_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
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ε.comp (aeval ha) = aeval ⋯
Tactic:
apply DFunLike.coe_injective
State after:
case a
σ : 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
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ (fun f => ⇑f) (ε.comp (aeval ha)) = (fun f => ⇑f) (aeval ⋯)

State before:
case a
σ : 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
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ (fun f => ⇑f) (ε.comp (aeval ha)) = (fun f => ⇑f) (aeval ⋯)
Tactic:
simp only [AlgHom.coe_comp, coe_aeval ha]
State after:
case a
σ : 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
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ⇑ε ∘ eval₂ (algebraMap R S) a = ⇑(aeval ⋯)

State before:
case a
σ : 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
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ⇑ε ∘ eval₂ (algebraMap R S) a = ⇑(aeval ⋯)
Tactic:
erw [comp_eval₂ (continuous_algebraMap R S) ha hε]
State after:
case a
σ : 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
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ eval₂ (ε.comp (algebraMap R S)) (⇑ε.toRingHom ∘ a) = ⇑(aeval ⋯)

State before:
case a
σ : 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
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ eval₂ (ε.comp (algebraMap R S)) (⇑ε.toRingHom ∘ a) = ⇑(aeval ⋯)
Tactic:
apply congr_arg₂
State after:
case a.hx
σ : 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
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ε.comp (algebraMap R S) = algebraMap R T

case a.hy
σ : 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
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ⇑ε.toRingHom ∘ a = fun n => (fun s => ε.toRingHom (a s)) n

State before:
case a.hx
σ : 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
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ε.comp (algebraMap R S) = algebraMap R T

case a.hy
σ : 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
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ⇑ε.toRingHom ∘ a = fun n => (fun s => ε.toRingHom (a s)) n
Tactic:
simp only [AlgHom.toRingHom_eq_coe, AlgHom.comp_algebraMap_of_tower]
State after:
case a.hy
σ : 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
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ⇑ε.toRingHom ∘ a = fun n => (fun s => ε.toRingHom (a s)) n

State before:
case a.hy
σ : 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
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ⇑ε.toRingHom ∘ a = fun n => (fun s => ε.toRingHom (a s)) n
Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe]
State after:
case a.hy
σ : 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
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ⇑ε ∘ a = fun n => ε (a n)

State before:
case a.hy
σ : 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
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ⇑ε ∘ a = fun n => ε (a n)
Tactic:
ext
State after:
case a.hy.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 : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
x✝ : σ
⊢ (⇑ε ∘ a) x✝ = ε (a x✝)

State before:
case a.hy.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 : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
x✝ : σ
⊢ (⇑ε ∘ a) x✝ = ε (a x✝)
Tactic:
rfl
State after:
no goals