awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
    ∑ k ∈ range (min m n).succ,
      (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
have hsum : (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
  ∑ k ∈ range n.succ,
    (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
Tactic: have hsum : derivative^[n] (p * X ^ m) =
      ∑ k ∈ range n.succ,
        (n.choose k * m.descFactorial k) • (derivative^[n - k] p * X ^ (m - k)) := by
    simp_rw [iterate_derivative_mul, iterate_derivative_X_pow_eq_smul, mul_smul]
    congr! 2 with k hk
    norm_cast
    ring
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
    ∑ k ∈ range n.succ,
      (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
    ∑ k ∈ range (min m n).succ,
      (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
have rw : Eq.{u + 1} (α := R[X])
  (∑ k ∈ range n.succ,
    (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)))
  (∑ k ∈ range (min m n).succ,
    (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)))
Tactic: rw [hsum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
    ∑ k ∈ range n.succ,
      (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
⊢ Eq.{u + 1} (α := R[X])
    (∑ k ∈ range n.succ,
      (n.choose k * m.descFactorial k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)))
    (∑ k ∈ range (min m n).succ,
      (n.choose k * m.descFactorial k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)))
have refine : ∀ (k : ℕ) (hk : k ∈ range n.succ) (hk' : k ∉ range (min m n).succ),
  (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)) = 0
Tactic: refine sum_congr_of_eq_on_inter (fun k hk hk' ↦ ?_) (by simp_all) (by simp)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
    ∑ k ∈ range n.succ,
      (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)) = 0
have inl : ∀ (hkm : k ≤ m),
  (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)) = 0
Tactic: rcases le_or_gt k m with hkm | hkm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
    ∑ k ∈ range n.succ,
      (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
inl :
  ∀ (hkm : k ≤ m),
    (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)) =
      0
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)) = 0
have inr : ∀ (hkm : m < k),
  (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)) = 0
Tactic: rcases le_or_gt k m with hkm | hkm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
    ∑ k ∈ range n.succ,
      (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
hkm : k ≤ m
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)) = 0
have hk'₁ : n < k
Tactic: replace hk' : n < k := by simpa [hkm] using hk'
Cleared hypotheses: hk'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] (p * X) =
    (⇑derivative : (a : R[X]) → R[X])^[n] p * X + n • (⇑derivative : (a : R[X]) → R[X])^[n - 1] p
have h : X = HPow.hPow (α := R[X]) (β := ℕ) X 1
Tactic: convert! p.iterate_derivative_mul_X_pow n 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
h : X = HPow.hPow (α := R[X]) (β := ℕ) X 1
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] (p * X) =
    (⇑derivative : (a : R[X]) → R[X])^[n] p * X + n • (⇑derivative : (a : R[X]) → R[X])^[n - 1] p
have h₁ : (⇑derivative : (a : R[X]) → R[X])^[n] p * X + n • (⇑derivative : (a : R[X]) → R[X])^[n - 1] p =
  ∑ k ∈ range (min 1 n).succ,
    (n.choose k * Nat.descFactorial 1 k) •
      ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (1 - k))
Tactic: convert! p.iterate_derivative_mul_X_pow n 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] p * X + n • (⇑derivative : (a : R[X]) → R[X])^[n - 1] p =
    ∑ k ∈ range (min 1 n).succ,
      (n.choose k * Nat.descFactorial 1 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (1 - k))
have h : (⇑derivative : (a : R[X]) → R[X])^[0] p * X +
    HSMul.hSMul (α := ℕ) 0 ((⇑derivative : (a : R[X]) → R[X])^[HSub.hSub (α := ℕ) 0 1] p) =
  ∑ k ∈ range (Nat.succ (min 1 0)),
    (Nat.choose 0 k * Nat.descFactorial 1 k) •
      ((⇑derivative : (a : R[X]) → R[X])^[0 - k] p * HPow.hPow (α := R[X]) X (1 - k))
