Theorem: Polynomial.rTensor_apply (DividedPowers/ForMathlib/RingTheory/TensorProduct/Polynomial.lean)

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S[X] ⊗[R] N
d : ℕ
⊢ ((rTensor R N S) t) d = (LinearMap.rTensor N (↑R (lcoeff S d))) t
Tactic:
simp only [rTensor, LinearEquiv.trans_apply, finsuppLeft'_apply,
  LinearEquiv.rTensor'_apply, LinearEquiv.rTensor]
State after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S[X] ⊗[R] N
d : ℕ
⊢ ((finsuppLeft R S N ℕ)
        ((TensorProduct.congr (LinearEquiv.restrictScalars R (toFinsuppLinearEquiv S)) (LinearEquiv.refl R N)) t))
      d =
    (LinearMap.rTensor N (↑R (lcoeff S d))) t

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S[X] ⊗[R] N
d : ℕ
⊢ ((finsuppLeft R S N ℕ)
        ((TensorProduct.congr (LinearEquiv.restrictScalars R (toFinsuppLinearEquiv S)) (LinearEquiv.refl R N)) t))
      d =
    (LinearMap.rTensor N (↑R (lcoeff S d))) t
Tactic:
simp only [TensorProduct.congr, refl_toLinearMap, refl_symm, ofLinear_apply, finsuppLeft_apply,
  LinearMap.rTensor]
State after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S[X] ⊗[R] N
d : ℕ
⊢ (TensorProduct.map (Finsupp.lapply d) LinearMap.id)
      ((TensorProduct.map (↑(LinearEquiv.restrictScalars R (toFinsuppLinearEquiv S))) LinearMap.id) t) =
    (TensorProduct.map (↑R (lcoeff S d)) LinearMap.id) t

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S[X] ⊗[R] N
d : ℕ
⊢ (TensorProduct.map (Finsupp.lapply d) LinearMap.id)
      ((TensorProduct.map (↑(LinearEquiv.restrictScalars R (toFinsuppLinearEquiv S))) LinearMap.id) t) =
    (TensorProduct.map (↑R (lcoeff S d)) LinearMap.id) t
Tactic:
rw [← LinearMap.comp_apply, ← TensorProduct.map_comp]
State after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S[X] ⊗[R] N
d : ℕ
⊢ (TensorProduct.map (Finsupp.lapply d ∘ₗ ↑(LinearEquiv.restrictScalars R (toFinsuppLinearEquiv S)))
        (LinearMap.id ∘ₗ LinearMap.id))
      t =
    (TensorProduct.map (↑R (lcoeff S d)) LinearMap.id) t

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommMonoid P
inst✝² : Module R P
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
t : S[X] ⊗[R] N
d : ℕ
⊢ (TensorProduct.map (Finsupp.lapply d ∘ₗ ↑(LinearEquiv.restrictScalars R (toFinsuppLinearEquiv S)))
        (LinearMap.id ∘ₗ LinearMap.id))
      t =
    (TensorProduct.map (↑R (lcoeff S d)) LinearMap.id) t
Tactic:
rfl
State after:
no goals