Theorem: MvPowerSeries.scale_algHom_one (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
⊢ scale_algHom R (Function.const σ 1) = AlgHom.id R (MvPowerSeries σ R)
Tactic:
rw [DFunLike.ext_iff]
State after:
σ : 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), (scale_algHom R (Function.const σ 1)) x = (AlgHom.id R (MvPowerSeries σ R)) x

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
⊢ ∀ (x : MvPowerSeries σ R), (scale_algHom R (Function.const σ 1)) x = (AlgHom.id R (MvPowerSeries σ R)) x
Tactic:
intro f
State after:
σ : 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
f : MvPowerSeries σ R
⊢ (scale_algHom R (Function.const σ 1)) f = (AlgHom.id R (MvPowerSeries σ R)) f

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
f : MvPowerSeries σ R
⊢ (scale_algHom R (Function.const σ 1)) f = (AlgHom.id R (MvPowerSeries σ R)) f
Tactic:
simp only [Function.const_one, coe_scale_algHom, AlgHom.coe_id, id_eq, scale_one]
State after:
no goals