Theorem: PowerSeries.scale_algHom_comp (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✝¹
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a✝ : S⟦X⟧
ha : SubstDomain a✝
b✝ : MvPowerSeries υ T
hb : SubstDomain b✝
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a b : A
⊢ (scale_algHom R a).comp (scale_algHom R b) = scale_algHom R (a * b)
Tactic:
simp only [scale_algHom]
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✝¹
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a✝ : S⟦X⟧
ha : SubstDomain a✝
b✝ : MvPowerSeries υ T
hb : SubstDomain b✝
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a b : A
⊢ (MvPowerSeries.scale_algHom R (Function.const Unit a)).comp (MvPowerSeries.scale_algHom R (Function.const Unit b)) =
    MvPowerSeries.scale_algHom R (Function.const Unit (a * b))

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✝¹
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a✝ : S⟦X⟧
ha : SubstDomain a✝
b✝ : MvPowerSeries υ T
hb : SubstDomain b✝
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a b : A
⊢ (MvPowerSeries.scale_algHom R (Function.const Unit a)).comp (MvPowerSeries.scale_algHom R (Function.const Unit b)) =
    MvPowerSeries.scale_algHom R (Function.const Unit (a * b))
Tactic:
rw [MvPowerSeries.scale_algHom_comp]
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✝¹
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a✝ : S⟦X⟧
ha : SubstDomain a✝
b✝ : MvPowerSeries υ T
hb : SubstDomain b✝
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a b : A
⊢ MvPowerSeries.scale_algHom R (Function.const Unit a * Function.const Unit b) =
    MvPowerSeries.scale_algHom R (Function.const Unit (a * b))

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✝¹
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
a✝ : S⟦X⟧
ha : SubstDomain a✝
b✝ : MvPowerSeries υ T
hb : SubstDomain b✝
a' : MvPowerSeries τ S
ha' : SubstDomain a'
b' : τ → MvPowerSeries υ T
hb' : MvPowerSeries.SubstDomain b'
a b : A
⊢ MvPowerSeries.scale_algHom R (Function.const Unit a * Function.const Unit b) =
    MvPowerSeries.scale_algHom R (Function.const Unit (a * b))
Tactic:
rfl
State after:
no goals