awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ 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) (x ^ i) ((algebraMap S R : (a : S) → R) m : 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)
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)
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)
single₂ :
  HMul.hMul (β := R) (x ^ i) ((algebraMap S R : (a : S) → R) m : 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)
⊢ 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) (x ^ i) ((algebraMap S R : (a : S) → R) m : R) =
  (eval x : (a : PolynomialModule R R) → R)
    ((PolynomialModule.single R i : (a : R) → PolynomialModule R R) ((Algebra.linearMap S R : (a : S) → R) m) :
      PolynomialModule 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)
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)
single₂ :
  HMul.hMul (β := R) (x ^ i) ((algebraMap S R : (a : S) → R) m : 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)
single₃ :
  HMul.hMul (β := R) (x ^ i) ((algebraMap S R : (a : S) → R) m : R) =
    (eval x : (a : PolynomialModule R R) → R)
      ((PolynomialModule.single R i : (a : R) → PolynomialModule R R) ((Algebra.linearMap S R : (a : S) → R) m) :
        PolynomialModule 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) (x ^ i) ((algebraMap S R : (a : S) → R) m : R) =
  (eval x : (a : PolynomialModule R R) → R)
    ((PolynomialModule.single R i : (a : R) → PolynomialModule R R) ((algebraMap S R : (a : S) → R) m) :
      PolynomialModule 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)
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)
single₂ :
  HMul.hMul (β := R) (x ^ i) ((algebraMap S R : (a : S) → R) m : 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)
single₃ :
  HMul.hMul (β := R) (x ^ i) ((algebraMap S R : (a : S) → R) m : R) =
    (eval x : (a : PolynomialModule R R) → R)
      ((PolynomialModule.single R i : (a : R) → PolynomialModule R R) ((Algebra.linearMap S R : (a : S) → R) m) :
        PolynomialModule R R)
single₄ :
  HMul.hMul (β := R) (x ^ i) ((algebraMap S R : (a : S) → R) m : R) =
    (eval x : (a : PolynomialModule R R) → R)
      ((PolynomialModule.single R i : (a : R) → PolynomialModule R R) ((algebraMap S R : (a : S) → R) m) :
        PolynomialModule 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) (x ^ i) ((algebraMap S R : (a : S) → R) m : R) =
  HSMul.hSMul (β := R) (x ^ i) ((algebraMap S R : (a : S) → R) m : 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)
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)
single₂ :
  HMul.hMul (β := R) (x ^ i) ((algebraMap S R : (a : S) → R) m : 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)
single₃ :
  HMul.hMul (β := R) (x ^ i) ((algebraMap S R : (a : S) → R) m : R) =
    (eval x : (a : PolynomialModule R R) → R)
      ((PolynomialModule.single R i : (a : R) → PolynomialModule R R) ((Algebra.linearMap S R : (a : S) → R) m) :
        PolynomialModule R R)
single₄ :
  HMul.hMul (β := R) (x ^ i) ((algebraMap S R : (a : S) → R) m : R) =
    (eval x : (a : PolynomialModule R R) → R)
      ((PolynomialModule.single R i : (a : R) → PolynomialModule R R) ((algebraMap S R : (a : S) → R) m) :
        PolynomialModule R R)
single₅ :
  HMul.hMul (β := R) (x ^ i) ((algebraMap S R : (a : S) → R) m : R) =
    HSMul.hSMul (β := R) (x ^ i) ((algebraMap S R : (a : S) → R) m : 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) (x ^ i) ((algebraMap S R : (a : S) → R) m : R) =
  HMul.hMul (β := R) (x ^ i) ((algebraMap S R : (a : S) → R) m : 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
f : PolynomialModule S S
x : R
⊢ 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)
have zero : Eq (α := R) ((aeval x : (a : S[X]) → R) ((equivPolynomial : (a : PolynomialModule S S) → S[X]) 0) : R)
  ((eval x : (a : PolynomialModule R R) → R)
      ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R) 0) :
    R)
Tactic: induction f using induction_linear with
  | zero => simp
  | add f g e₁ e₂ => simp_rw [map_add, e₁, e₂]
  | single i m => rw [equivPolynomial_single, aeval_monomial, mul_comm, map_single,
      Algebra.linearMap_apply, eval_single, smul_eq_mul]
Cleared hypotheses: f
-- 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
f : PolynomialModule S S
x : R
zero :
  Eq (α := R) ((aeval x : (a : S[X]) → R) ((equivPolynomial : (a : PolynomialModule S S) → S[X]) 0) : R)
    ((eval x : (a : PolynomialModule R R) → R)
        ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R) 0) :
      R)
