Theorem: Polynomial.rTensor_apply_tmul_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
p : S[X]
n : N
i : ℕ
⊢ ((rTensor R N S) (p ⊗ₜ[R] n)) i = p.coeff i ⊗ₜ[R] n
Tactic:
simp only [rTensor, LinearEquiv.trans_apply, finsuppLeft'_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
i : ℕ
⊢ ((finsuppLeft R S N ℕ) ((rTensor' N (toFinsuppLinearEquiv S)) (p ⊗ₜ[R] n))) i = p.coeff i ⊗ₜ[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
i : ℕ
⊢ ((finsuppLeft R S N ℕ) ((rTensor' N (toFinsuppLinearEquiv S)) (p ⊗ₜ[R] n))) i = p.coeff i ⊗ₜ[R] n
Tactic:
simp only [LinearEquiv.rTensor'_apply, LinearEquiv.rTensor, congr_tmul,
  LinearEquiv.restrictScalars_apply, LinearEquiv.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
i : ℕ
⊢ ((finsuppLeft R S N ℕ) ((toFinsuppLinearEquiv S) p ⊗ₜ[R] n)) i = p.coeff i ⊗ₜ[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
i : ℕ
⊢ ((finsuppLeft R S N ℕ) ((toFinsuppLinearEquiv S) p ⊗ₜ[R] n)) i = p.coeff i ⊗ₜ[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
i : ℕ
⊢ ((finsuppLeft R S N ℕ) (p.toFinsupp ⊗ₜ[R] n)) i = p.coeff i ⊗ₜ[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
i : ℕ
⊢ ((finsuppLeft R S N ℕ) (p.toFinsupp ⊗ₜ[R] n)) i = p.coeff i ⊗ₜ[R] n
Tactic:
rw [finsuppLeft_apply_tmul_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
i : ℕ
⊢ p.toFinsupp i ⊗ₜ[R] n = p.coeff i ⊗ₜ[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
i : ℕ
⊢ p.toFinsupp i ⊗ₜ[R] n = p.coeff i ⊗ₜ[R] n
Tactic:
rfl
State after:
no goals