Theorem: TensorProduct.rTensor_smul' (DividedPowers/PolynomialMap/Homogeneous.lean)

State before:
R✝ : Type u_1
inst✝¹⁷ : CommSemiring R✝
M✝ : Type u_2
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R✝ M✝
R : Type u_3
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : Semiring S
inst✝¹² : Algebra R S
M : Type u_5
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module S M
inst✝⁸ : IsScalarTower R S M
N : Type u_6
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
P : Type u_7
inst✝³ : AddCommMonoid P
inst✝² : Module R P
Q : Type u_8
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[S] N
s : S
t : M ⊗[R] P
⊢ (rTensor P (↑R f)) (s • t) = s • (rTensor P (↑R f)) t
Tactic:
have : rTensor P (f.restrictScalars R) = (IsLinearMap.mk' _
  (TensorProduct.map_isLinearMap_of_left f LinearMap.id)).restrictScalars R := rfl
State after:
R✝ : Type u_1
inst✝¹⁷ : CommSemiring R✝
M✝ : Type u_2
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R✝ M✝
R : Type u_3
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : Semiring S
inst✝¹² : Algebra R S
M : Type u_5
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module S M
inst✝⁸ : IsScalarTower R S M
N : Type u_6
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
P : Type u_7
inst✝³ : AddCommMonoid P
inst✝² : Module R P
Q : Type u_8
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[S] N
s : S
t : M ⊗[R] P
this : rTensor P (↑R f) = ↑R (IsLinearMap.mk' ⇑(map (↑R f) LinearMap.id) ⋯)
⊢ (rTensor P (↑R f)) (s • t) = s • (rTensor P (↑R f)) t

State before:
R✝ : Type u_1
inst✝¹⁷ : CommSemiring R✝
M✝ : Type u_2
inst✝¹⁶ : AddCommMonoid M✝
inst✝¹⁵ : Module R✝ M✝
R : Type u_3
inst✝¹⁴ : CommSemiring R
S : Type u_4
inst✝¹³ : Semiring S
inst✝¹² : Algebra R S
M : Type u_5
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module S M
inst✝⁸ : IsScalarTower R S M
N : Type u_6
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
P : Type u_7
inst✝³ : AddCommMonoid P
inst✝² : Module R P
Q : Type u_8
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[S] N
s : S
t : M ⊗[R] P
this : rTensor P (↑R f) = ↑R (IsLinearMap.mk' ⇑(map (↑R f) LinearMap.id) ⋯)
⊢ (rTensor P (↑R f)) (s • t) = s • (rTensor P (↑R f)) t
Tactic:
rw [this, coe_restrictScalars, map_smul, IsLinearMap.mk'_apply]
State after:
no goals