awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
IH :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * q) =
    ∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
succ :
  HAdd.hAdd (α := R[X])
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k] q))
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q)) =
    ∑ k ∈ range n.succ,
          n.choose k.succ •
            ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q) +
        HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q) +
      ∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q)
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 1] (p * q) =
    ∑ k ∈ range (n + 1).succ,
      (n + 1).choose k • ((⇑derivative : (a : R[X]) → R[X])^[n + 1 - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)

Tactic:
calc
      derivative^[n + 1] (p * q) =
          derivative (∑ k ∈ range n.succ,
              n.choose k • (derivative^[n - k] p * derivative^[k] q)) := by
        rw [Function.iterate_succ_apply', IH]
      _ = (∑ k ∈ range n.succ,
            n.choose k • (derivative^[n - k + 1] p * derivative^[k] q)) +
          ∑ k ∈ range n.succ,
            n.choose k • (derivative^[n - k] p * derivative^[k + 1] q) := by
        simp_rw [derivative_sum, derivative_smul, derivative_mul, Function.iterate_succ_apply',
          smul_add, sum_add_distrib]
      _ = (∑ k ∈ range n.succ,
                n.choose k.succ • (derivative^[n - k] p * derivative^[k + 1] q)) +
              1 • (derivative^[n + 1] p * derivative^[0] q) +
            ∑ k ∈ range n.succ, n.choose k • (derivative^[n - k] p * derivative^[k + 1] q) :=
        ?_
      _ = ((∑ k ∈ range n.succ, n.choose k • (derivative^[n - k] p * derivative^[k + 1] q)) +
              ∑ k ∈ range n.succ,
                n.choose k.succ • (derivative^[n - k] p * derivative^[k + 1] q)) +
            1 • (derivative^[n + 1] p * derivative^[0] q) := by
        rw [add_comm, add_assoc]
      _ = (∑ i ∈ range n.succ,
              (n + 1).choose (i + 1) • (derivative^[n + 1 - (i + 1)] p * derivative^[i + 1] q)) +
            1 • (derivative^[n + 1] p * derivative^[0] q) := by
        simp_rw [Nat.choose_succ_succ, Nat.succ_sub_succ, add_smul, sum_add_distrib]
      _ = ∑ k ∈ range n.succ.succ,
            n.succ.choose k • (derivative^[n.succ - k] p * derivative^[k] q) := by
        rw [sum_range_succ' _ n.succ, Nat.choose_zero_right, tsub_zero]

Premises used: Polynomial.derivative, Nat.choose, HMul.hMul, HSub.hSub, Nat.iterate, Finset.range, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat, Nat.succ, DFunLike.coe, Finset.sum
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
IH :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * q) =
    ∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
succ :
  ∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k] q) =
    ∑ k ∈ range n.succ,
        n.choose k.succ • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q) +
      HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q)
⊢ HAdd.hAdd (α := R[X])
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k] q))
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q)) =
    ∑ k ∈ range n.succ,
          n.choose k.succ •
            ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q) +
        HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q) +
      ∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q)

Tactic:
congr
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
IH :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * q) =
    ∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
⊢ ∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k] q) =
    ∑ k ∈ range n.succ,
        n.choose k.succ • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q) +
      HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q)

Tactic:
(sum_range_succ' _ _).trans (congr_arg₂ (· + ·) ?_ ?_)

Premises used: HAdd.hAdd, Finset.sum_range_succ', Eq.trans, congr_arg₂
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
IH :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * q) =
    ∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
succ :
  Eq.{u + 1} (α := R[X])
    (∑ k ∈ range n,
      n.choose (k + 1) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - (k + 1) + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q))
    (∑ k ∈ range n.succ,
      n.choose k.succ • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q))
succ₁ :
  n.choose 0 • ((⇑derivative : (a : R[X]) → R[X])^[n - 0 + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q) =
    HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q)
⊢ ∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k] q) =
    ∑ k ∈ range n.succ,
        n.choose k.succ • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q) +
      HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q)

