Theorem: MvPowerSeries.subst_comp_subst (DividedPowers/ForMathlib/MvPowerSeries/Substitutions.lean)

State before:
σ : Type u_1
inst✝²³ : DecidableEq σ
A : Type u_2
inst✝²² : CommSemiring A
R : Type u_3
inst✝²¹ : CommRing R
inst✝²⁰ : Algebra A R
τ : Type u_4
inst✝¹⁹ : DecidableEq τ
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : UniformAddGroup T✝
inst✝⁹ : TopologicalRing T✝
inst✝⁸ : LinearTopology T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
ε : MvPowerSeries τ S →ₐ[R] T✝
υ : 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
b : τ → MvPowerSeries υ T
hb : SubstDomain b
⊢ subst b ∘ subst a = subst fun s => subst b (a s)
Tactic:
apply funext
State after:
case h
σ : Type u_1
inst✝²³ : DecidableEq σ
A : Type u_2
inst✝²² : CommSemiring A
R : Type u_3
inst✝²¹ : CommRing R
inst✝²⁰ : Algebra A R
τ : Type u_4
inst✝¹⁹ : DecidableEq τ
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : UniformAddGroup T✝
inst✝⁹ : TopologicalRing T✝
inst✝⁸ : LinearTopology T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
ε : MvPowerSeries τ S →ₐ[R] T✝
υ : 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
b : τ → MvPowerSeries υ T
hb : SubstDomain b
⊢ ∀ (x : MvPowerSeries σ R), (subst b ∘ subst a) x = subst (fun s => subst b (a s)) x

State before:
case h
σ : Type u_1
inst✝²³ : DecidableEq σ
A : Type u_2
inst✝²² : CommSemiring A
R : Type u_3
inst✝²¹ : CommRing R
inst✝²⁰ : Algebra A R
τ : Type u_4
inst✝¹⁹ : DecidableEq τ
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : UniformAddGroup T✝
inst✝⁹ : TopologicalRing T✝
inst✝⁸ : LinearTopology T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
ε : MvPowerSeries τ S →ₐ[R] T✝
υ : 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
b : τ → MvPowerSeries υ T
hb : SubstDomain b
⊢ ∀ (x : MvPowerSeries σ R), (subst b ∘ subst a) x = subst (fun s => subst b (a s)) x
Tactic:
simpa only [DFunLike.ext_iff, AlgHom.coe_comp, AlgHom.coe_restrictScalars', Function.comp_apply] using
  substAlgHom_comp_substAlgHom (R := R) ha hb
State after:
no goals