Theorem: Polynomial.rTensorLinearEquiv_coeff_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✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
e : ℕ
⊢ ((rTensorLinearEquiv R N S) (p ⊗ₜ[R] n)).coeff e = p.coeff e ⊗ₜ[R] n
Tactic:
dsimp [coeff]
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✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
e : ℕ
⊢ ((rTensorLinearEquiv R N S) (p ⊗ₜ[R] n)).toFinsupp e = p.toFinsupp e ⊗ₜ[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✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
e : ℕ
⊢ ((rTensorLinearEquiv R N S) (p ⊗ₜ[R] n)).toFinsupp e = p.toFinsupp e ⊗ₜ[R] n
Tactic:
have h : (rTensorLinearEquiv R N S (p ⊗ₜ[R] n)).toFinsupp
  = TensorProduct.finsuppLeft' _ _ _ _ S (p.toFinsupp ⊗ₜ[R] n) := by
  rfl
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✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
e : ℕ
h : ((rTensorLinearEquiv R N S) (p ⊗ₜ[R] n)).toFinsupp = (finsuppLeft' R S N ℕ S) (p.toFinsupp ⊗ₜ[R] n)
⊢ ((rTensorLinearEquiv R N S) (p ⊗ₜ[R] n)).toFinsupp e = p.toFinsupp e ⊗ₜ[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✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
e : ℕ
h : ((rTensorLinearEquiv R N S) (p ⊗ₜ[R] n)).toFinsupp = (finsuppLeft' R S N ℕ S) (p.toFinsupp ⊗ₜ[R] n)
⊢ ((rTensorLinearEquiv R N S) (p ⊗ₜ[R] n)).toFinsupp e = p.toFinsupp e ⊗ₜ[R] n
Tactic:
rw [h, finsuppLeft'_apply, finsuppLeft_apply_tmul_apply]
State after:
no goals

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✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X]
n : N
e : ℕ
⊢ ((rTensorLinearEquiv R N S) (p ⊗ₜ[R] n)).toFinsupp = (finsuppLeft' R S N ℕ S) (p.toFinsupp ⊗ₜ[R] n)
Tactic:
rfl
State after:
no goals