Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹⁷ : CommRing R
inst✝¹⁶ : UniformSpace R
S : Type u_3
inst✝¹⁵ : CommRing S
inst✝¹⁴ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : IsUniformAddGroup R
inst✝¹¹ : IsUniformAddGroup S
inst✝¹⁰ : CompleteSpace S
inst✝⁹ : T2Space S
inst✝⁸ : IsTopologicalRing S
inst✝⁷ : IsLinearTopology S S
hφ : Continuous[inst✝¹⁶.toTopologicalSpace, inst✝¹⁴.toTopologicalSpace] ⇑φ
ha : HasEval a
T : Type u_4
inst✝⁶ : UniformSpace T
inst✝⁵ : CompleteSpace T
inst✝⁴ : T2Space T
inst✝³ : CommRing T
inst✝² : IsTopologicalRing T
inst✝¹ : IsLinearTopology T T
inst✝ : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst✝¹⁴.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑ε
⊢ ⇑ε ∘ eval₂ φ a = eval₂ (ε.comp φ) (⇑ε ∘ a)

Tactic:
apply eval₂_unique _ (ha.map hε)

Goal state after:
case hε
σ : Type u_1
R : Type u_2
inst✝¹⁷ : CommRing R
inst✝¹⁶ : UniformSpace R
S : Type u_3
inst✝¹⁵ : CommRing S
inst✝¹⁴ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : IsUniformAddGroup R
inst✝¹¹ : IsUniformAddGroup S
inst✝¹⁰ : CompleteSpace S
inst✝⁹ : T2Space S
inst✝⁸ : IsTopologicalRing S
inst✝⁷ : IsLinearTopology S S
hφ : Continuous[inst✝¹⁶.toTopologicalSpace, inst✝¹⁴.toTopologicalSpace] ⇑φ
ha : HasEval a
T : Type u_4
inst✝⁶ : UniformSpace T
inst✝⁵ : CompleteSpace T
inst✝⁴ : T2Space T
inst✝³ : CommRing T
inst✝² : IsTopologicalRing T
inst✝¹ : IsLinearTopology T T
inst✝ : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst✝¹⁴.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑ε
⊢ Continuous[instTopologicalSpace R, inst✝⁶.toTopologicalSpace] (⇑ε ∘ eval₂ φ a)

case h
σ : Type u_1
R : Type u_2
inst✝¹⁷ : CommRing R
inst✝¹⁶ : UniformSpace R
S : Type u_3
inst✝¹⁵ : CommRing S
inst✝¹⁴ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : IsUniformAddGroup R
inst✝¹¹ : IsUniformAddGroup S
inst✝¹⁰ : CompleteSpace S
inst✝⁹ : T2Space S
inst✝⁸ : IsTopologicalRing S
inst✝⁷ : IsLinearTopology S S
hφ : Continuous[inst✝¹⁶.toTopologicalSpace, inst✝¹⁴.toTopologicalSpace] ⇑φ
ha : HasEval a
T : Type u_4
inst✝⁶ : UniformSpace T
inst✝⁵ : CompleteSpace T
inst✝⁴ : T2Space T
inst✝³ : CommRing T
inst✝² : IsTopologicalRing T
inst✝¹ : IsLinearTopology T T
inst✝ : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst✝¹⁴.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑ε
⊢ ∀ (p : MvPolynomial σ R), (⇑ε ∘ eval₂ φ a) ↑p = MvPolynomial.eval₂ (ε.comp φ) (fun s ↦ ε (a s)) p

σ : Type u_1
R : Type u_2
inst✝¹⁷ : CommRing R
inst✝¹⁶ : UniformSpace R
S : Type u_3
inst✝¹⁵ : CommRing S
inst✝¹⁴ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝¹³ : IsTopologicalSemiring R
inst✝¹² : IsUniformAddGroup R
inst✝¹¹ : IsUniformAddGroup S
inst✝¹⁰ : CompleteSpace S
inst✝⁹ : T2Space S
inst✝⁸ : IsTopologicalRing S
inst✝⁷ : IsLinearTopology S S
hφ : Continuous[inst✝¹⁶.toTopologicalSpace, inst✝¹⁴.toTopologicalSpace] ⇑φ
ha : HasEval a
T : Type u_4
inst✝⁶ : UniformSpace T
inst✝⁵ : CompleteSpace T
inst✝⁴ : T2Space T
inst✝³ : CommRing T
inst✝² : IsTopologicalRing T
inst✝¹ : IsLinearTopology T T
inst✝ : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst✝¹⁴.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑ε
⊢ Continuous[inst✝¹⁶.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑(ε.comp φ)