Theorem: Polynomial.rTensorAlgHom_toLinearMap (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
⊢ (rTensorAlgHom R N S).toLinearMap = ↑(rTensorLinearEquiv R N S)
Tactic:
ext d n e
State after:
case a.h.h.h.a
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
d : ℕ
n : N
e : ℕ
⊢ (((AlgebraTensorModule.curry (rTensorAlgHom R N S).toLinearMap ∘ₗ monomial d) 1) n).coeff e =
    (((AlgebraTensorModule.curry ↑(rTensorLinearEquiv R N S) ∘ₗ monomial d) 1) n).coeff e

State before:
case a.h.h.h.a
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
d : ℕ
n : N
e : ℕ
⊢ (((AlgebraTensorModule.curry (rTensorAlgHom R N S).toLinearMap ∘ₗ monomial d) 1) n).coeff e =
    (((AlgebraTensorModule.curry ↑(rTensorLinearEquiv R N S) ∘ₗ monomial d) 1) n).coeff e
Tactic:
simp only [coe_comp, Function.comp_apply, AlgebraTensorModule.curry_apply, curry_apply,
  LinearMap.coe_restrictScalars, AlgHom.toLinearMap_apply, LinearEquiv.coe_coe]
State after:
case a.h.h.h.a
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
d : ℕ
n : N
e : ℕ
⊢ ((rTensorAlgHom R N S) ((monomial d) 1 ⊗ₜ[R] n)).coeff e =
    ((rTensorLinearEquiv R N S) ((monomial d) 1 ⊗ₜ[R] n)).coeff e

State before:
case a.h.h.h.a
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
d : ℕ
n : N
e : ℕ
⊢ ((rTensorAlgHom R N S) ((monomial d) 1 ⊗ₜ[R] n)).coeff e =
    ((rTensorLinearEquiv R N S) ((monomial d) 1 ⊗ₜ[R] n)).coeff e
Tactic:
rw [rTensorAlgHom_coeff_apply_tmul, rTensorLinearEquiv_coeff_tmul]
State after:
no goals