-- 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'
q : PolynomialModule R M
r : R
zero :
  Eq (α := M')
    (((eval ((algebraMap R R' : (a : R) → R') r) : PolynomialModule R' M' →ₗ[R'] M') :
          (a : PolynomialModule R' M') → 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')
          0) :
      M')
    ((f : (a : M) → M') ((eval r : (a : PolynomialModule R M) → M) 0 : M) : M')
add :
  ∀ (f_1 g : PolynomialModule R M)
    (e₁ :
      Eq (α := M')
        (((eval ((algebraMap R R' : (a : R) → R') r) : PolynomialModule R' M' →ₗ[R'] M') :
              (a : PolynomialModule R' M') → 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')
                f_1 :
              PolynomialModule R' M') :
          M')
        ((f : (a : M) → M') ((eval r : (a : PolynomialModule R M) → M) f_1 : M) : M'))
    (e₂ :
      Eq (α := M')
        (((eval ((algebraMap R R' : (a : R) → R') r) : PolynomialModule R' M' →ₗ[R'] M') :
              (a : PolynomialModule R' M') → 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')
                g :
              PolynomialModule R' M') :
          M')
        ((f : (a : M) → M') ((eval r : (a : PolynomialModule R M) → M) g : M) : M')),
    Eq (α := M')
      (((eval ((algebraMap R R' : (a : R) → R') r) : PolynomialModule R' M' →ₗ[R'] M') :
            (a : PolynomialModule R' M') → 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')
              (f_1 + g) :
            PolynomialModule R' M') :
        M')
      ((f : (a : M) → M') ((eval r : (a : PolynomialModule R M) → M) (f_1 + g) : M) : M')
⊢ Eq (α := M')
    (((eval ((algebraMap R R' : (a : R) → R') r) : PolynomialModule R' M' →ₗ[R'] M') :
          (a : PolynomialModule R' M') → 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')
            q :
          PolynomialModule R' M') :
      M')
    ((f : (a : M) → M') ((eval r : (a : PolynomialModule R M) → M) q : M) : M')
have single : ∀ (i : ℕ) (m : M),
  Eq (α := M')
    (((eval ((algebraMap R R' : (a : R) → R') r) : PolynomialModule R' M' →ₗ[R'] M') :
          (a : PolynomialModule R' M') → 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')
            ((single R i : (a : M) → PolynomialModule R M) m) :
          PolynomialModule R' M') :
      M')
    ((f : (a : M) → M')
        ((eval r : (a : PolynomialModule R M) → M)
            ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
          M) :
      M')
Tactic: induction q using induction_linear with
  | zero => simp_rw [map_zero]
  | add f g e₁ e₂ => simp_rw [map_add, e₁, e₂]
  | single i m => simp only [map_single, eval_single, f.map_smul]; module
Cleared hypotheses: q