Theorem: PowerSeries.substAlgHom_coe (DividedPowers/ForMathlib/MvPowerSeries/Substitutions.lean)

State before:
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
p : Polynomial R
⊢ (substAlgHom ha) ↑p = (Polynomial.aeval a) p
Tactic:
rw [p.toPowerSeries_toMvPowerSeries, substAlgHom]
State after:
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
p : Polynomial R
⊢ (MvPowerSeries.substAlgHom ⋯) ↑((Polynomial.aeval (MvPolynomial.X ())) p) = (Polynomial.aeval a) p

State before:
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
p : Polynomial R
⊢ (MvPowerSeries.substAlgHom ⋯) ↑((Polynomial.aeval (MvPolynomial.X ())) p) = (Polynomial.aeval a) p
Tactic:
erw [MvPowerSeries.coe_substAlgHom]
State after:
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
p : Polynomial R
⊢ MvPowerSeries.subst (fun x => a) ↑((Polynomial.aeval (MvPolynomial.X ())) p) = (Polynomial.aeval a) p

State before:
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
p : Polynomial R
⊢ MvPowerSeries.subst (fun x => a) ↑((Polynomial.aeval (MvPolynomial.X ())) p) = (Polynomial.aeval a) p
Tactic:
rw [MvPowerSeries.subst_coe ha.const, ← AlgHom.comp_apply]
State after:
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
p : Polynomial R
⊢ ((MvPolynomial.aeval fun x => a).comp (Polynomial.aeval (MvPolynomial.X ()))) p = (Polynomial.aeval a) p

State before:
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
p : Polynomial R
⊢ ((MvPolynomial.aeval fun x => a).comp (Polynomial.aeval (MvPolynomial.X ()))) p = (Polynomial.aeval a) p
Tactic:
apply AlgHom.congr_fun
State after:
case H
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
p : Polynomial R
⊢ (MvPolynomial.aeval fun x => a).comp (Polynomial.aeval (MvPolynomial.X ())) = Polynomial.aeval a

State before:
case H
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
p : Polynomial R
⊢ (MvPolynomial.aeval fun x => a).comp (Polynomial.aeval (MvPolynomial.X ())) = Polynomial.aeval a
Tactic:
apply Polynomial.algHom_ext
State after:
case H.hX
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
p : Polynomial R
⊢ ((MvPolynomial.aeval fun x => a).comp (Polynomial.aeval (MvPolynomial.X ()))) Polynomial.X =
    (Polynomial.aeval a) Polynomial.X

State before:
case H.hX
A : Type u_1
inst✝¹² : CommRing A
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : Algebra A R
τ : Type u_3
inst✝⁹ : DecidableEq τ
S : Type u_4
inst✝⁸ : CommRing S
inst✝⁷ : Algebra A S
inst✝⁶ : Algebra R S
inst✝⁵ : IsScalarTower A R S
υ : Type u_5
inst✝⁴ : DecidableEq υ
T : Type u_6
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a : MvPowerSeries τ S
ha : SubstDomain a
p : Polynomial R
⊢ ((MvPolynomial.aeval fun x => a).comp (Polynomial.aeval (MvPolynomial.X ()))) Polynomial.X =
    (Polynomial.aeval a) Polynomial.X
Tactic:
simp only [AlgHom.coe_comp, Function.comp_apply, Polynomial.aeval_X, MvPolynomial.aeval_X]
State after:
no goals