awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
p : R[X]
r : R
i : ℕ
m : M
single :
  ∀ (p q : R[X])
    (e₁ :
      (eval r : (a : PolynomialModule R M) → M)
          (HSMul.hSMul (β := PolynomialModule R M) p
            ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
        HSMul.hSMul (β := M) (Polynomial.eval r p)
          ((eval r : (a : PolynomialModule R M) → M)
              ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
            M))
    (e₂ :
      (eval r : (a : PolynomialModule R M) → M)
          (HSMul.hSMul (β := PolynomialModule R M) q
            ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
        HSMul.hSMul (β := M) (Polynomial.eval r q)
          ((eval r : (a : PolynomialModule R M) → M)
              ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
            M)),
    (eval r : (a : PolynomialModule R M) → M)
        (HSMul.hSMul (β := PolynomialModule R M) (p + q)
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
      HSMul.hSMul (β := M) (Polynomial.eval r (p + q))
        ((eval r : (a : PolynomialModule R M) → M)
            ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
          M)
⊢ (eval r : (a : PolynomialModule R M) → M)
      (HSMul.hSMul (β := PolynomialModule R M) p
        ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (β := M) (Polynomial.eval r p)
      ((eval r : (a : PolynomialModule R M) → M)
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
have single₁ : ∀ (n : ℕ) (a : R),
  (eval r : (a : PolynomialModule R M) → 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 (β := M) (Polynomial.eval r ((monomial n : (a : R) → R[X]) a))
      ((eval r : (a : PolynomialModule R M) → M)
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
Tactic: induction p using Polynomial.induction_on' with
    | add _ _ e₁ e₂ => rw [add_smul, map_add, Polynomial.eval_add, e₁, e₂, add_smul]
    | monomial => simp only [monomial_smul_single, Polynomial.eval_monomial, eval_single]; module
Cleared hypotheses: p
-- 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
p : R[X]
q : PolynomialModule R M
r : R
⊢ (eval r : (a : PolynomialModule R M) → M) (p • q) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) q : M)
have zero : (eval r : (a : PolynomialModule R M) → M) (HSMul.hSMul (β := PolynomialModule R M) p 0) =
  HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) 0 : M)
Tactic: induction q using induction_linear with
  | zero => rw [smul_zero, map_zero, smul_zero]
  | add f g e₁ e₂ => rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
  | single i m =>
    induction p using Polynomial.induction_on' with
    | add _ _ e₁ e₂ => rw [add_smul, map_add, Polynomial.eval_add, e₁, e₂, add_smul]
    | monomial => simp only [monomial_smul_single, Polynomial.eval_monomial, eval_single]; module
Cleared hypotheses: q
-- 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
p : R[X]
q : PolynomialModule R M
r : R
zero :
  (eval r : (a : PolynomialModule R M) → M) (HSMul.hSMul (β := PolynomialModule R M) p 0) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) 0 : M)
⊢ (eval r : (a : PolynomialModule R M) → M) (p • q) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) q : M)
have add : ∀ (f g : PolynomialModule R M)
  (e₁ :
    (eval r : (a : PolynomialModule R M) → M) (p • f) =
      HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M))
  (e₂ :
    (eval r : (a : PolynomialModule R M) → M) (p • g) =
      HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M)),
  (eval r : (a : PolynomialModule R M) → M) (p • (f + g)) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
Tactic: induction q using induction_linear with
  | zero => rw [smul_zero, map_zero, smul_zero]
  | add f g e₁ e₂ => rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
  | single i m =>
    induction p using Polynomial.induction_on' with
    | add _ _ e₁ e₂ => rw [add_smul, map_add, Polynomial.eval_add, e₁, e₂, add_smul]
    | monomial => simp only [monomial_smul_single, Polynomial.eval_monomial, eval_single]; module
Cleared hypotheses: q
-- 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
p : R[X]
q : PolynomialModule R M
r : R
zero :
  (eval r : (a : PolynomialModule R M) → M) (HSMul.hSMul (β := PolynomialModule R M) p 0) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) 0 : M)
add :
  ∀ (f g : PolynomialModule R M)
    (e₁ :
      (eval r : (a : PolynomialModule R M) → M) (p • f) =
        HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M))
    (e₂ :
      (eval r : (a : PolynomialModule R M) → M) (p • g) =
        HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M)),
    (eval r : (a : PolynomialModule R M) → M) (p • (f + g)) =
      HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
