-- 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
⊢ 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 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
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