-- 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_1 : M →ₗ[R] M'
p : R[X]
f g : PolynomialModule R M
e₁ :
  ((map R' f_1 : 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')
      (p • f) =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
      (((map R' f_1 : 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')
          f :
        PolynomialModule R' M')
e₂ :
  ((map R' f_1 : 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')
      (p • g) =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
      (((map R' f_1 : 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')
          g :
        PolynomialModule R' M')
add :
  ((map R' f_1 : 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')
      (p • f + p • g) =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
      (((map R' f_1 : 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')
          (f + g) :
        PolynomialModule R' M')
add₁ :
  HAdd.hAdd (α := PolynomialModule R' M') (β := PolynomialModule R' M')
      (((map R' f_1 : 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')
          (p • f) :
        PolynomialModule R' M')
      (((map R' f_1 : 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')
          (p • g) :
        PolynomialModule R' M') =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
      (((map R' f_1 : 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')
          (f + g) :
        PolynomialModule R' M')
add₂ :
  HAdd.hAdd (β := PolynomialModule R' M')
      (HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
        (((map R' f_1 : 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')
            f :
          PolynomialModule R' M'))
      (((map R' f_1 : 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')
          (p • g) :
        PolynomialModule R' M') =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
      (((map R' f_1 : 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')
          (f + g) :
        PolynomialModule R' M')
add₃ :
  HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
        (((map R' f_1 : 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')
            f :
          PolynomialModule R' M') +
      HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
        (((map R' f_1 : 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')
            g :
          PolynomialModule R' M') =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
      (((map R' f_1 : 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')
          (f + g) :
        PolynomialModule R' M')
add₄ :
  HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
        (((map R' f_1 : 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')
            f :
          PolynomialModule R' M') +
      HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
        (((map R' f_1 : 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')
            g :
          PolynomialModule R' M') =
    HSMul.hSMul (α := R'[X]) (Polynomial.map (algebraMap R R') p)
      (HAdd.hAdd (α := PolynomialModule R' M') (β := PolynomialModule R' M')
        (((map R' f_1 : 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')
            f :
          PolynomialModule R' M')
        (((map R' f_1 : 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')
            g :
          PolynomialModule R' M'))
⊢ ((map R' f_1 : 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')
      (p • (f + g)) =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
      (((map R' f_1 : 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')
          (f + g) :
        PolynomialModule R' M')
have add₅ : HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
      (((map R' f_1 : 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')
          f :
        PolynomialModule R' M') +
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
      (((map R' f_1 : 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')
          g :
        PolynomialModule R' M') =
  HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
      (((map R' f_1 : 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')
          f :
        PolynomialModule R' M') +
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
      (((map R' f_1 : 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')
          g :
        PolynomialModule R' M')
Tactic: rw [smul_add, map_add, e₁, e₂, map_add, smul_add]