Tactic:
refine (sum_range_succ' _ _).trans (congr_arg₂ (· + ·) ?_ ?_)

Premises used: HAdd.hAdd, Finset.sum_range_succ', Eq.trans, congr_arg₂
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
IH :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * q) =
    ∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
succ :
  Eq.{u + 1} (α := R[X])
    (∑ k ∈ range n,
      n.choose (k + 1) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - (k + 1) + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q))
    (∑ x ∈ range n,
      n.choose x.succ • ((⇑derivative : (a : R[X]) → R[X])^[n - x] p * (⇑derivative : (a : R[X]) → R[X])^[x + 1] q))
⊢ Eq.{u + 1} (α := R[X])
    (∑ k ∈ range n,
      n.choose (k + 1) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - (k + 1) + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q))
    (∑ k ∈ range n.succ,
      n.choose k.succ • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q))

Tactic:
rw [sum_range_succ, Nat.choose_succ_self, zero_smul, add_zero]

Premises used: zero_smul, add_zero, Nat.choose_succ_self, Finset.sum_range_succ
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
IH :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * q) =
    ∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
⊢ Eq.{u + 1} (α := R[X])
    (∑ k ∈ range n,
      n.choose (k + 1) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - (k + 1) + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q))
    (∑ x ∈ range n,
      n.choose x.succ • ((⇑derivative : (a : R[X]) → R[X])^[n - x] p * (⇑derivative : (a : R[X]) → R[X])^[x + 1] q))

Tactic:
sum_congr rfl fun k hk => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
IH :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * q) =
    ∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
succ :
  ∀ (k : ℕ) (hk : k ∈ range n),
    n.choose (k + 1) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - (k + 1) + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q) =
      n.choose k.succ • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q)
⊢ Eq.{u + 1} (α := R[X])
    (∑ k ∈ range n,
      n.choose (k + 1) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - (k + 1) + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q))
    (∑ x ∈ range n,
      n.choose x.succ • ((⇑derivative : (a : R[X]) → R[X])^[n - x] p * (⇑derivative : (a : R[X]) → R[X])^[x + 1] q))

Tactic:
refine sum_congr rfl fun k hk => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
IH :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * q) =
    ∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
k : ℕ
hk : k ∈ range n
⊢ k < n

Tactic:
rw [mem_range] at hk

Premises used: Finset.mem_range
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
IH :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * q) =
    ∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
k : ℕ
hk : k < n
succ : n - (k + 1) + 1 = n - k
⊢ n.choose (k + 1) •
      ((⇑derivative : (a : R[X]) → R[X])^[n - (k + 1) + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q) =
    n.choose k.succ • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q)

Tactic:
congr
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
IH :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * q) =
    ∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
k : ℕ
hk : k < n
⊢ n - (k + 1) + 1 = n - k

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
IH :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * q) =
    ∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
succ :
  HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n - 0 + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q) =
    HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q)
succ₁ succ₂ :
  HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q) =
    HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q)
