-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
k : ℕ
sn : S ⊗[R] N
zero :
  HSMul.hSMul (β := TensorProduct.{u, v, u_3} R S[X] N) (HPow.hPow (α := S[X]) X k)
      ((rTensor N
            ((↑R :
                {S M M₂ : Type v} →
                  [inst : Semiring R] →
                    [inst_5 : Semiring S] →
                      [inst_6 : AddCommMonoid M] →
                        [inst_7 : AddCommMonoid M₂] →
                          [inst_8 : Module R M] →
                            [inst_9 : Module R M₂] →
                              [inst_10 : Module S M] →
                                [inst_11 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (monomial 0)) :
          (a : S ⊗[R] N) → S[X] ⊗[R] N)
        0) =
    (rTensor N
          ((↑R :
              {S M M₂ : Type v} →
                [inst : Semiring R] →
                  [inst_5 : Semiring S] →
                    [inst_6 : AddCommMonoid M] →
                      [inst_7 : AddCommMonoid M₂] →
                        [inst_8 : Module R M] →
                          [inst_9 : Module R M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (monomial k)) :
        (a : S ⊗[R] N) → S[X] ⊗[R] N)
      0
add :
  ∀ (x y : S ⊗[R] N)
    (hx :
      HSMul.hSMul (β := TensorProduct.{u, v, u_3} R S[X] N) (HPow.hPow (α := S[X]) X k)
          ((rTensor N
                  ((↑R :
                      {S M M₂ : Type v} →
                        [inst : Semiring R] →
                          [inst_5 : Semiring S] →
                            [inst_6 : AddCommMonoid M] →
                              [inst_7 : AddCommMonoid M₂] →
                                [inst_8 : Module R M] →
                                  [inst_9 : Module R M₂] →
                                    [inst_10 : Module S M] →
                                      [inst_11 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    (monomial 0)) :
                (a : S ⊗[R] N) → S[X] ⊗[R] N)
              x :
            TensorProduct.{u, v, u_3} R S[X] N) =
        (rTensor N
              ((↑R :
                  {S M M₂ : Type v} →
                    [inst : Semiring R] →
                      [inst_5 : Semiring S] →
                        [inst_6 : AddCommMonoid M] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R M] →
                              [inst_9 : Module R M₂] →
                                [inst_10 : Module S M] →
                                  [inst_11 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (monomial k)) :
            (a : S ⊗[R] N) → S[X] ⊗[R] N)
          x)
    (hy :
      HSMul.hSMul (β := TensorProduct.{u, v, u_3} R S[X] N) (HPow.hPow (α := S[X]) X k)
          ((rTensor N
                  ((↑R :
                      {S M M₂ : Type v} →
                        [inst : Semiring R] →
                          [inst_5 : Semiring S] →
                            [inst_6 : AddCommMonoid M] →
                              [inst_7 : AddCommMonoid M₂] →
                                [inst_8 : Module R M] →
                                  [inst_9 : Module R M₂] →
                                    [inst_10 : Module S M] →
                                      [inst_11 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    (monomial 0)) :
                (a : S ⊗[R] N) → S[X] ⊗[R] N)
              y :
            TensorProduct.{u, v, u_3} R S[X] N) =
        (rTensor N
              ((↑R :
                  {S M M₂ : Type v} →
                    [inst : Semiring R] →
                      [inst_5 : Semiring S] →
                        [inst_6 : AddCommMonoid M] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R M] →
                              [inst_9 : Module R M₂] →
                                [inst_10 : Module S M] →
                                  [inst_11 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (monomial k)) :
            (a : S ⊗[R] N) → S[X] ⊗[R] N)
          y),
    HSMul.hSMul (β := TensorProduct.{u, v, u_3} R S[X] N) (HPow.hPow (α := S[X]) X k)
        ((rTensor N
                ((↑R :
                    {S M M₂ : Type v} →
                      [inst : Semiring R] →
                        [inst_5 : Semiring S] →
                          [inst_6 : AddCommMonoid M] →
                            [inst_7 : AddCommMonoid M₂] →
                              [inst_8 : Module R M] →
                                [inst_9 : Module R M₂] →
                                  [inst_10 : Module S M] →
                                    [inst_11 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  (monomial 0)) :
              (a : S ⊗[R] N) → S[X] ⊗[R] N)
            (x + y) :
          TensorProduct.{u, v, u_3} R S[X] N) =
      (rTensor N
            ((↑R :
                {S M M₂ : Type v} →
                  [inst : Semiring R] →
                    [inst_5 : Semiring S] →
                      [inst_6 : AddCommMonoid M] →
                        [inst_7 : AddCommMonoid M₂] →
                          [inst_8 : Module R M] →
                            [inst_9 : Module R M₂] →
                              [inst_10 : Module S M] →
                                [inst_11 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (monomial k)) :
          (a : S ⊗[R] N) → S[X] ⊗[R] N)
        (x + y)
tmul :
  ∀ (s : S) (n : N),
    HSMul.hSMul (β := TensorProduct.{u, v, u_3} R S[X] N) (HPow.hPow (α := S[X]) X k)
        ((rTensor N
                ((↑R :
                    {S M M₂ : Type v} →
                      [inst : Semiring R] →
                        [inst_5 : Semiring S] →
                          [inst_6 : AddCommMonoid M] →
                            [inst_7 : AddCommMonoid M₂] →
                              [inst_8 : Module R M] →
                                [inst_9 : Module R M₂] →
                                  [inst_10 : Module S M] →
                                    [inst_11 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  (monomial 0)) :
              (a : S ⊗[R] N) → S[X] ⊗[R] N)
            (s ⊗ₜ[R] n) :
          TensorProduct.{u, v, u_3} R S[X] N) =
      (rTensor N
            ((↑R :
                {S M M₂ : Type v} →
                  [inst : Semiring R] →
                    [inst_5 : Semiring S] →
                      [inst_6 : AddCommMonoid M] →
                        [inst_7 : AddCommMonoid M₂] →
                          [inst_8 : Module R M] →
                            [inst_9 : Module R M₂] →
                              [inst_10 : Module S M] →
                                [inst_11 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (monomial k)) :
          (a : S ⊗[R] N) → S[X] ⊗[R] N)
        (s ⊗ₜ[R] n)
⊢ HSMul.hSMul (β := TensorProduct.{u, v, u_3} R S[X] N) (HPow.hPow (α := S[X]) X k)
      ((rTensor N
              ((↑R :
                  {S M M₂ : Type v} →
                    [inst : Semiring R] →
                      [inst_5 : Semiring S] →
                        [inst_6 : AddCommMonoid M] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R M] →
                              [inst_9 : Module R M₂] →
                                [inst_10 : Module S M] →
                                  [inst_11 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                (monomial 0)) :
            (a : S ⊗[R] N) → S[X] ⊗[R] N)
          sn :
        TensorProduct.{u, v, u_3} R S[X] N) =
    (rTensor N
          ((↑R :
              {S M M₂ : Type v} →
                [inst : Semiring R] →
                  [inst_5 : Semiring S] →
                    [inst_6 : AddCommMonoid M] →
                      [inst_7 : AddCommMonoid M₂] →
                        [inst_8 : Module R M] →
                          [inst_9 : Module R M₂] →
                            [inst_10 : Module S M] →
                              [inst_11 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (monomial k)) :
        (a : S ⊗[R] N) → S[X] ⊗[R] N)
      sn

Tactic:
induction sn using TensorProduct.induction_on with
  | zero => simp
  | add x y hx hy => simp [hx, hy]
  | tmul s n =>
    simp only [rTensor_tmul, coe_restrictScalars, monomial_zero_left]
    rw [smul_tmul', smul_eq_mul, mul_comm, C_mul_X_pow_eq_monomial]

Premises used: LinearMap.rTensor_tmul, Polynomial.C_mul_X_pow_eq_monomial, LinearMap.coe_restrictScalars, TensorProduct.smul_tmul', mul_comm, Polynomial.monomial_zero_left, TensorProduct.tmul, smul_eq_mul