Tactic: rcases n with rfl | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
h :
  (⇑derivative : (a : R[X]) → R[X])^[0] p * X +
      HSMul.hSMul (α := ℕ) 0 ((⇑derivative : (a : R[X]) → R[X])^[HSub.hSub (α := ℕ) 0 1] p) =
    ∑ k ∈ range (Nat.succ (min 1 0)),
      (Nat.choose 0 k * Nat.descFactorial 1 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[0 - k] p * HPow.hPow (α := R[X]) X (1 - k))
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] p * X + n • (⇑derivative : (a : R[X]) → R[X])^[n - 1] p =
    ∑ k ∈ range (min 1 n).succ,
      (n.choose k * Nat.descFactorial 1 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (1 - k))
have h₁ : ∀ (n : ℕ),
  (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X + (n + 1) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 - 1] p =
    ∑ k ∈ range (min 1 (n + 1)).succ,
      ((n + 1).choose k * Nat.descFactorial 1 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n + 1 - k] p * HPow.hPow (α := R[X]) X (1 - k))
Tactic: rcases n with rfl | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[n]
      (HMul.hMul (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) X) =
    (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X + n • (⇑derivative : (a : R[X]) → R[X])^[n] p
have h : X = HPow.hPow (α := R[X]) (β := ℕ) X 1
Tactic: convert! (derivative p).iterate_derivative_mul_X_pow n 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
h : X = HPow.hPow (α := R[X]) (β := ℕ) X 1
⊢ (⇑derivative : (a : R[X]) → R[X])^[n]
      (HMul.hMul (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) X) =
    (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X + n • (⇑derivative : (a : R[X]) → R[X])^[n] p
have h₁ : (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X + n • (⇑derivative : (a : R[X]) → R[X])^[n] p =
  ∑ k ∈ range (min 1 n).succ,
    (n.choose k * Nat.descFactorial 1 k) •
      HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n - k] ((derivative : (a : R[X]) → R[X]) p) : R[X])
        (HPow.hPow (α := R[X]) X (1 - k))
Tactic: convert! (derivative p).iterate_derivative_mul_X_pow n 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X + n • (⇑derivative : (a : R[X]) → R[X])^[n] p =
    ∑ k ∈ range (min 1 n).succ,
      (n.choose k * Nat.descFactorial 1 k) •
        HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n - k] ((derivative : (a : R[X]) → R[X]) p) : R[X])
          (HPow.hPow (α := R[X]) X (1 - k))
have h : (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] p * X +
    HSMul.hSMul (α := ℕ) 0 ((⇑derivative : (a : R[X]) → R[X])^[0] p) =
  ∑ k ∈ range (Nat.succ (min 1 0)),
    (Nat.choose 0 k * Nat.descFactorial 1 k) •
      HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[0 - k] ((derivative : (a : R[X]) → R[X]) p) : R[X])
        (HPow.hPow (α := R[X]) X (1 - k))
Tactic: rcases n with rfl | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
h :
  (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] p * X +
      HSMul.hSMul (α := ℕ) 0 ((⇑derivative : (a : R[X]) → R[X])^[0] p) =
    ∑ k ∈ range (Nat.succ (min 1 0)),
      (Nat.choose 0 k * Nat.descFactorial 1 k) •
        HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[0 - k] ((derivative : (a : R[X]) → R[X]) p) : R[X])
          (HPow.hPow (α := R[X]) X (1 - k))
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X + n • (⇑derivative : (a : R[X]) → R[X])^[n] p =
    ∑ k ∈ range (min 1 n).succ,
      (n.choose k * Nat.descFactorial 1 k) •
        HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n - k] ((derivative : (a : R[X]) → R[X]) p) : R[X])
          (HPow.hPow (α := R[X]) X (1 - k))
have h₁ : ∀ (n : ℕ),
  (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1] p * X + (n + 1) • (⇑derivative : (a : R[X]) → R[X])^[n + 1] p =
    ∑ k ∈ range (min 1 (n + 1)).succ,
      ((n + 1).choose k * Nat.descFactorial 1 k) •
        HMul.hMul (α := R[X])
          ((⇑derivative : (a : R[X]) → R[X])^[n + 1 - k] ((derivative : (a : R[X]) → R[X]) p) : R[X])
          (HPow.hPow (α := R[X]) X (1 - k))
