-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ 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
have 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)
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]
Cleared hypotheses: sn