awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
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))
⊢ ∑ 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)
have 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)
Tactic: refine (sum_range_succ' _ _).trans (congr_arg₂ (· + ·) ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
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))
    (∑ 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))
have 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))
Tactic: rw [sum_range_succ, Nat.choose_succ_self, zero_smul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
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))
have 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)
Tactic: refine sum_congr rfl fun k hk => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (hypothesis)
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
⊢ 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)
have hk₁ : k < n
Tactic: rw [mem_range] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
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.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)
have succ : n - (k + 1) + 1 = n - k
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Nat.choose_zero_right, tsub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Nat.choose_zero_right, tsub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
⊢ (⇑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)
have zero : (⇑derivative : (a : R[X]) → R[X])^[0] (p * q) =
  ∑ k ∈ range (Nat.succ 0),
    Nat.choose 0 k • ((⇑derivative : (a : R[X]) → R[X])^[0 - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
Tactic: induction n with
  | zero =>
    simp [Finset.range]
  | succ n IH =>
    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]
    congr
    refine (sum_range_succ' _ _).trans (congr_arg₂ (· + ·) ?_ ?_)
    · rw [sum_range_succ, Nat.choose_succ_self, zero_smul, add_zero]
      refine sum_congr rfl fun k hk => ?_
      rw [mem_range] at hk
      congr
      lia
    · rw [Nat.choose_zero_right, tsub_zero]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
zero :
  (⇑derivative : (a : R[X]) → R[X])^[0] (p * q) =
    ∑ k ∈ range (Nat.succ 0),
      Nat.choose 0 k • ((⇑derivative : (a : R[X]) → R[X])^[0 - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)
⊢ (⇑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)
have succ : ∀ (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)),
  (⇑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: induction n with
  | zero =>
    simp [Finset.range]
  | succ n IH =>
    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]
    congr
    refine (sum_range_succ' _ _).trans (congr_arg₂ (· + ·) ?_ ?_)
    · rw [sum_range_succ, Nat.choose_succ_self, zero_smul, add_zero]
      refine sum_congr rfl fun k hk => ?_
      rw [mem_range] at hk
      congr
      lia
    · rw [Nat.choose_zero_right, tsub_zero]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
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 : ℕ
⊢ Ne.{u + 1} (α := R[X]) ((fun (x : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x] p) i) 0 → i ∈ range (p.natDegree + 1)
have contrapose : i ∉ range (p.natDegree + 1) → Eq.{u + 1} (α := R[X]) ((fun (x : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x] p) i) 0
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
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]
⊢ 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) ⋯)
have 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)) sorry :
          (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) sorry)
            (Finsupp.onFinset (range (x_1.natDegree + 1)) (fun (x : ℕ) ↦ (⇑derivative : (a : R[X]) → R[X])^[x] x_1) sorry) :
          (a : ℕ) → R[X])
        a)
      n)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
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]
⊢ 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) ⋯)
have 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)) sorry :
          (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) sorry) :
          (a : ℕ) → R[X])
        a)
      n)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
r : R
⊢ 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])
have 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])
Tactic: ext i : 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
⊢ (derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) X = HAdd.hAdd (α := ℕ →₀ R[X]) (Finsupp.single 0 X) (Finsupp.single 1 1)
have 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])
Tactic: ext i : 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
⊢ 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])
have 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) sorry ((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) p) : (a : ℕ) → S[X])
        i :
      S[X])
Tactic: ext i : 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : 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])
have 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) sorry : (a : ℕ) → R[X]) i : R[X])
Tactic: ext i : 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n_1 n : ℕ
ih :
  (derivative : (a : R[X]) → R[X]) (p ^ (n + 1)) =
    HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n : R) 1) : R[X]) (p ^ n))
      ((derivative : (a : R[X]) → R[X]) p : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (p ^ (n.succ + 1)) =
    HMul.hMul (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n.succ : R) 1) : R[X]) (p ^ n.succ))
      ((derivative : (a : R[X]) → R[X]) p : R[X])
have rw : HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑n : R) * p ^ n * p + p ^ n * p)
      ((derivative : (a : R[X]) → R[X]) p : R[X]) +
    HMul.hMul (β := R[X]) (p ^ n * p) ((derivative : (a : R[X]) → R[X]) p : R[X]) =
  HMul.hMul (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n.succ : R) 1) : R[X]) (p ^ n) * p)
    ((derivative : (a : R[X]) → R[X]) p : R[X])
Tactic: rw [pow_succ, derivative_mul, ih, Nat.add_one, mul_right_comm, C_add,
      add_mul, add_mul, pow_succ, ← mul_assoc, C_1, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n_1 n : ℕ
⊢ (derivative : (a : R[X]) → R[X]) (p ^ n.succ) =
    HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑n.succ : R) * p ^ (n.succ - 1))
      ((derivative : (a : R[X]) → R[X]) p : R[X])
