Theorem: Polynomial.rTensor_apply_tmul (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
p : S[X]
n : N
⊢ (rTensor R N S) (p ⊗ₜ[R] n) = p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)
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
p : S[X]
n : N
⊢ (finsuppLeft R S N ℕ)
      ((TensorProduct.congr (LinearEquiv.restrictScalars R (toFinsuppLinearEquiv S)) (LinearEquiv.refl R N))
        (p ⊗ₜ[R] n)) =
    p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)

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
p : S[X]
n : N
⊢ (finsuppLeft R S N ℕ)
      ((TensorProduct.congr (LinearEquiv.restrictScalars R (toFinsuppLinearEquiv S)) (LinearEquiv.refl R N))
        (p ⊗ₜ[R] n)) =
    p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)
Tactic:
simp only [congr_tmul, LinearEquiv.restrictScalars_apply, refl_apply]
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
p : S[X]
n : N
⊢ (finsuppLeft R S N ℕ) ((toFinsuppLinearEquiv S) p ⊗ₜ[R] n) = p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)

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
p : S[X]
n : N
⊢ (finsuppLeft R S N ℕ) ((toFinsuppLinearEquiv S) p ⊗ₜ[R] n) = p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)
Tactic:
simp only [toFinsuppLinearEquiv, RingEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe,
  Equiv.invFun_as_coe, LinearEquiv.coe_mk, toFinsuppIso_apply]
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
p : S[X]
n : N
⊢ (finsuppLeft R S N ℕ) (p.toFinsupp ⊗ₜ[R] n) = p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)

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
p : S[X]
n : N
⊢ (finsuppLeft R S N ℕ) (p.toFinsupp ⊗ₜ[R] n) = p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)
Tactic:
rw [finsuppLeft_apply_tmul]
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
p : S[X]
n : N
⊢ (Finsupp.sum p.toFinsupp fun i m => Finsupp.single i (m ⊗ₜ[R] n)) = p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)

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
p : S[X]
n : N
⊢ (Finsupp.sum p.toFinsupp fun i m => Finsupp.single i (m ⊗ₜ[R] n)) = p.sum fun i m => Finsupp.single i (m ⊗ₜ[R] n)
Tactic:
rfl
State after:
no goals