awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
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
zero :
  (eval r : (a : PolynomialModule R M) → M) 0 =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) 0 : M)
zero₁ : 0 = HSMul.hSMul (β := M) (Polynomial.eval r p) 0
zero₂ zero₃ : Eq.{u_2 + 1} (α := M) 0 0
⊢ (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:
rw [smul_zero, map_zero, smul_zero]

Premises used: smul_zero, map_zero
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
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₁ :
  (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)
add :
  (eval r : (a : PolynomialModule R M) → M) (p • f + p • g) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
add₁ :
  HAdd.hAdd (α := M) (β := M) ((eval r : (a : PolynomialModule R M) → M) (p • f) : M)
      ((eval r : (a : PolynomialModule R M) → M) (p • g) : M) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
add₂ :
  HAdd.hAdd (β := M) (HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M))
      ((eval r : (a : PolynomialModule R M) → M) (p • g) : M) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
add₃ :
  HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M) +
      HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) (f + g) : M)
add₄ :
  HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M) +
      HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M) =
    Polynomial.eval r p •
      HAdd.hAdd (α := M) (β := M) ((eval r : (a : PolynomialModule R M) → M) f : M)
        ((eval r : (a : PolynomialModule R M) → M) g : M)
add₅ add₆ :
  HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M) +
      HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) g : M) =
    HSMul.hSMul (β := M) (Polynomial.eval r p) ((eval r : (a : PolynomialModule R M) → M) f : M) +
      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:
rw [smul_add, map_add, e₁, e₂, map_add, smul_add]

Premises used: map_add, smul_add
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
i : ℕ
m : M
n : ℕ
a : R
single : r ^ (n + i) • a • m = (a * r ^ n) • r ^ i • m
⊢ (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:
simp only [monomial_smul_single, Polynomial.eval_monomial, eval_single]

Premises used: PolynomialModule.monomial_smul_single, Polynomial.eval_monomial, PolynomialModule.eval_single
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
i : ℕ
m : M
n : ℕ
a : R
⊢ r ^ (n + i) • a • m = (a * r ^ n) • r ^ i • m

Tactic:
module
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
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)
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)
⊢ (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)

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

Premises used: PolynomialModule.monomial_smul_single, map_add, Polynomial.monomial, add_smul, Polynomial.eval_add, Polynomial.eval_monomial, PolynomialModule.eval_single
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
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)
single :
  ∀ (i : ℕ) (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)
⊢ (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)

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

Premises used: PolynomialModule.monomial_smul_single, smul_zero, map_zero, PolynomialModule.single, map_add, Polynomial.monomial, add_smul, Polynomial.eval_add, smul_add, Polynomial.eval_monomial, PolynomialModule.eval_single
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
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
⊢ 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:
simp_rw [map_zero]

Premises used: map_zero
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
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
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')
⊢ 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')
            ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m) :
          PolynomialModule R' M') :
      M')
    ((f : (a : M) → M')
        ((eval r : (a : PolynomialModule R M) → M)
            ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
          M) :
      M')

Tactic:
simp only [map_single, eval_single, f.map_smul]

Premises used: LinearMap.map_smul, PolynomialModule.map_single, PolynomialModule.eval_single
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
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
⊢ 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:
module
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
q : PolynomialModule R M
r : R
⊢ Eq (α := M)
    ((eval r : (a : PolynomialModule R M) → M)
        ((map R f : (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)

Tactic:
eval_map R f q r

Premises used: PolynomialModule.eval_map
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_6
inst_1 : CommRing S
inst_2 : Algebra S R
x : R
⊢ 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:
simp
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
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)
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)
⊢ 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:
simp_rw [map_add, e₁, e₂]

Premises used: map_add
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
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)
single₆ 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)
⊢ 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)

Tactic:
rw [equivPolynomial_single, aeval_monomial, mul_comm, map_single,
      Algebra.linearMap_apply, eval_single, smul_eq_mul]

Premises used: Algebra.linearMap_apply, PolynomialModule.equivPolynomial_single, mul_comm, Polynomial.aeval_monomial, smul_eq_mul, PolynomialModule.map_single, PolynomialModule.eval_single
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
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)
single :
  ∀ (i : ℕ) (m : S),
    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)
⊢ 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)

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]

Premises used: Algebra.linearMap_apply, PolynomialModule.single, map_add, PolynomialModule.equivPolynomial_single, mul_comm, Polynomial.aeval_monomial, smul_eq_mul, PolynomialModule.map_single, PolynomialModule.eval_single
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
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
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)
⊢ (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)

Tactic:
rw [comp_apply, map_single, eval_single]

Premises used: PolynomialModule.comp_apply, PolynomialModule.map_single, PolynomialModule.eval_single
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
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
⊢ 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:
rfl
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
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
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)
⊢ 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)

Tactic:
rw [← LinearMap.comp_apply]

Premises used: LinearMap.comp_apply
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
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
⊢ 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:
simp_rw [map_zero]

Premises used: map_zero