Tactic: rcases n with rfl | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] ((⇑derivative : (a : R[X]) → R[X])^[2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2) =
    (⇑derivative : (a : R[X]) → R[X])^[n + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * n) • (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X +
      (n * (n - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n] p
have h : (⇑derivative : (a : R[X]) → R[X])^[n + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
      (2 * n) • (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X +
    (n * (n - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n] p =
  ∑ k ∈ range (min 2 n).succ,
    (n.choose k * Nat.descFactorial 2 k) •
      ((⇑derivative : (a : R[X]) → R[X])^[n - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
        HPow.hPow (α := R[X]) X (2 - k))
Tactic: convert! (derivative^[2] p).iterate_derivative_mul_X_pow n 2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * n) • (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X +
      (n * (n - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n] p =
    ∑ k ∈ range (min 2 n).succ,
      (n.choose k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))
have h : (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
      HMul.hMul (α := ℕ) 2 0 • (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] p * X +
    (0 * HSub.hSub (α := ℕ) 0 1) • (⇑derivative : (a : R[X]) → R[X])^[0] p =
  ∑ k ∈ range (Nat.succ (min 2 0)),
    (Nat.choose 0 k * Nat.descFactorial 2 k) •
      ((⇑derivative : (a : R[X]) → R[X])^[0 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
        HPow.hPow (α := R[X]) X (2 - k))
Tactic: rcases n with rfl | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
h :
  (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        HMul.hMul (α := ℕ) 2 0 • (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] p * X +
      (0 * HSub.hSub (α := ℕ) 0 1) • (⇑derivative : (a : R[X]) → R[X])^[0] p =
    ∑ k ∈ range (Nat.succ (min 2 0)),
      (Nat.choose 0 k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[0 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * n) • (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X +
      (n * (n - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n] p =
    ∑ k ∈ range (min 2 n).succ,
      (n.choose k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))
have h₁ : ∀ (n : ℕ),
  (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * (n + 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1] p * X +
      ((n + 1) * (n + 1 - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1] p =
    ∑ k ∈ range (min 2 (n + 1)).succ,
      ((n + 1).choose k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n + 1 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))
Tactic: rcases n with rfl | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n : ℕ
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * (n + 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1] p * X +
      ((n + 1) * (n + 1 - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1] p =
    ∑ k ∈ range (min 2 (n + 1)).succ,
      ((n + 1).choose k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n + 1 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))
have h : (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1 + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
      (2 * HAdd.hAdd (α := ℕ) 0 1) • (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1 + 1] p * X +
    (HAdd.hAdd (α := ℕ) 0 1 * (HAdd.hAdd (α := ℕ) 0 1 - 1)) •
      (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] p =
  ∑ k ∈ range (min 2 (HAdd.hAdd (α := ℕ) 0 1)).succ,
    ((HAdd.hAdd (α := ℕ) 0 1).choose k * Nat.descFactorial 2 k) •
      ((⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
        HPow.hPow (α := R[X]) X (2 - k))
Tactic: rcases n with rfl | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n : ℕ
h :
  (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1 + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * HAdd.hAdd (α := ℕ) 0 1) • (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1 + 1] p * X +
      (HAdd.hAdd (α := ℕ) 0 1 * (HAdd.hAdd (α := ℕ) 0 1 - 1)) •
        (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] p =
    ∑ k ∈ range (min 2 (HAdd.hAdd (α := ℕ) 0 1)).succ,
      ((HAdd.hAdd (α := ℕ) 0 1).choose k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * (n + 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1] p * X +
      ((n + 1) * (n + 1 - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1] p =
    ∑ k ∈ range (min 2 (n + 1)).succ,
      ((n + 1).choose k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n + 1 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))
have h₁ : ∀ (n : ℕ),
  (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * (n + 1 + 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 + 1] p * X +
      ((n + 1 + 1) * (n + 1 + 1 - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1] p =
    ∑ k ∈ range (min 2 (n + 1 + 1)).succ,
      ((n + 1 + 1).choose k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))
Tactic: rcases n with rfl | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n : ℕ
this : (n + 1 + 1) * (n + 1) / 2 * 2 = (n + 1 + 1) * (n + 1)
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * (n + 1 + 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 + 1] p * X +
      ((n + 1 + 1) * (n + 1 + 1 - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1] p =
    ∑ k ∈ range (min 2 (n + 1 + 1)).succ,
      ((n + 1 + 1).choose k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))
have simp : HMul.hMul (α := R[X])
        ((⇑derivative : (a : R[X]) → R[X])^[n]
            ((derivative : (a : R[X]) → R[X])
              ((derivative : (a : R[X]) → R[X])
                ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p)))) :
          R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
      HSMul.hSMul (β := R[X]) (2 * (n + 1 + 1))
          ((⇑derivative : (a : R[X]) → R[X])^[n]
              ((derivative : (a : R[X]) → R[X])
                ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p))) :
            R[X]) *
        X +
    HSMul.hSMul (β := R[X]) ((n + 1 + 1) * (n + 1))
      ((⇑derivative : (a : R[X]) → R[X])^[n] ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p)) :
        R[X]) =
  HMul.hMul (α := R[X])
        ((⇑derivative : (a : R[X]) → R[X])^[n]
            ((derivative : (a : R[X]) → R[X])
              ((derivative : (a : R[X]) → R[X])
                ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p)))) :
          R[X])
        (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
      ((n + 1 + 1) * 2) •
        HMul.hMul (α := R[X]) (β := R[X])
          ((⇑derivative : (a : R[X]) → R[X])^[n]
              ((derivative : (a : R[X]) → R[X])
                ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p))) :
            R[X])
          X +
    HSMul.hSMul (β := R[X]) ((n + 1 + 1) * (n + 1))
      ((⇑derivative : (a : R[X]) → R[X])^[n] ((derivative : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) p)) :
        R[X])
Tactic: simp -implicitDefEqProofs [this, -nsmul_eq_mul, sum_range_succ, Nat.choose_two_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n : ℕ
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * (n + 1 + 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 + 1] p * X +
      ((n + 1 + 1) * (n + 1 + 1 - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1] p =
    ∑ k ∈ range (min 2 (n + 1 + 1)).succ,
      ((n + 1 + 1).choose k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))
have h : (n + 1 + 1) * (n + 1) / 2 * 2 = (n + 1 + 1) * (n + 1)
Tactic: suffices ((n + 1 + 1) * (n + 1) / 2) * 2 = (n + 1 + 1) * (n + 1) by
    simp -implicitDefEqProofs [this, -nsmul_eq_mul, sum_range_succ, Nat.choose_two_right]
    ring
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n : ℕ
⊢ (n + 1 + 1) * (n + 1) / 2 * 2 = (n + 1 + 1) * (n + 1)
have h : (n + 1) * (n + 1 + 1) / 2 * 2 = (n + 1) * (n + 1 + 1)
Tactic: rw [mul_comm (n + 1 + 1)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
⊢ (derivative : (a : R[X]) → R[X]) (p.comp q) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) (comp ((derivative : (a : R[X]) → R[X]) p) q)
have add : ∀ (p q_1 : R[X]),
  (derivative : (a : R[X]) → R[X]) (p.comp q) =
      HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) (comp ((derivative : (a : R[X]) → R[X]) p) q) →
    (derivative : (a : R[X]) → R[X]) (q_1.comp q) =
        HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
          (comp ((derivative : (a : R[X]) → R[X]) q_1) q) →
      (derivative : (a : R[X]) → R[X]) ((p + q_1).comp q) =
        HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
          (comp ((derivative : (a : R[X]) → R[X]) (p + q_1)) q)
Tactic: induction p using Polynomial.induction_on'
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
add :
  ∀ (p q_1 : R[X]),
    (derivative : (a : R[X]) → R[X]) (p.comp q) =
        HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
          (comp ((derivative : (a : R[X]) → R[X]) p) q) →
      (derivative : (a : R[X]) → R[X]) (q_1.comp q) =
          HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
            (comp ((derivative : (a : R[X]) → R[X]) q_1) q) →
        (derivative : (a : R[X]) → R[X]) ((p + q_1).comp q) =
          HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
            (comp ((derivative : (a : R[X]) → R[X]) (p + q_1)) q)
⊢ (derivative : (a : R[X]) → R[X]) (p.comp q) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) (comp ((derivative : (a : R[X]) → R[X]) p) q)
have monomial : ∀ (n : ℕ) (a : R),
  (derivative : (a : R[X]) → R[X]) (comp ((monomial n : (a : R) → R[X]) a) q) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X])
      (comp ((derivative : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) a)) q)
Tactic: induction p using Polynomial.induction_on'
Cleared hypotheses: p