Theorem: Polynomial.toPowerSeries_toMvPowerSeries (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
⊢ ↑p = ↑((Polynomial.aeval (MvPolynomial.X ())) p)
Tactic:
change (Polynomial.coeToPowerSeries.algHom R) p =
  (MvPolynomial.coeToMvPowerSeries.algHom R) (Polynomial.aeval (MvPolynomial.X () : MvPolynomial Unit R) p)
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
⊢ (Polynomial.coeToPowerSeries.algHom R) p =
    (MvPolynomial.coeToMvPowerSeries.algHom R) ((Polynomial.aeval (MvPolynomial.X ())) 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
⊢ (Polynomial.coeToPowerSeries.algHom R) p =
    (MvPolynomial.coeToMvPowerSeries.algHom R) ((Polynomial.aeval (MvPolynomial.X ())) p)
Tactic:
rw [← 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
⊢ (Polynomial.coeToPowerSeries.algHom R) p =
    ((MvPolynomial.coeToMvPowerSeries.algHom R).comp (Polynomial.aeval (MvPolynomial.X ()))) 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
⊢ (Polynomial.coeToPowerSeries.algHom R) p =
    ((MvPolynomial.coeToMvPowerSeries.algHom R).comp (Polynomial.aeval (MvPolynomial.X ()))) 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
⊢ Polynomial.coeToPowerSeries.algHom R =
    (MvPolynomial.coeToMvPowerSeries.algHom R).comp (Polynomial.aeval (MvPolynomial.X ()))

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
⊢ Polynomial.coeToPowerSeries.algHom R =
    (MvPolynomial.coeToMvPowerSeries.algHom R).comp (Polynomial.aeval (MvPolynomial.X ()))
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
⊢ (Polynomial.coeToPowerSeries.algHom R) Polynomial.X =
    ((MvPolynomial.coeToMvPowerSeries.algHom R).comp (Polynomial.aeval (MvPolynomial.X ()))) 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
⊢ (Polynomial.coeToPowerSeries.algHom R) Polynomial.X =
    ((MvPolynomial.coeToMvPowerSeries.algHom R).comp (Polynomial.aeval (MvPolynomial.X ()))) Polynomial.X
Tactic:
simp only [Polynomial.coeToPowerSeries.algHom_apply, Algebra.id.map_eq_id, Polynomial.coe_X,
  map_X]
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
⊢ X = ((MvPolynomial.coeToMvPowerSeries.algHom R).comp (Polynomial.aeval (MvPolynomial.X ()))) 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
⊢ X = ((MvPolynomial.coeToMvPowerSeries.algHom R).comp (Polynomial.aeval (MvPolynomial.X ()))) Polynomial.X
Tactic:
erw [AlgHom.comp_apply]
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
⊢ X = (MvPolynomial.coeToMvPowerSeries.algHom R) ((Polynomial.aeval (MvPolynomial.X ())) 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
⊢ X = (MvPolynomial.coeToMvPowerSeries.algHom R) ((Polynomial.aeval (MvPolynomial.X ())) Polynomial.X)
Tactic:
simp only [Polynomial.aeval_X, MvPolynomial.coeToMvPowerSeries.algHom_apply,
  Algebra.id.map_eq_id, MvPowerSeries.map_id, MvPolynomial.coe_X, RingHom.id_apply]
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
⊢ X = MvPowerSeries.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
⊢ X = MvPowerSeries.X ()
Tactic:
rfl
State after:
no goals