⊢ 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)
have add : ∀ (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)
Tactic: induction f using induction_linear with
  | zero => simp
  | add f g e₁ e₂ => simp_rw [map_add, e₁, e₂]
  | single i m => rw [equivPolynomial_single, aeval_monomial, mul_comm, map_single,
      Algebra.linearMap_apply, eval_single, smul_eq_mul]
Cleared hypotheses: f
-- 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
f : PolynomialModule S S
x : R
zero :
  Eq (α := R) ((aeval x : (a : S[X]) → R) ((equivPolynomial : (a : PolynomialModule S S) → S[X]) 0) : R)
    ((eval x : (a : PolynomialModule R R) → R)
        ((map R (Algebra.linearMap S R) : (a : PolynomialModule S S) → PolynomialModule R R) 0) :
      R)
add :
  ∀ (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)
⊢ 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)
have single : ∀ (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)
Tactic: induction f using induction_linear with
  | zero => simp
  | add f g e₁ e₂ => simp_rw [map_add, e₁, e₂]
  | single i m => rw [equivPolynomial_single, aeval_monomial, mul_comm, map_single,
      Algebra.linearMap_apply, eval_single, smul_eq_mul]
Cleared hypotheses: f
-- 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]
i : ℕ
m : M
⊢ (comp p : (a : PolynomialModule R M) → PolynomialModule R M) ((single R i : (a : M) → PolynomialModule R M) m) =
    HSMul.hSMul (β := PolynomialModule R M) (p ^ i)
      ((single R 0 : (a : M) → PolynomialModule R M) m : PolynomialModule R M)
have rw : HSMul.hSMul (β := PolynomialModule R M) (p ^ i)
    ((lsingle R 0 : (a : M) → PolynomialModule R M) m : PolynomialModule R M) =
  HSMul.hSMul (β := PolynomialModule R M) (p ^ i)
    ((single R 0 : (a : M) → PolynomialModule R M) m : PolynomialModule R M)
Tactic: rw [comp_apply, map_single, eval_single]
-- 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
⊢ Eq (α := M)
    ((eval r : (a : PolynomialModule R M) → M)
        ((comp p : (a : PolynomialModule R M) → PolynomialModule R M) q : PolynomialModule R M) :
      M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) q : M)
have rw : Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) q : M)
  ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) q : M)
Tactic: rw [← LinearMap.comp_apply]
-- 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
f g : PolynomialModule R M
e₁ :
  Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) f : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) f : M)
e₂ :
  Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) g : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) g : M)
⊢ Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) (f + g) : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) (f + g) : M)
have add : HAdd.hAdd (α := M) (β := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) f : M)
    ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) g : M) =
  HAdd.hAdd (α := M) (β := M) ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) f : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) g : 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
p : R[X]
r : R
f g : PolynomialModule R M
e₁ :
  Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) f : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) f : M)
e₂ :
  Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) g : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) g : M)
add :
  HAdd.hAdd (α := M) (β := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) f : M)
      ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) g : M) =
    HAdd.hAdd (α := M) (β := M) ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) f : M)
      ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) g : M)
⊢ Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) (f + g) : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) (f + g) : M)
have add₁ : HAdd.hAdd (α := M) (β := M) ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) f : M)
    ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) g : M) =
  HAdd.hAdd (α := M) (β := M) ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) f : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) g : 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
p : R[X]
r : R
i : ℕ
m : M
⊢ Eq (α := M)
    ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M)
        ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
      M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M)
        ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
      M)
have single : Polynomial.eval r p ^ i • HPow.hPow (β := ℕ) r 0 • m = Polynomial.eval r p ^ i • m
Tactic: rw [LinearMap.comp_apply, comp_single, eval_single, eval_smul, eval_single, eval_pow]
-- 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
⊢ Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) q : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) q : M)
have zero : Eq.{u_2 + 1} (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) 0 : M)
  ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) 0 : M)
Tactic: induction q using induction_linear with
  | zero => simp_rw [map_zero]
  | add _ _ e₁ e₂ => simp_rw [map_add, e₁, e₂]
  | single i m =>
    rw [LinearMap.comp_apply, comp_single, eval_single, eval_smul, eval_single, eval_pow]
    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 :
  Eq.{u_2 + 1} (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) 0 : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) 0 : M)
⊢ Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) q : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) q : M)
have add : ∀ (f g : PolynomialModule R M)
  (e₁ :
    Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) f : M)
      ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) f : M))
  (e₂ :
    Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) g : M)
      ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) g : M)),
  Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) (f + g) : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) (f + g) : M)
Tactic: induction q using induction_linear with
  | zero => simp_rw [map_zero]
  | add _ _ e₁ e₂ => simp_rw [map_add, e₁, e₂]
  | single i m =>
    rw [LinearMap.comp_apply, comp_single, eval_single, eval_smul, eval_single, eval_pow]
    module
Cleared hypotheses: q