Theorem: MvPowerSeries.comp_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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ⇑ε ∘ eval₂ φ a = eval₂ (ε.comp φ) (⇑ε ∘ a)
Tactic:
rw [← coe_eval₂Hom hφ ha, ← RingHom.coe_comp]
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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ⇑(ε.comp (eval₂Hom hφ ha)) = eval₂ (ε.comp φ) (⇑ε ∘ a)

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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ⇑(ε.comp (eval₂Hom hφ ha)) = eval₂ (ε.comp φ) (⇑ε ∘ a)
Tactic:
apply eval₂_unique
State after:
case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ Continuous ⇑(ε.comp (eval₂Hom hφ ha))

case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ∀ (p : MvPolynomial σ R), (ε.comp (eval₂Hom hφ ha)) ↑p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p

State before:
case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ Continuous ⇑(ε.comp (eval₂Hom hφ ha))

case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ∀ (p : MvPolynomial σ R), (ε.comp (eval₂Hom hφ ha)) ↑p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Tactic:
simp only [RingHom.coe_comp]
State after:
case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ Continuous (⇑ε ∘ ⇑(eval₂Hom hφ ha))

case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ∀ (p : MvPolynomial σ R), (ε.comp (eval₂Hom hφ ha)) ↑p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p

State before:
case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ Continuous (⇑ε ∘ ⇑(eval₂Hom hφ ha))

case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ∀ (p : MvPolynomial σ R), (ε.comp (eval₂Hom hφ ha)) ↑p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Tactic:
exact Continuous.comp hε (continuous_eval₂ hφ ha)
State after:
case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ∀ (p : MvPolynomial σ R), (ε.comp (eval₂Hom hφ ha)) ↑p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p

State before:
case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
⊢ ∀ (p : MvPolynomial σ R), (ε.comp (eval₂Hom hφ ha)) ↑p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Tactic:
intro p
State after:
case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ (ε.comp (eval₂Hom hφ ha)) ↑p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p

State before:
case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ (ε.comp (eval₂Hom hφ ha)) ↑p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Tactic:
simp only [RingHom.coe_comp, Function.comp_apply, eval₂_coe]
State after:
case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ ε ((eval₂Hom hφ ha) ↑p) = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p

State before:
case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ ε ((eval₂Hom hφ ha) ↑p) = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Tactic:
rw [coe_eval₂Hom hφ ha, eval₂_coe hφ ha, ← MvPolynomial.coe_eval₂Hom]
State after:
case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ ε ((MvPolynomial.eval₂Hom φ a) p) = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p

State before:
case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ ε ((MvPolynomial.eval₂Hom φ a) p) = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Tactic:
rw [← RingHom.comp_apply, MvPolynomial.comp_eval₂Hom]
State after:
case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ (MvPolynomial.eval₂Hom (ε.comp φ) fun i => ε (a i)) p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p

State before:
case 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 : σ →₀ ℕ
T : Type u_4
inst✝³ : CommRing T
inst✝² : UniformSpace T
inst✝¹ : LinearTopology T
inst✝ : T2Space T
ε : S →+* T
hε : Continuous ⇑ε
p : MvPolynomial σ R
⊢ (MvPolynomial.eval₂Hom (ε.comp φ) fun i => ε (a i)) p = MvPolynomial.eval₂ (ε.comp φ) (⇑ε ∘ a) p
Tactic:
rfl
State after:
no goals