have rw : HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n : R) 1) : R[X]) (p ^ n))
    ((derivative : (a : R[X]) → R[X]) p : R[X]) =
  HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑n.succ : R) * p ^ (n.succ - 1))
    ((derivative : (a : R[X]) → R[X]) p : R[X])
Tactic: rw [p.derivative_pow_succ n, Nat.add_one_sub_one, n.cast_succ]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n_1 n : ℕ
rw :
  HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n : R) 1) : R[X]) (p ^ n))
      ((derivative : (a : R[X]) → R[X]) p : R[X]) =
    HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑n.succ : R) * p ^ (n.succ - 1))
      ((derivative : (a : R[X]) → R[X]) p : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (p ^ n.succ) =
    HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑n.succ : R) * p ^ (n.succ - 1))
      ((derivative : (a : R[X]) → R[X]) p : R[X])
have rw₁ : HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n : R) 1) : R[X]) (p ^ n))
    ((derivative : (a : R[X]) → R[X]) p : R[X]) =
  HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑n.succ : R) * p ^ n) ((derivative : (a : R[X]) → R[X]) p : R[X])
Tactic: rw [p.derivative_pow_succ n, Nat.add_one_sub_one, n.cast_succ]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n_1 n : ℕ
rw :
  HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n : R) 1) : R[X]) (p ^ n))
      ((derivative : (a : R[X]) → R[X]) p : R[X]) =
    HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑n.succ : R) * p ^ (n.succ - 1))
      ((derivative : (a : R[X]) → R[X]) p : R[X])
rw₁ :
  HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n : R) 1) : R[X]) (p ^ n))
      ((derivative : (a : R[X]) → R[X]) p : R[X]) =
    HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑n.succ : R) * p ^ n) ((derivative : (a : R[X]) → R[X]) p : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (p ^ n.succ) =
    HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑n.succ : R) * p ^ (n.succ - 1))
      ((derivative : (a : R[X]) → R[X]) p : R[X])
have rw₂ : HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n : R) 1) : R[X]) (p ^ n))
    ((derivative : (a : R[X]) → R[X]) p : R[X]) =
  HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n : R) 1) : R[X]) (p ^ n))
    ((derivative : (a : R[X]) → R[X]) p : R[X])
Tactic: rw [p.derivative_pow_succ n, Nat.add_one_sub_one, n.cast_succ]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
⊢ (derivative : (a : R[X]) → R[X]) (HPow.hPow (β := ℕ) p 2) =
    HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) 2 * p) ((derivative : (a : R[X]) → R[X]) p : R[X])
have rw : HMul.hMul (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑1 : R) 1) : R[X]) (HPow.hPow (β := ℕ) p 1))
    ((derivative : (a : R[X]) → R[X]) p : R[X]) =
  HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) 2 * p) ((derivative : (a : R[X]) → R[X]) p : R[X])
Tactic: rw [derivative_pow_succ, Nat.cast_one, one_add_one_eq_two, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
rw :
  HMul.hMul (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑1 : R) 1) : R[X]) (HPow.hPow (β := ℕ) p 1))
      ((derivative : (a : R[X]) → R[X]) p : R[X]) =
    HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) 2 * p) ((derivative : (a : R[X]) → R[X]) p : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (HPow.hPow (β := ℕ) p 2) =
    HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) 2 * p) ((derivative : (a : R[X]) → R[X]) p : R[X])
have rw₁ : HMul.hMul (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) 1 1) : R[X]) (HPow.hPow (β := ℕ) p 1))
    ((derivative : (a : R[X]) → R[X]) p : R[X]) =
  HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) 2 * p) ((derivative : (a : R[X]) → R[X]) p : R[X])
Tactic: rw [derivative_pow_succ, Nat.cast_one, one_add_one_eq_two, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
rw :
  HMul.hMul (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑1 : R) 1) : R[X]) (HPow.hPow (β := ℕ) p 1))
      ((derivative : (a : R[X]) → R[X]) p : R[X]) =
    HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) 2 * p) ((derivative : (a : R[X]) → R[X]) p : R[X])
rw₁ :
  HMul.hMul (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) 1 1) : R[X]) (HPow.hPow (β := ℕ) p 1))
      ((derivative : (a : R[X]) → R[X]) p : R[X]) =
    HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) 2 * p) ((derivative : (a : R[X]) → R[X]) p : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (HPow.hPow (β := ℕ) p 2) =
    HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) 2 * p) ((derivative : (a : R[X]) → R[X]) p : R[X])
have rw₂ : HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) 2 * HPow.hPow (β := ℕ) p 1) ((derivative : (a : R[X]) → R[X]) p : R[X]) =
  HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) 2 * p) ((derivative : (a : R[X]) → R[X]) p : R[X])
Tactic: rw [derivative_pow_succ, Nat.cast_one, one_add_one_eq_two, pow_one]