⊢ n.choose 0 • ((⇑derivative : (a : R[X]) → R[X])^[n - 0 + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q) =
    HSMul.hSMul (α := ℕ) 1 ((⇑derivative : (a : R[X]) → R[X])^[n + 1] p * (⇑derivative : (a : R[X]) → R[X])^[0] q)

Tactic:
rw [Nat.choose_zero_right, tsub_zero]

Premises used: tsub_zero, Nat.choose_zero_right
-- 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 : R[X]
i : ℕ
contrapose :
  i ∉ range (p.natDegree + 1) → Eq.{u + 1} (α := R[X]) ((fun (x : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x] p) i) 0
⊢ Ne.{u + 1} (α := R[X]) ((fun (x : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x] p) i) 0 → i ∈ range (p.natDegree + 1)

Tactic:
contrapose
-- 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 : R[X]
i : ℕ
⊢ i ∉ range (p.natDegree + 1) → Eq.{u + 1} (α := R[X]) ((fun (x : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x] p) i) 0

Tactic:
simp_all [iterate_derivative_eq_zero]

Premises used: Polynomial.iterate_derivative_eq_zero
-- 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
x x_1 : R[X]
h :
  ∀ (a n : ℕ),
    Eq.{u + 1} (α := R)
      (coeff
        ((Finsupp.onFinset (range ((x + x_1).natDegree + 1))
              (fun (x_2 : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x_2] (x + x_1)) ⋯ :
            (a : ℕ) → R[X])
          a)
        n)
      (coeff
        ((HAdd.hAdd (α := ℕ →₀ R[X])
              (Finsupp.onFinset (range (x.natDegree + 1)) (fun (x_2 : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x_2] x) ⋯)
              (Finsupp.onFinset (range (x_1.natDegree + 1)) (fun (x : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x] x_1)
                ⋯) :
            (a : ℕ) → R[X])
          a)
        n)
⊢ Finsupp.onFinset (range ((x + x_1).natDegree + 1)) (fun (x_2 : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x_2] (x + x_1))
      ⋯ =
    HAdd.hAdd (α := ℕ →₀ R[X])
      (Finsupp.onFinset (range (x.natDegree + 1)) (fun (x_2 : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x_2] x) ⋯)
      (Finsupp.onFinset (range (x_1.natDegree + 1)) (fun (x : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x] x_1) ⋯)

Tactic:
ext
-- 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
x x_1 : R[X]
a_1 n_1 : ℕ
⊢ Eq.{u + 1} (α := R)
    (coeff
      ((Finsupp.onFinset (range ((x + x_1).natDegree + 1))
            (fun (x_2 : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x_2] (x + x_1)) ⋯ :
          (a : ℕ) → R[X])
        a_1)
      n_1)
    (coeff
      ((HAdd.hAdd (α := ℕ →₀ R[X])
            (Finsupp.onFinset (range (x.natDegree + 1)) (fun (x_2 : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x_2] x) ⋯)
            (Finsupp.onFinset (range (x_1.natDegree + 1)) (fun (x : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x] x_1) ⋯) :
          (a : ℕ) → R[X])
        a_1)
      n_1)

Tactic:
simp
-- 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
x : R
x_1 : R[X]
h :
  ∀ (a n : ℕ),
    Eq.{u + 1} (α := R)
      (coeff
        ((Finsupp.onFinset (range ((x • x_1).natDegree + 1))
              (fun (x_2 : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x_2] (x • x_1)) ⋯ :
            (a : ℕ) → R[X])
          a)
        n)
      (coeff
        ((HSMul.hSMul (α := R) (β := ℕ →₀ R[X]) ((RingHom.id R : (a : R) → R) x : R)
              (Finsupp.onFinset (range (x_1.natDegree + 1)) (fun (x : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x] x_1)
                ⋯) :
            (a : ℕ) → R[X])
          a)
        n)
⊢ Finsupp.onFinset (range ((x • x_1).natDegree + 1)) (fun (x_2 : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x_2] (x • x_1))
      ⋯ =
    HSMul.hSMul (α := R) (β := ℕ →₀ R[X]) ((RingHom.id R : (a : R) → R) x : R)
      (Finsupp.onFinset (range (x_1.natDegree + 1)) (fun (x : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x] x_1) ⋯)

Tactic:
ext
-- 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
x : R
x_1 : R[X]
a_1 n_1 : ℕ
⊢ Eq.{u + 1} (α := R)
    (coeff
      ((Finsupp.onFinset (range ((x • x_1).natDegree + 1))
            (fun (x_2 : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x_2] (x • x_1)) ⋯ :
          (a : ℕ) → R[X])
        a_1)
      n_1)
    (coeff
      ((HSMul.hSMul (α := R) (β := ℕ →₀ R[X]) ((RingHom.id R : (a : R) → R) x : R)
            (Finsupp.onFinset (range (x_1.natDegree + 1)) (fun (x : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x] x_1) ⋯) :
          (a : ℕ) → R[X])
        a_1)
      n_1)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ Finsupp.support.{0, u} (M := R[X])
      (Finsupp.onFinset (range (p.natDegree + 1)) (fun (x : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x] p) ⋯) ⊆
    range n

Tactic:
Finsupp.support_onFinset_subset.trans (Finset.range_subset_range.mpr h)

Premises used: Iff.mpr, HasSubset.Subset.trans, Finset.range_subset_range, Finsupp.support_onFinset_subset
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ Finsupp.support.{0, u} (M := R[X])
      (Finsupp.onFinset (range (p.natDegree + 1)) (fun (x : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x] p) ⋯) ⊆
    range n

Tactic:
exact Finsupp.support_onFinset_subset.trans (Finset.range_subset_range.mpr h)

Premises used: Iff.mpr, HasSubset.Subset.trans, Finset.range_subset_range, Finsupp.support_onFinset_subset
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
r : R
h :
  ∀ (i : ℕ),
    Eq (α := R[X])
      ((((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) ((C : (a : R) → R[X]) r) : ℕ →₀ R[X]) : (a : ℕ) → R[X]) i : R[X])
      (((Finsupp.single 0 ((C : (a : R) → R[X]) r) : ℕ →₀ R[X]) : (a : ℕ) → R[X]) i : R[X])
⊢ Eq (α := ℕ →₀ R[X]) ((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) ((C : (a : R) → R[X]) r) : ℕ →₀ R[X])
    (Finsupp.single 0 ((C : (a : R) → R[X]) r) : ℕ →₀ R[X])

Tactic:
ext i : 1
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
r : R
i : ℕ
⊢ Eq (α := R[X])
    ((((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) ((C : (a : R) → R[X]) r) : ℕ →₀ R[X]) : (a : ℕ) → R[X]) 0 : R[X])
    (((Finsupp.single 0 ((C : (a : R) → R[X]) r) : ℕ →₀ R[X]) : (a : ℕ) → R[X]) 0 : R[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
r : R
i_1 i : ℕ
⊢ Eq (α := R[X])
    ((((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) ((C : (a : R) → R[X]) r) : ℕ →₀ R[X]) : (a : ℕ) → R[X]) (i + 1) :
      R[X])
    (((Finsupp.single 0 ((C : (a : R) → R[X]) r) : ℕ →₀ R[X]) : (a : ℕ) → R[X]) (i + 1) : R[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
r : R
i : ℕ
⊢ Eq (α := R[X])
    ((((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) ((C : (a : R) → R[X]) r) : ℕ →₀ R[X]) : (a : ℕ) → R[X]) i : R[X])
    (((Finsupp.single 0 ((C : (a : R) → R[X]) r) : ℕ →₀ R[X]) : (a : ℕ) → R[X]) i : R[X])

Tactic:
match i with
  | 0 => simp
  | i + 1 => simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := ℕ →₀ R[X]) ((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) 1) (Finsupp.single 0 1)

Tactic:
simpa using derivativeFinsupp_C (1 : R)

Premises used: OfNat.ofNat, Polynomial.derivativeFinsupp_C
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
h :
  ∀ (i : ℕ),
    Eq (α := R[X]) ((((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) X : ℕ →₀ R[X]) : (a : ℕ) → R[X]) i : R[X])
      ((HAdd.hAdd (α := ℕ →₀ R[X]) (Finsupp.single 0 X) (Finsupp.single 1 1) : (a : ℕ) → R[X]) i : R[X])
⊢ (derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) X = HAdd.hAdd (α := ℕ →₀ R[X]) (Finsupp.single 0 X) (Finsupp.single 1 1)

Tactic:
ext i : 1
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
i : ℕ
⊢ Eq (α := R[X]) ((((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) X : ℕ →₀ R[X]) : (a : ℕ) → R[X]) 0 : R[X])
    ((HAdd.hAdd (α := ℕ →₀ R[X]) (Finsupp.single 0 X) (Finsupp.single 1 1) : (a : ℕ) → R[X]) 0 : R[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
i : ℕ
⊢ Eq (α := R[X]) ((((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) X : ℕ →₀ R[X]) : (a : ℕ) → R[X]) 1 : R[X])
    ((HAdd.hAdd (α := ℕ →₀ R[X]) (Finsupp.single 0 X) (Finsupp.single 1 1) : (a : ℕ) → R[X]) 1 : R[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
i n : ℕ
⊢ Eq (α := R[X]) ((((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) X : ℕ →₀ R[X]) : (a : ℕ) → R[X]) (n + 2) : R[X])
    ((HAdd.hAdd (α := ℕ →₀ R[X]) (Finsupp.single 0 X) (Finsupp.single 1 1) : (a : ℕ) → R[X]) (n + 2) : R[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
i : ℕ
⊢ Eq (α := R[X]) ((((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) X : ℕ →₀ R[X]) : (a : ℕ) → R[X]) i : R[X])
    ((HAdd.hAdd (α := ℕ →₀ R[X]) (Finsupp.single 0 X) (Finsupp.single 1 1) : (a : ℕ) → R[X]) i : R[X])

Tactic:
match i with
  | 0 => simp
  | 1 => simp
  | (n + 2) => simp
-- 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
inst_1 : Semiring S
p : R[X]
f : R →+* S
⊢ Eq.{v + 1} (α := S[X]) ((fun (x : R[X]) ↦ map f x) 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
h :
  ∀ (i : ℕ),
    Eq (α := S[X]) ((((derivativeFinsupp : (a : S[X]) → ℕ →₀ S[X]) (map f p) : ℕ →₀ S[X]) : (a : ℕ) → S[X]) i : S[X])
      ((Finsupp.mapRange (fun (x : R[X]) ↦ map f x) ⋯ ((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) p) : (a : ℕ) → S[X])
          i :
        S[X])
⊢ Eq (α := ℕ →₀ S[X]) ((derivativeFinsupp : (a : S[X]) → ℕ →₀ S[X]) (map f p) : ℕ →₀ S[X])
    (Finsupp.mapRange (fun (x : R[X]) ↦ map f x) ⋯ ((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) p) : ℕ →₀ S[X])

Tactic:
ext i : 1
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
i : ℕ
⊢ Eq (α := S[X]) ((((derivativeFinsupp : (a : S[X]) → ℕ →₀ S[X]) (map f p) : ℕ →₀ S[X]) : (a : ℕ) → S[X]) i : S[X])
    ((Finsupp.mapRange (fun (x : R[X]) ↦ map f x) ⋯ ((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) p) : (a : ℕ) → S[X])
        i :
      S[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
h :
  ∀ (i : ℕ),
    Eq (α := R[X])
      ((((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) ((derivative : (a : R[X]) → R[X]) p) : ℕ →₀ R[X]) :
            (a : ℕ) → R[X])
          i :
        R[X])
      ((Finsupp.comapDomain Nat.succ ((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) p) ⋯ : (a : ℕ) → R[X]) i : R[X])
⊢ Eq (α := ℕ →₀ R[X]) ((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) ((derivative : (a : R[X]) → R[X]) p) : ℕ →₀ R[X])
    (Finsupp.comapDomain Nat.succ ((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) p) ⋯ : ℕ →₀ R[X])

Tactic:
ext i : 1
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
⊢ Eq (α := R[X])
    ((((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) ((derivative : (a : R[X]) → R[X]) p) : ℕ →₀ R[X]) : (a : ℕ) → R[X])
        i :
      R[X])
    ((Finsupp.comapDomain Nat.succ ((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) p) ⋯ : (a : ℕ) → R[X]) i : R[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n : ℕ
⊢ (derivative : (a : R[X]) → R[X]) (p ^ (Nat.zero + 1)) =
    HMul.hMul (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑Nat.zero : R) 1) : R[X]) (p ^ Nat.zero))
      ((derivative : (a : R[X]) → R[X]) p : R[X])

Tactic:
simp