awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
D₁ D₂ : Derivation R R[X] A
h : Eq.{u_2 + 1} (α := A) ((D₁ : (a : R[X]) → A) X : A) ((D₂ : (a : R[X]) → A) X : A)
f : R[X]
⊢ f ∈ (↑R[ X] : Set R[X])

Tactic:
simp only [adjoin_X, Algebra.coe_top, Set.mem_univ]

Premises used: Algebra.coe_top, Set.mem_univ, Polynomial.adjoin_X
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
inst_4 : IsScalarTower R R[X] A
a b : A
h :
  Eq.{u_2 + 1} (α := A)
    (((((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A (a + b)) :
                  LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
                (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
              derivative' :
            Derivation R R[X] A) :
          (a : R[X]) → A)
        X :
      A)
    ((HAdd.hAdd (α := Derivation R R[X] A) (β := Derivation R R[X] A)
            (((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a) :
                    LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
                  (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
                derivative' :
              Derivation R R[X] A)
            (((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A b) :
                    LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
                  (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
                derivative' :
              Derivation R R[X] A) :
          (a : R[X]) → A)
        X :
      A)
⊢ ((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A (a + b)) :
          LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
        (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
      derivative' =
    HAdd.hAdd (α := Derivation R R[X] A) (β := Derivation R R[X] A)
      (((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a) :
              LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
            (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
          derivative' :
        Derivation R R[X] A)
      (((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A b) :
              LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
            (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
          derivative' :
        Derivation R R[X] A)

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
inst_4 : IsScalarTower R R[X] A
a b : A
⊢ Eq.{u_2 + 1} (α := A)
    (((((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A (a + b)) :
                  LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
                (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
              derivative' :
            Derivation R R[X] A) :
          (a : R[X]) → A)
        X :
      A)
    ((HAdd.hAdd (α := Derivation R R[X] A) (β := Derivation R R[X] A)
            (((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a) :
                    LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
                  (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
                derivative' :
              Derivation R R[X] A)
            (((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A b) :
                    LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
                  (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
                derivative' :
              Derivation R R[X] A) :
          (a : R[X]) → A)
        X :
      A)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
inst_4 : IsScalarTower R R[X] A
t : R
a : A
h :
  Eq.{u_2 + 1} (α := A)
    (((((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A (t • a)) :
                  LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
                (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
              derivative' :
            Derivation R R[X] A) :
          (a : R[X]) → A)
        X :
      A)
    ((HSMul.hSMul (α := R) (β := Derivation R R[X] A) ((RingHom.id R : (a : R) → R) t : R)
            (((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a) :
                    LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
                  (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
                derivative' :
              Derivation R R[X] A) :
          (a : R[X]) → A)
        X :
      A)
⊢ ((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A (t • a)) :
          LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
        (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
      derivative' =
    HSMul.hSMul (α := R) (β := Derivation R R[X] A) ((RingHom.id R : (a : R) → R) t : R)
      (((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a) :
              LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
            (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
          derivative' :
        Derivation R R[X] A)

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
inst_4 : IsScalarTower R R[X] A
t : R
a : A
⊢ Eq.{u_2 + 1} (α := A)
    (((((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A (t • a)) :
                  LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
                (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
              derivative' :
            Derivation R R[X] A) :
          (a : R[X]) → A)
        X :
      A)
    ((HSMul.hSMul (α := R) (β := Derivation R R[X] A) ((RingHom.id R : (a : R) → R) t : R)
            (((LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a) :
                    LinearMap (R := R[X]) (RingHom.id R[X]) (Derivation R R[X] R[X]) (Derivation R R[X] A)) :
                  (a : Derivation R R[X] R[X]) → Derivation R R[X] A)
                derivative' :
              Derivation R R[X] A) :
          (a : R[X]) → A)
        X :
      A)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
inst_4 : IsScalarTower R R[X] A
a : A
f : R[X]
⊢ ((((mkDerivation R : A →ₗ[R] Derivation R R[X] A) : (a : A) → Derivation R R[X] A) a : Derivation R R[X] A) :
        (a : R[X]) → A)
      f =
    HSMul.hSMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) a

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
inst_4 : IsScalarTower R R[X] A
a : A
⊢ ((((mkDerivation R : A →ₗ[R] Derivation R R[X] A) : (a : A) → Derivation R R[X] A) a : Derivation R R[X] A) :
        (a : R[X]) → A)
      X =
    a

Tactic:
simp [mkDerivation_apply]

Premises used: Polynomial.mkDerivation_apply
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
inst : CommSemiring R
h :
  Eq (α := R[X])
    ((((mkDerivation R : R[X] →ₗ[R] Derivation R R[X] R[X]) : (a : R[X]) → Derivation R R[X] R[X]) 1 :
          (a : R[X]) → R[X])
        X :
      R[X])
    ((derivative' : (a : R[X]) → R[X]) X : R[X])
⊢ Eq (α := Derivation R R[X] R[X])
    (((mkDerivation R : R[X] →ₗ[R] Derivation R R[X] R[X]) : (a : R[X]) → Derivation R R[X] R[X]) 1) derivative'

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := R[X])
    ((((mkDerivation R : R[X] →ₗ[R] Derivation R R[X] R[X]) : (a : R[X]) → Derivation R R[X] R[X]) 1 :
          (a : R[X]) → R[X])
        X :
      R[X])
    ((derivative' : (a : R[X]) → R[X]) X : R[X])

Tactic:
simp [derivative']

Premises used: Polynomial.derivative'
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
rw : Eq (α := R[X]) ((derivative' : (a : R[X]) → R[X]) f : R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X])
⊢ Eq (α := R[X])
    ((((mkDerivation R : R[X] →ₗ[R] Derivation R R[X] R[X]) : (a : R[X]) → Derivation R R[X] R[X]) 1 :
          (a : R[X]) → R[X])
        f :
      R[X])
    ((derivative : (a : R[X]) → R[X]) f : R[X])

Tactic:
rw [mkDerivation_one_eq_derivative']

Premises used: Polynomial.mkDerivation_one_eq_derivative'
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
⊢ Eq (α := R[X]) ((derivative' : (a : R[X]) → R[X]) f : R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X])

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
inst_4 : IsScalarTower R R[X] A
a : A
⊢ Eq (α := Derivation R R[X] A)
    (((mkDerivationEquiv R : A ≃ₗ[R] Derivation R R[X] A) : (a : A) → Derivation R R[X] A) a : Derivation R R[X] A)
    (((mkDerivation R : A →ₗ[R] Derivation R R[X] A) : (a : A) → Derivation R R[X] A) a : Derivation R R[X] A)

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module.{u_1, u_2} R[X] A
inst_4 : IsScalarTower R R[X] A
D : Derivation R R[X] A
⊢ Eq.{u_2 + 1} (α := A)
    (((LinearEquiv.symm (mkDerivationEquiv R) : Derivation R R[X] A ≃ₗ[R] A) : (a : Derivation R R[X] A) → A) D : A)
    ((D : (a : R[X]) → A) X : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
d : Derivation R A M
a : A
⊢ ∀ (x y : R[X]),
    (AEval.of R M a : (a_1 : M) → AEval R M a) ((d : (a : A) → M) ((aeval a : (a : R[X]) → A) (x + y) : A) : M) =
      HAdd.hAdd (α := AEval R M a) (β := AEval R M a)
        ((AEval.of R M a : (a_1 : M) → AEval R M a) ((d : (a : A) → M) ((aeval a : (a : R[X]) → A) x : A) : M) :
          AEval R M a)
        ((AEval.of R M a : (a_1 : M) → AEval R M a) ((d : (a : A) → M) ((aeval a : (a : R[X]) → A) y : A) : M) :
          AEval R M a)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
d : Derivation R A M
a : A
⊢ ∀ (m : R) (x : R[X]),
    (AEval.of R M a : (a_1 : M) → AEval R M a) ((d : (a : A) → M) ((aeval a : (a : R[X]) → A) (m • x) : A) : M) =
      HSMul.hSMul (α := R) (β := AEval R M a) ((RingHom.id R : (a : R) → R) m : R)
        ((AEval.of R M a : (a_1 : M) → AEval R M a) ((d : (a : A) → M) ((aeval a : (a : R[X]) → A) x : A) : M) :
          AEval R M a)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
d : Derivation R A M
a : A
⊢ Eq.{u_3 + 1} (α := AEval R M a)
    (({
          toFun := fun (f : R[X]) ↦
            (AEval.of R M a : (a_1 : M) → AEval R M a) ((d : (a : A) → M) ((aeval a : (a : R[X]) → A) f : A) : M),
          map_add' := ⋯, map_smul' := ⋯ } :
        (a_1 : R[X]) → AEval R M a)
      1)
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
d : Derivation R A M
a : A
⊢ ∀ (a_1 b : R[X]),
    ({
            toFun := fun (f : R[X]) ↦
              (AEval.of R M a : (a_2 : M) → AEval R M a) ((d : (a : A) → M) ((aeval a : (a : R[X]) → A) f : A) : M),
            map_add' := ⋯, map_smul' := ⋯ } :
          (a_2 : R[X]) → AEval R M a)
        (a_1 * b) =
      HSMul.hSMul (β := AEval R M a) a_1
          (({
                  toFun := fun (f : R[X]) ↦
                    (AEval.of R M a : (a_2 : M) → AEval R M a)
                      ((d : (a : A) → M) ((aeval a : (a : R[X]) → A) f : A) : M),
                  map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_1, u_1, u_3} (RingHom.id R) R[X] (AEval R M a) } :
                (a_2 : R[X]) → AEval R M a)
              b :
            AEval R M a) +
        HSMul.hSMul (β := AEval R M a) b
          (({
                  toFun := fun (f : R[X]) ↦
                    (AEval.of R M a : (a_2 : M) → AEval R M a)
                      ((d : (a : A) → M) ((aeval a : (a : R[X]) → A) f : A) : M),
                  map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_1, u_1, u_3} (RingHom.id R) R[X] (AEval R M a) } :
                (a_2 : R[X]) → AEval R M a)
              a_1 :
            AEval R M a)

Tactic:
simp [AEval.of_aeval_smul, -Derivation.map_aeval]

Premises used: Derivation.map_aeval, Module.AEval.of_aeval_smul
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
a : A
d : Derivation R A M
f : R[X]
⊢ ((d.compAEval a : Derivation.{u_1, u_1, u_3} R R[X] (AEval R M a)) : (a_1 : R[X]) → AEval R M a) f =
    HSMul.hSMul (α := R[X]) (β := AEval R M a) ((derivative : (a : R[X]) → R[X]) f : R[X])
      ((AEval.of R M a : (a_1 : M) → AEval R M a) ((d : (a : A) → M) a : M) : AEval R M a)

Tactic:
simpa using AEval.of_aeval_smul _ _ _

Premises used: Module.AEval.of_aeval_smul
-- Module: Mathlib.Algebra.Polynomial.Derivation
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
a : A
d : Derivation R A M
f : R[X]
⊢ (LinearEquiv.symm (AEval.of R M a) : (a : AEval R M a) → M)
      (((d.compAEval a : Derivation.{u_1, u_1, u_3} R R[X] (AEval R M a)) : (a_1 : R[X]) → AEval R M a) f :
        AEval R M a) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := A) (β := M)
      ((aeval a : (a : R[X]) → A) ((derivative : (a : R[X]) → R[X]) f : R[X]) : A) ((d : (a : A) → M) a : M)

Tactic:
simp [-compAEval_apply, compAEval_eq]

Premises used: Derivation.compAEval_eq, Derivation.compAEval_apply
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst : Semiring R
p q : R[X]
hf :
  ∀ (i : ℕ),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HMul.hMul (α := R) 0 (↑i : R)) : R[X])
        (HPow.hPow (α := R[X]) X (i - 1)) =
      0
h_add :
  ∀ (a : ℕ) (b₁ b₂ : R),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((b₁ + b₂) * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)) =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (b₁ * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (b₂ * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1))
⊢ ((p + q).sum fun (n : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) =
    HAdd.hAdd (α := R[X])
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
      (q.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))

Tactic:
rw [sum_add_index]

Premises used: Polynomial.sum_add_index
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst : Semiring R
p q : R[X]
⊢ ∀ (i : ℕ),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HMul.hMul (α := R) 0 (↑i : R)) : R[X])
        (HPow.hPow (α := R[X]) X (i - 1)) =
      0

Tactic:
simp only [add_mul, forall_const, map_add, zero_mul, map_zero]

Premises used: add_mul, MulZeroClass.zero_mul, map_zero, map_add, forall_const
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n : ℕ
inst : Semiring R
p q : R[X]
⊢ ∀ (a : ℕ) (b₁ b₂ : R),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((b₁ + b₂) * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)) =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (b₁ * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (b₂ * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1))

Tactic:
simp only [add_mul, forall_const, map_add, zero_mul, map_zero]

Premises used: add_mul, MulZeroClass.zero_mul, map_zero, map_add, forall_const
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a_1 b : R
n : ℕ
inst : Semiring R
a : R
p : R[X]
dsimp :
  ((a • p).sum fun (n : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) =
    HSMul.hSMul (β := R[X]) a
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
⊢ ((a • p).sum fun (n : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) =
    HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) a : R)
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a_1 b : R
n : ℕ
inst : Semiring R
a : R
p : R[X]
rw :
  (p.sum fun (n : ℕ) (a_2 : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a_2 * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) =
    HSMul.hSMul (β := R[X]) a
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
hf :
  ∀ (i : ℕ),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HMul.hMul (α := R) 0 (↑i : R)) : R[X])
        (HPow.hPow (α := R[X]) X (i - 1)) =
      0
⊢ ((a • p).sum fun (n : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) =
    HSMul.hSMul (β := R[X]) a
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))

Tactic:
rw [sum_smul_index]

Premises used: Polynomial.sum_smul_index
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a_1 b : R
n : ℕ
inst : Semiring R
a : R
p : R[X]
⊢ (p.sum fun (n : ℕ) (a_2 : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a_2 * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) =
    HSMul.hSMul (β := R[X]) a
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))

Tactic:
simp only [mul_sum, ← C_mul', mul_assoc, map_mul, forall_const, zero_mul, map_zero, sum]

Premises used: Finset.mul_sum, Polynomial.C_mul', MulZeroClass.zero_mul, mul_assoc, Polynomial.sum, map_zero, map_mul, forall_const
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a_1 b : R
n : ℕ
inst : Semiring R
a : R
p : R[X]
⊢ ∀ (i : ℕ),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HMul.hMul (α := R) 0 (↑i : R)) : R[X])
        (HPow.hPow (α := R[X]) X (i - 1)) =
      0

Tactic:
simp only [mul_sum, ← C_mul', mul_assoc, map_mul, forall_const, zero_mul, map_zero, sum]

Premises used: Finset.mul_sum, Polynomial.C_mul', MulZeroClass.zero_mul, mul_assoc, Polynomial.sum, map_zero, map_mul, forall_const
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X])
    (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)) :
      R[X])

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Polynomial.sum, Finset.sum, rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
rw :
  coeff
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
      n =
    p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
⊢ coeff ((derivative : (a : R[X]) → R[X]) p) n = p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
rw [derivative_apply]

Premises used: Polynomial.derivative_apply
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
simp :
  (p.sum fun (a : ℕ) (b : R) ↦ b * (↑a : R) * if n = a - 1 then 1 else 0) =
    p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
⊢ coeff
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
      n =
    p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
simp only [coeff_X_pow, coeff_sum, coeff_C_mul]

Premises used: Polynomial.coeff_X_pow, Polynomial.coeff_C_mul, Polynomial.coeff_sum
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
rw :
  (p.coeff (n + 1) * (↑(n + 1) : R) * if n = n + 1 - 1 then 1 else 0) = p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
h₀ : ∀ b ∈ p.support, b ≠ n + 1 → (p.coeff b * (↑b : R) * if n = b - 1 then 1 else 0) = 0
h₁ : n + 1 ∉ p.support → (p.coeff (n + 1) * (↑(n + 1) : R) * if n = n + 1 - 1 then 1 else 0) = 0
⊢ (p.sum fun (a : ℕ) (b : R) ↦ b * (↑a : R) * if n = a - 1 then 1 else 0) =
    p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
rw [sum, Finset.sum_eq_single (n + 1)]

Premises used: Polynomial.sum, Finset.sum_eq_single, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
simp : p.coeff (n + 1) * (↑(n + 1) : R) = p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
⊢ (p.coeff (n + 1) * (↑(n + 1) : R) * if n = n + 1 - 1 then 1 else 0) = p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
simp only [Nat.add_succ_sub_one, add_zero, mul_one, if_true]

Premises used: if_true, Nat.add_succ_sub_one, mul_one, add_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : p.coeff (n + 1) * (↑(n + 1) : R) = p.coeff (n + 1) * (↑(n + 1) : R)
⊢ p.coeff (n + 1) * (↑(n + 1) : R) = p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
n b : ℕ
h₀ : 0 ∈ p.support → 0 ≠ n + 1 → (p.coeff 0 * (↑0 : R) * if n = HSub.hSub (α := ℕ) 0 1 then 1 else 0) = 0
h₁ :
  ∀ (n_1 : ℕ),
    n_1 + 1 ∈ p.support →
      n_1 + 1 ≠ n + 1 → (p.coeff (n_1 + 1) * (↑(n_1 + 1) : R) * if n = n_1 + 1 - 1 then 1 else 0) = 0
⊢ b ∈ p.support → b ≠ n + 1 → (p.coeff b * (↑b : R) * if n = b - 1 then 1 else 0) = 0

Tactic:
cases b