-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
R' : Type u_4
M' : Type u_5
inst_3 : CommRing R'
inst_4 : AddCommGroup M'
inst_5 : Module R' M'
inst_6 : Module R M'
inst_7 : Algebra R R'
inst_8 : IsScalarTower R R' M'
f : M →ₗ[R] M'
i : ℕ
m : M
n : ℕ
a : R
single :
  ((map R' f : LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) (PolynomialModule R M) (PolynomialModule R' M')) :
        (a : PolynomialModule R M) → PolynomialModule R' M')
      ((PolynomialModule.single R (n + i) : (a : M) → PolynomialModule R M) (a • m)) =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M')
      (Polynomial.map (algebraMap R R') ((monomial n : (a : R) → R[X]) a))
      (((map R' f : LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) (PolynomialModule R M) (PolynomialModule R' M')) :
            (a : PolynomialModule R M) → PolynomialModule R' M')
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m) :
        PolynomialModule R' M')
single₁ :
  (PolynomialModule.single R' (n + i) : (a : M') → PolynomialModule R' M') ((f : (a : M) → M') (a • m)) =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M')
      (Polynomial.map (algebraMap R R') ((monomial n : (a : R) → R[X]) a))
      (((map R' f : LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) (PolynomialModule R M) (PolynomialModule R' M')) :
            (a : PolynomialModule R M) → PolynomialModule R' M')
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m) :
        PolynomialModule R' M')
single₂ :
  (PolynomialModule.single R' (n + i) : (a : M') → PolynomialModule R' M') ((f : (a : M) → M') (a • m)) =
    HSMul.hSMul.{u_4, u_5, u_5} (α := R'[X]) (β := PolynomialModule R' M')
      ((monomial n : (a : R') → R'[X]) ((algebraMap R R' : (a : R) → R') a) : R'[X])
      (((map R' f : LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) (PolynomialModule R M) (PolynomialModule R' M')) :
            (a : PolynomialModule R M) → PolynomialModule R' M')
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m) :
        PolynomialModule R' M')
single₃ :
  (PolynomialModule.single R' (n + i) : (a : M') → PolynomialModule R' M') ((f : (a : M) → M') (a • m)) =
    HSMul.hSMul.{u_4, u_5, u_5} (α := R'[X]) (β := PolynomialModule R' M')
      ((monomial n : (a : R') → R'[X]) ((algebraMap R R' : (a : R) → R') a) : R'[X])
      ((PolynomialModule.single R' i : (a : M') → PolynomialModule R' M') ((f : (a : M) → M') m) :
        PolynomialModule R' M')
⊢ ((map R' f : LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) (PolynomialModule R M) (PolynomialModule R' M')) :
        (a : PolynomialModule R M) → PolynomialModule R' M')
      (HSMul.hSMul (α := R[X]) (β := PolynomialModule R M) ((monomial n : (a : R) → R[X]) a : R[X])
        ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M')
      (Polynomial.map (algebraMap R R') ((monomial n : (a : R) → R[X]) a))
      (((map R' f : LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) (PolynomialModule R M) (PolynomialModule R' M')) :
            (a : PolynomialModule R M) → PolynomialModule R' M')
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m) :
        PolynomialModule R' M')
have single₄ : Eq.{u_5 + 1} (α := PolynomialModule R' M')
  ((PolynomialModule.single R' (n + i) : (a : M') → PolynomialModule R' M') ((f : (a : M) → M') (a • m)) :
    PolynomialModule R' M')
  ((PolynomialModule.single R' (n + i) : (a : M') → PolynomialModule R' M')
      (HSMul.hSMul.{u_4, u_5, u_5} (α := R') (β := M') ((algebraMap R R' : (a : R) → R') a : R')
        ((f : (a : M) → M') m : M')) :
    PolynomialModule R' M')
Tactic: rw [monomial_smul_single, map_single, Polynomial.map_monomial, map_single,
        monomial_smul_single, f.map_smul, algebraMap_smul]