⊢ (eval r : (a : PolynomialModule R M) → M) (p • q) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) q : M)
have single : ∀ (i : ℕ) (m : M),
  (eval r : (a : PolynomialModule R M) → M)
      (HSMul.hSMul (β := PolynomialModule R M) p
        ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (β := M) (Polynomial.eval r p)
      ((eval r : (a : PolynomialModule R M) → M)
          ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
Tactic: induction q using induction_linear with
  | zero => rw [smul_zero, map_zero, smul_zero]
  | add f g e₁ e₂ => rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
  | single i m =>
    induction p using Polynomial.induction_on' with
    | add _ _ e₁ e₂ => rw [add_smul, map_add, Polynomial.eval_add, e₁, e₂, add_smul]
    | monomial => simp only [monomial_smul_single, Polynomial.eval_monomial, eval_single]; module
Cleared hypotheses: q
-- 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'
r : R
f 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_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') :
      M')
    ((f_1 : (a : M) → M') ((eval r : (a : PolynomialModule R M) → M) f : 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_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') :
      M')
    ((f_1 : (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_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') :
      M')
    ((f_1 : (a : M) → M') ((eval r : (a : PolynomialModule R M) → M) (f + g) : M) : M')
have add : HAdd.hAdd (α := M') (β := M')
    (((eval ((algebraMap R R' : (a : R) → R') r) : PolynomialModule R' M' →ₗ[R'] M') :
          (a : PolynomialModule R' M') → 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') :
      M')
    (((eval ((algebraMap R R' : (a : R) → R') r) : PolynomialModule R' M' →ₗ[R'] M') :
          (a : PolynomialModule R' M') → 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') :
      M') =
  HAdd.hAdd (α := M') (β := M') ((f_1 : (a : M) → M') ((eval r : (a : PolynomialModule R M) → M) f : M) : M')
    ((f_1 : (a : M) → M') ((eval r : (a : PolynomialModule R M) → M) g : M) : M')
Tactic: simp_rw [map_add, e₁, e₂]
-- 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'
r : R
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')
have single : HSMul.hSMul (β := M') (HPow.hPow (α := R') ((algebraMap R R' : (a : R) → R') r : R') i) ((f : (a : M) → M') m : M') =
  HSMul.hSMul (β := M') (r ^ i) ((f : (a : M) → M') m : M')
Tactic: simp only [map_single, eval_single, f.map_smul]
-- 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
⊢ 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 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')
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
-- 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')
⊢ 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 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')
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
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_6
inst_1 : CommRing S
inst_2 : Algebra S R
x : R
f g : PolynomialModule S S
e₁ :
  Eq.{u_1 + 1} (α := R)
    ((aeval x : (a : S[X]) → R) ((equivPolynomial : (a : PolynomialModule S S) → S[X]) f : S[X]) : R)
    ((eval x : (a : PolynomialModule R R) → R)
        ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R) f : PolynomialModule R R) :
      R)
e₂ :
  Eq.{u_1 + 1} (α := R)
    ((aeval x : (a : S[X]) → R) ((equivPolynomial : (a : PolynomialModule S S) → S[X]) g : S[X]) : R)
    ((eval x : (a : PolynomialModule R R) → R)
        ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R) g : PolynomialModule R R) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((aeval x : (a : S[X]) → R) ((equivPolynomial : (a : PolynomialModule S S) → S[X]) (f + g) : S[X]) : R)
    ((eval x : (a : PolynomialModule R R) → R)
        ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R) (f + g) :
          PolynomialModule R R) :
      R)
have add : HAdd.hAdd (α := R) (β := R)
    ((aeval x : (a : S[X]) → R) ((equivPolynomial : (a : PolynomialModule S S) → S[X]) f : S[X]) : R)
    ((aeval x : (a : S[X]) → R) ((equivPolynomial : (a : PolynomialModule S S) → S[X]) g : S[X]) : R) =
  HAdd.hAdd (α := R) (β := R)
    ((eval x : (a : PolynomialModule R R) → R)
        ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R) f : PolynomialModule R R) :
      R)
    ((eval x : (a : PolynomialModule R R) → R)
        ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R) g : PolynomialModule R R) :
      R)
Tactic: simp_rw [map_add, e₁, e₂]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_6
inst_1 : CommRing S
inst_2 : Algebra S R
x : R
f g : PolynomialModule S S
e₁ :
  Eq.{u_1 + 1} (α := R)
    ((aeval x : (a : S[X]) → R) ((equivPolynomial : (a : PolynomialModule S S) → S[X]) f : S[X]) : R)
    ((eval x : (a : PolynomialModule R R) → R)
        ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R) f : PolynomialModule R R) :
      R)
e₂ :
  Eq.{u_1 + 1} (α := R)
    ((aeval x : (a : S[X]) → R) ((equivPolynomial : (a : PolynomialModule S S) → S[X]) g : S[X]) : R)
    ((eval x : (a : PolynomialModule R R) → R)
        ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R) g : PolynomialModule R R) :
      R)
add :
  HAdd.hAdd (α := R) (β := R)
      ((aeval x : (a : S[X]) → R) ((equivPolynomial : (a : PolynomialModule S S) → S[X]) f : S[X]) : R)
      ((aeval x : (a : S[X]) → R) ((equivPolynomial : (a : PolynomialModule S S) → S[X]) g : S[X]) : R) =
    HAdd.hAdd (α := R) (β := R)
      ((eval x : (a : PolynomialModule R R) → R)
          ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R) f :
            PolynomialModule R R) :
        R)
      ((eval x : (a : PolynomialModule R R) → R)
          ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R) g :
            PolynomialModule R R) :
        R)
⊢ Eq.{u_1 + 1} (α := R)
    ((aeval x : (a : S[X]) → R) ((equivPolynomial : (a : PolynomialModule S S) → S[X]) (f + g) : S[X]) : R)
    ((eval x : (a : PolynomialModule R R) → R)
        ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R) (f + g) :
          PolynomialModule R R) :
      R)
have add₁ : HAdd.hAdd (α := R) (β := R)
    ((eval x : (a : PolynomialModule R R) → R)
        ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R) f : PolynomialModule R R) :
      R)
    ((aeval x : (a : S[X]) → R) ((equivPolynomial : (a : PolynomialModule S S) → S[X]) g : S[X]) : R) =
  HAdd.hAdd (α := R) (β := R)
    ((eval x : (a : PolynomialModule R R) → R)
        ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R) f : PolynomialModule R R) :
      R)
    ((eval x : (a : PolynomialModule R R) → R)
        ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R) g : PolynomialModule R R) :
      R)
Tactic: simp_rw [map_add, e₁, e₂]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_6
inst_1 : CommRing S
inst_2 : Algebra S R
x : R
i : ℕ
m : S
⊢ Eq.{u_1 + 1} (α := R)
    ((aeval x : (a : S[X]) → R)
        ((equivPolynomial : (a : PolynomialModule S S) → S[X]) ((single S i : (a : S) → PolynomialModule S S) m) :
          S[X]) :
      R)
    ((eval x : (a : PolynomialModule R R) → R)
        ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R)
            ((single S i : (a : S) → PolynomialModule S S) m) :
          PolynomialModule R R) :
      R)
have single : Eq.{u_1 + 1} (α := R) ((aeval x : (a : S[X]) → R) ((monomial i : (a : S) → S[X]) m : S[X]) : R)
  ((eval x : (a : PolynomialModule R R) → R)
      ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R)
          ((single S i : (a : S) → PolynomialModule S S) m) :
        PolynomialModule R R) :
    R)
Tactic: rw [equivPolynomial_single, aeval_monomial, mul_comm, map_single,
      Algebra.linearMap_apply, eval_single, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_6
inst_1 : CommRing S
inst_2 : Algebra S R
x : R
i : ℕ
m : S
single :
  Eq.{u_1 + 1} (α := R) ((aeval x : (a : S[X]) → R) ((monomial i : (a : S) → S[X]) m : S[X]) : R)
    ((eval x : (a : PolynomialModule R R) → R)
        ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R)
            ((PolynomialModule.single S i : (a : S) → PolynomialModule S S) m) :
          PolynomialModule R R) :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((aeval x : (a : S[X]) → R)
        ((equivPolynomial : (a : PolynomialModule S S) → S[X])
            ((PolynomialModule.single S i : (a : S) → PolynomialModule S S) m) :
          S[X]) :
      R)
    ((eval x : (a : PolynomialModule R R) → R)
        ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R)
            ((PolynomialModule.single S i : (a : S) → PolynomialModule S S) m) :
          PolynomialModule R R) :
      R)
have single₁ : HMul.hMul (α := R) ((algebraMap S R : (a : S) → R) m : R) (x ^ i) =
  (eval x : (a : PolynomialModule R R) → R)
    ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R)
        ((PolynomialModule.single S i : (a : S) → PolynomialModule S S) m) :
      PolynomialModule R R)
Tactic: rw [equivPolynomial_single, aeval_monomial, mul_comm, map_single,
      Algebra.linearMap_apply, eval_single, smul_eq_mul]