From 74b97a374896374f5d9c2d56699d3b2cc9b991e9 Mon Sep 17 00:00:00 2001 From: Yuval Filmus Date: Fri, 26 Dec 2025 13:34:25 +0200 Subject: [PATCH 01/15] Completed proofs --- Mathlib/Algebra/Polynomial/Derivative.lean | 92 ++++++++++++++++++++++ 1 file changed, 92 insertions(+) diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean index 9c3881a0db7d87..ce431739d2f6f8 100644 --- a/Mathlib/Algebra/Polynomial/Derivative.lean +++ b/Mathlib/Algebra/Polynomial/Derivative.lean @@ -516,6 +516,98 @@ theorem iterate_derivative_X_add_pow (n k : ℕ) (c : R) : Nat.cast_mul] ring +theorem iterate_derivative_mul_X_pow {n m} (p : R[X]) : + derivative^[n] (p * X ^ m) = + ∑ k ∈ range m.succ, + ((n.choose k * m.descFactorial k) • (derivative^[n - k] p * X ^ (m - k))) := by + 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 + rw [iterate_derivative_mul] + congr! 1 with k hk + rw [iterate_derivative_X_pow_eq_smul, ← smul_smul] + norm_cast + ring + rw [hsum] + by_cases! n ≤ m + case pos h => + rw [← add_zero (∑ k ∈ range n.succ, _), + show range m.succ = range n.succ ∪ Ico n.succ m.succ by grind, + sum_union (by rw [range_eq_Ico]; apply Ico_disjoint_Ico_consecutive)] + congr 1 + refine (sum_eq_zero (fun k hk => ?_)).symm + rw [Nat.choose_eq_zero_of_lt (by grind)] + simp + case neg h => + rw [← add_zero (∑ k ∈ range m.succ, _), + show range n.succ = range m.succ ∪ Ico m.succ n.succ by grind, + sum_union (by rw [range_eq_Ico]; apply Ico_disjoint_Ico_consecutive)] + congr 1 + refine sum_eq_zero (fun k hk => ?_) + rw [Nat.descFactorial_eq_zero_iff_lt.mpr (by grind)] + simp + +theorem iterate_derivative_mul_X_pow' {n m} (p : R[X]) : + derivative^[n] (derivative^[m] p * X ^ m) = + ∑ k ∈ range m.succ, + ((n.choose k * m.descFactorial k) • (derivative^[n + (m - k)] p * X ^ (m - k))) := by + rw [iterate_derivative_mul_X_pow] + congr! 1 with k hk + by_cases! k ≤ n + case pos h => + rw [← Function.iterate_add_apply, ← Nat.sub_add_comm h, + Nat.add_sub_assoc (mem_range_succ_iff.mp hk)] + case neg h => + simp [Nat.choose_eq_zero_of_lt h] + +theorem iterate_derivative_mul_X {n} (p : R[X]) : + derivative^[n] (p * X) = (derivative^[n] p) * X + n • derivative^[n - 1] p := by + rw [← pow_one X, iterate_derivative_mul_X_pow, range_add_one, sum_insert (by simp), range_one, + sum_singleton] + simp + ring + +theorem iterate_derivative_mul_X' {n} (p : R[X]) : + derivative^[n] (derivative p * X) = (derivative^[n + 1] p) * X + n • derivative^[n] p := by + trans derivative^[n] (derivative^[1] p * X) + · rw [Function.iterate_one] + rw [← pow_one X, iterate_derivative_mul_X_pow', range_add_one, sum_insert (by simp), range_one, + sum_singleton] + simp + ring + +theorem iterate_derivative_mul_X_sq {n} (p : R[X]) : + derivative^[n] (p * X ^ 2) = + (derivative^[n] p) * X ^ 2 + (2 * n) • (derivative^[n - 1] p) * X + + (n * (n - 1)) • derivative^[n - 2] p := by + trans (n * (n - 1)) • derivative^[n - 2] p + ((2 * n) • (derivative^[n - 1] p) * X + + (derivative^[n] p) * X ^ 2) + · rw [iterate_derivative_mul_X_pow, range_add_one, sum_insert (by simp), range_add_one, + sum_insert (by simp), range_one, sum_singleton, Nat.sub_self, pow_zero, mul_one, + Nat.descFactorial_one, Nat.choose_one_right, pow_one, Nat.choose_zero_right, + Nat.descFactorial_zero, mul_one, one_smul, Nat.sub_zero, Nat.sub_zero] + congr 2 + · rw [Nat.descFactorial_self, mul_comm, ← Nat.descFactorial_eq_factorial_mul_choose, + Nat.descFactorial_succ, Nat.descFactorial_one, mul_comm] + ring + ring + +theorem iterate_derivative_mul_X_sq' {n} (p : R[X]) : + derivative^[n] (derivative^[2] p * X ^ 2) = + (derivative^[n + 2] p) * X ^ 2 + (2 * n) • (derivative^[n + 1] p) * X + + (n * (n - 1)) • derivative^[n] p := by + trans (n * (n - 1)) • derivative^[n] p + ((2 * n) • (derivative^[n + 1] p) * X + + (derivative^[n + 2] p) * X ^ 2) + · rw [iterate_derivative_mul_X_pow', range_add_one, sum_insert (by simp), range_add_one, + sum_insert (by simp), range_one, sum_singleton, Nat.sub_self, pow_zero, mul_one, + Nat.descFactorial_one, Nat.choose_one_right, pow_one, Nat.choose_zero_right, + Nat.descFactorial_zero, mul_one, one_smul, Nat.sub_zero] + congr 2 + · rw [Nat.descFactorial_self, mul_comm, ← Nat.descFactorial_eq_factorial_mul_choose, + Nat.descFactorial_succ, Nat.descFactorial_one, mul_comm] + ring + ring + theorem derivative_comp (p q : R[X]) : derivative (p.comp q) = derivative q * p.derivative.comp q := by induction p using Polynomial.induction_on' From c29f6479d32c8e55ebace0d936e049d416834b4e Mon Sep 17 00:00:00 2001 From: Yuval Filmus Date: Fri, 26 Dec 2025 16:01:23 +0200 Subject: [PATCH 02/15] Optimization (removed some simp's) --- Mathlib/Algebra/Polynomial/Derivative.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean index ce431739d2f6f8..b1ec39ec5331f0 100644 --- a/Mathlib/Algebra/Polynomial/Derivative.lean +++ b/Mathlib/Algebra/Polynomial/Derivative.lean @@ -562,8 +562,8 @@ theorem iterate_derivative_mul_X_pow' {n m} (p : R[X]) : theorem iterate_derivative_mul_X {n} (p : R[X]) : derivative^[n] (p * X) = (derivative^[n] p) * X + n • derivative^[n - 1] p := by - rw [← pow_one X, iterate_derivative_mul_X_pow, range_add_one, sum_insert (by simp), range_one, - sum_singleton] + rw [← pow_one X, iterate_derivative_mul_X_pow, range_add_one, sum_insert notMem_range_self, + range_one, sum_singleton] simp ring @@ -571,8 +571,8 @@ theorem iterate_derivative_mul_X' {n} (p : R[X]) : derivative^[n] (derivative p * X) = (derivative^[n + 1] p) * X + n • derivative^[n] p := by trans derivative^[n] (derivative^[1] p * X) · rw [Function.iterate_one] - rw [← pow_one X, iterate_derivative_mul_X_pow', range_add_one, sum_insert (by simp), range_one, - sum_singleton] + rw [← pow_one X, iterate_derivative_mul_X_pow', range_add_one, sum_insert notMem_range_self, + range_one, sum_singleton] simp ring @@ -582,8 +582,8 @@ theorem iterate_derivative_mul_X_sq {n} (p : R[X]) : (n * (n - 1)) • derivative^[n - 2] p := by trans (n * (n - 1)) • derivative^[n - 2] p + ((2 * n) • (derivative^[n - 1] p) * X + (derivative^[n] p) * X ^ 2) - · rw [iterate_derivative_mul_X_pow, range_add_one, sum_insert (by simp), range_add_one, - sum_insert (by simp), range_one, sum_singleton, Nat.sub_self, pow_zero, mul_one, + · rw [iterate_derivative_mul_X_pow, range_add_one, sum_insert notMem_range_self, range_add_one, + sum_insert notMem_range_self, range_one, sum_singleton, Nat.sub_self, pow_zero, mul_one, Nat.descFactorial_one, Nat.choose_one_right, pow_one, Nat.choose_zero_right, Nat.descFactorial_zero, mul_one, one_smul, Nat.sub_zero, Nat.sub_zero] congr 2 @@ -598,8 +598,8 @@ theorem iterate_derivative_mul_X_sq' {n} (p : R[X]) : (n * (n - 1)) • derivative^[n] p := by trans (n * (n - 1)) • derivative^[n] p + ((2 * n) • (derivative^[n + 1] p) * X + (derivative^[n + 2] p) * X ^ 2) - · rw [iterate_derivative_mul_X_pow', range_add_one, sum_insert (by simp), range_add_one, - sum_insert (by simp), range_one, sum_singleton, Nat.sub_self, pow_zero, mul_one, + · rw [iterate_derivative_mul_X_pow', range_add_one, sum_insert notMem_range_self, range_add_one, + sum_insert notMem_range_self, range_one, sum_singleton, Nat.sub_self, pow_zero, mul_one, Nat.descFactorial_one, Nat.choose_one_right, pow_one, Nat.choose_zero_right, Nat.descFactorial_zero, mul_one, one_smul, Nat.sub_zero] congr 2 From f7f3445a7e8a76ddd044021c58cde618d5da1ca5 Mon Sep 17 00:00:00 2001 From: Yuval Filmus Date: Sun, 4 Jan 2026 12:44:24 +0200 Subject: [PATCH 03/15] Added new version of iterate_derivative_mul_X_pow --- Mathlib/Algebra/Polynomial/Derivative.lean | 39 +++++++++++++--------- 1 file changed, 24 insertions(+), 15 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean index b1ec39ec5331f0..aa4bc10b1c33e2 100644 --- a/Mathlib/Algebra/Polynomial/Derivative.lean +++ b/Mathlib/Algebra/Polynomial/Derivative.lean @@ -518,7 +518,7 @@ theorem iterate_derivative_X_add_pow (n k : ℕ) (c : R) : theorem iterate_derivative_mul_X_pow {n m} (p : R[X]) : derivative^[n] (p * X ^ m) = - ∑ k ∈ range m.succ, + ∑ k ∈ range (min m n).succ, ((n.choose k * m.descFactorial k) • (derivative^[n - k] p * X ^ (m - k))) := by have hsum : derivative^[n] (p * X ^ m) = ∑ k ∈ range n.succ, @@ -530,16 +530,9 @@ theorem iterate_derivative_mul_X_pow {n m} (p : R[X]) : ring rw [hsum] by_cases! n ≤ m - case pos h => - rw [← add_zero (∑ k ∈ range n.succ, _), - show range m.succ = range n.succ ∪ Ico n.succ m.succ by grind, - sum_union (by rw [range_eq_Ico]; apply Ico_disjoint_Ico_consecutive)] - congr 1 - refine (sum_eq_zero (fun k hk => ?_)).symm - rw [Nat.choose_eq_zero_of_lt (by grind)] - simp + case pos h => simp [h] case neg h => - rw [← add_zero (∑ k ∈ range m.succ, _), + rw [min_eq_left_of_lt h, ← add_zero (∑ k ∈ range m.succ, _), show range n.succ = range m.succ ∪ Ico m.succ n.succ by grind, sum_union (by rw [range_eq_Ico]; apply Ico_disjoint_Ico_consecutive)] congr 1 @@ -548,10 +541,26 @@ theorem iterate_derivative_mul_X_pow {n m} (p : R[X]) : simp theorem iterate_derivative_mul_X_pow' {n m} (p : R[X]) : + derivative^[n] (p * X ^ m) = + ∑ k ∈ range m.succ, + ((n.choose k * m.descFactorial k) • (derivative^[n - k] p * X ^ (m - k))) := by + rw [iterate_derivative_mul_X_pow p] + by_cases! n ≤ m + case neg h => rw [min_eq_left_of_lt h] + case pos h => + rw [min_eq_right h, ← add_zero (∑ k ∈ range n.succ, _), + show range m.succ = range n.succ ∪ Ico n.succ m.succ by grind, + sum_union (by rw [range_eq_Ico]; apply Ico_disjoint_Ico_consecutive)] + congr 1 + refine (sum_eq_zero (fun k hk => ?_)).symm + rw [Nat.choose_eq_zero_of_lt (by grind)] + simp + +theorem iterate_derivative_mul_X_pow'' {n m} (p : R[X]) : derivative^[n] (derivative^[m] p * X ^ m) = ∑ k ∈ range m.succ, ((n.choose k * m.descFactorial k) • (derivative^[n + (m - k)] p * X ^ (m - k))) := by - rw [iterate_derivative_mul_X_pow] + rw [iterate_derivative_mul_X_pow'] congr! 1 with k hk by_cases! k ≤ n case pos h => @@ -562,7 +571,7 @@ theorem iterate_derivative_mul_X_pow' {n m} (p : R[X]) : theorem iterate_derivative_mul_X {n} (p : R[X]) : derivative^[n] (p * X) = (derivative^[n] p) * X + n • derivative^[n - 1] p := by - rw [← pow_one X, iterate_derivative_mul_X_pow, range_add_one, sum_insert notMem_range_self, + rw [← pow_one X, iterate_derivative_mul_X_pow', range_add_one, sum_insert notMem_range_self, range_one, sum_singleton] simp ring @@ -571,7 +580,7 @@ theorem iterate_derivative_mul_X' {n} (p : R[X]) : derivative^[n] (derivative p * X) = (derivative^[n + 1] p) * X + n • derivative^[n] p := by trans derivative^[n] (derivative^[1] p * X) · rw [Function.iterate_one] - rw [← pow_one X, iterate_derivative_mul_X_pow', range_add_one, sum_insert notMem_range_self, + rw [← pow_one X, iterate_derivative_mul_X_pow'', range_add_one, sum_insert notMem_range_self, range_one, sum_singleton] simp ring @@ -582,7 +591,7 @@ theorem iterate_derivative_mul_X_sq {n} (p : R[X]) : (n * (n - 1)) • derivative^[n - 2] p := by trans (n * (n - 1)) • derivative^[n - 2] p + ((2 * n) • (derivative^[n - 1] p) * X + (derivative^[n] p) * X ^ 2) - · rw [iterate_derivative_mul_X_pow, range_add_one, sum_insert notMem_range_self, range_add_one, + · rw [iterate_derivative_mul_X_pow', range_add_one, sum_insert notMem_range_self, range_add_one, sum_insert notMem_range_self, range_one, sum_singleton, Nat.sub_self, pow_zero, mul_one, Nat.descFactorial_one, Nat.choose_one_right, pow_one, Nat.choose_zero_right, Nat.descFactorial_zero, mul_one, one_smul, Nat.sub_zero, Nat.sub_zero] @@ -598,7 +607,7 @@ theorem iterate_derivative_mul_X_sq' {n} (p : R[X]) : (n * (n - 1)) • derivative^[n] p := by trans (n * (n - 1)) • derivative^[n] p + ((2 * n) • (derivative^[n + 1] p) * X + (derivative^[n + 2] p) * X ^ 2) - · rw [iterate_derivative_mul_X_pow', range_add_one, sum_insert notMem_range_self, range_add_one, + · rw [iterate_derivative_mul_X_pow'', range_add_one, sum_insert notMem_range_self, range_add_one, sum_insert notMem_range_self, range_one, sum_singleton, Nat.sub_self, pow_zero, mul_one, Nat.descFactorial_one, Nat.choose_one_right, pow_one, Nat.choose_zero_right, Nat.descFactorial_zero, mul_one, one_smul, Nat.sub_zero] From 9d921c914ebd191135e9e44ce4c471d4bacde250 Mon Sep 17 00:00:00 2001 From: Yuval Filmus Date: Mon, 5 Jan 2026 17:57:30 +0200 Subject: [PATCH 04/15] Update Mathlib/Algebra/Polynomial/Derivative.lean Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com> --- Mathlib/Algebra/Polynomial/Derivative.lean | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean index 5dc020e5ee44f2..afb8959dc7f3cb 100644 --- a/Mathlib/Algebra/Polynomial/Derivative.lean +++ b/Mathlib/Algebra/Polynomial/Derivative.lean @@ -540,22 +540,6 @@ theorem iterate_derivative_mul_X_pow {n m} (p : R[X]) : rw [Nat.descFactorial_eq_zero_iff_lt.mpr (by grind)] simp -theorem iterate_derivative_mul_X_pow' {n m} (p : R[X]) : - derivative^[n] (p * X ^ m) = - ∑ k ∈ range m.succ, - ((n.choose k * m.descFactorial k) • (derivative^[n - k] p * X ^ (m - k))) := by - rw [iterate_derivative_mul_X_pow p] - by_cases! n ≤ m - case neg h => rw [min_eq_left_of_lt h] - case pos h => - rw [min_eq_right h, ← add_zero (∑ k ∈ range n.succ, _), - show range m.succ = range n.succ ∪ Ico n.succ m.succ by grind, - sum_union (by rw [range_eq_Ico]; apply Ico_disjoint_Ico_consecutive)] - congr 1 - refine (sum_eq_zero (fun k hk => ?_)).symm - rw [Nat.choose_eq_zero_of_lt (by grind)] - simp - theorem iterate_derivative_mul_X_pow'' {n m} (p : R[X]) : derivative^[n] (derivative^[m] p * X ^ m) = ∑ k ∈ range m.succ, From bdf1b75a8102aa2b55b63f4e35b03826b8a70b71 Mon Sep 17 00:00:00 2001 From: Yuval Filmus Date: Mon, 5 Jan 2026 17:57:40 +0200 Subject: [PATCH 05/15] Update Mathlib/Algebra/Polynomial/Derivative.lean Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com> --- Mathlib/Algebra/Polynomial/Derivative.lean | 21 +++++++++------------ 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean index afb8959dc7f3cb..a580a52ccf33c4 100644 --- a/Mathlib/Algebra/Polynomial/Derivative.lean +++ b/Mathlib/Algebra/Polynomial/Derivative.lean @@ -540,18 +540,15 @@ theorem iterate_derivative_mul_X_pow {n m} (p : R[X]) : rw [Nat.descFactorial_eq_zero_iff_lt.mpr (by grind)] simp -theorem iterate_derivative_mul_X_pow'' {n m} (p : R[X]) : - derivative^[n] (derivative^[m] p * X ^ m) = - ∑ k ∈ range m.succ, - ((n.choose k * m.descFactorial k) • (derivative^[n + (m - k)] p * X ^ (m - k))) := by - rw [iterate_derivative_mul_X_pow'] - congr! 1 with k hk - by_cases! k ≤ n - case pos h => - rw [← Function.iterate_add_apply, ← Nat.sub_add_comm h, - Nat.add_sub_assoc (mem_range_succ_iff.mp hk)] - case neg h => - simp [Nat.choose_eq_zero_of_lt h] +theorem iterate_derivative_derivative_mul_X_pow {n m l : ℕ} (p : R[X]) (hl : m ≤ l) : + derivative^[n] (derivative^[l] p * X ^ m) = + ∑ k ∈ range (min m n).succ, + ((n.choose k * m.descFactorial k) • (derivative^[n + (l - k)] p * X ^ (m - k))) := by + have {k : ℕ} (hk : k ∈ range (min m n).succ) : n - k + l = n + (l - k) := by + replace hk : k ≤ m ∧ k ≤ n := by simpa using hk + grind + simp_rw [iterate_derivative_mul_X_pow, ← Function.iterate_add_apply] + exact Finset.sum_congr rfl fun k hk ↦ by simp [this hk] theorem iterate_derivative_mul_X {n} (p : R[X]) : derivative^[n] (p * X) = (derivative^[n] p) * X + n • derivative^[n - 1] p := by From f83ccc4584c30cf317bf2791e47396c15edd4bf0 Mon Sep 17 00:00:00 2001 From: Yuval Filmus Date: Mon, 5 Jan 2026 18:00:31 +0200 Subject: [PATCH 06/15] Removed spurious lemmas --- Mathlib/Algebra/Polynomial/Derivative.lean | 52 +--------------------- 1 file changed, 2 insertions(+), 50 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean index a580a52ccf33c4..3f477ea99d3ed3 100644 --- a/Mathlib/Algebra/Polynomial/Derivative.lean +++ b/Mathlib/Algebra/Polynomial/Derivative.lean @@ -540,63 +540,15 @@ theorem iterate_derivative_mul_X_pow {n m} (p : R[X]) : rw [Nat.descFactorial_eq_zero_iff_lt.mpr (by grind)] simp -theorem iterate_derivative_derivative_mul_X_pow {n m l : ℕ} (p : R[X]) (hl : m ≤ l) : - derivative^[n] (derivative^[l] p * X ^ m) = - ∑ k ∈ range (min m n).succ, - ((n.choose k * m.descFactorial k) • (derivative^[n + (l - k)] p * X ^ (m - k))) := by - have {k : ℕ} (hk : k ∈ range (min m n).succ) : n - k + l = n + (l - k) := by - replace hk : k ≤ m ∧ k ≤ n := by simpa using hk - grind - simp_rw [iterate_derivative_mul_X_pow, ← Function.iterate_add_apply] - exact Finset.sum_congr rfl fun k hk ↦ by simp [this hk] - theorem iterate_derivative_mul_X {n} (p : R[X]) : - derivative^[n] (p * X) = (derivative^[n] p) * X + n • derivative^[n - 1] p := by - rw [← pow_one X, iterate_derivative_mul_X_pow', range_add_one, sum_insert notMem_range_self, - range_one, sum_singleton] - simp - ring - -theorem iterate_derivative_mul_X' {n} (p : R[X]) : derivative^[n] (derivative p * X) = (derivative^[n + 1] p) * X + n • derivative^[n] p := by - trans derivative^[n] (derivative^[1] p * X) - · rw [Function.iterate_one] - rw [← pow_one X, iterate_derivative_mul_X_pow'', range_add_one, sum_insert notMem_range_self, - range_one, sum_singleton] - simp - ring + sorry theorem iterate_derivative_mul_X_sq {n} (p : R[X]) : - derivative^[n] (p * X ^ 2) = - (derivative^[n] p) * X ^ 2 + (2 * n) • (derivative^[n - 1] p) * X + - (n * (n - 1)) • derivative^[n - 2] p := by - trans (n * (n - 1)) • derivative^[n - 2] p + ((2 * n) • (derivative^[n - 1] p) * X + - (derivative^[n] p) * X ^ 2) - · rw [iterate_derivative_mul_X_pow', range_add_one, sum_insert notMem_range_self, range_add_one, - sum_insert notMem_range_self, range_one, sum_singleton, Nat.sub_self, pow_zero, mul_one, - Nat.descFactorial_one, Nat.choose_one_right, pow_one, Nat.choose_zero_right, - Nat.descFactorial_zero, mul_one, one_smul, Nat.sub_zero, Nat.sub_zero] - congr 2 - · rw [Nat.descFactorial_self, mul_comm, ← Nat.descFactorial_eq_factorial_mul_choose, - Nat.descFactorial_succ, Nat.descFactorial_one, mul_comm] - ring - ring - -theorem iterate_derivative_mul_X_sq' {n} (p : R[X]) : derivative^[n] (derivative^[2] p * X ^ 2) = (derivative^[n + 2] p) * X ^ 2 + (2 * n) • (derivative^[n + 1] p) * X + (n * (n - 1)) • derivative^[n] p := by - trans (n * (n - 1)) • derivative^[n] p + ((2 * n) • (derivative^[n + 1] p) * X + - (derivative^[n + 2] p) * X ^ 2) - · rw [iterate_derivative_mul_X_pow'', range_add_one, sum_insert notMem_range_self, range_add_one, - sum_insert notMem_range_self, range_one, sum_singleton, Nat.sub_self, pow_zero, mul_one, - Nat.descFactorial_one, Nat.choose_one_right, pow_one, Nat.choose_zero_right, - Nat.descFactorial_zero, mul_one, one_smul, Nat.sub_zero] - congr 2 - · rw [Nat.descFactorial_self, mul_comm, ← Nat.descFactorial_eq_factorial_mul_choose, - Nat.descFactorial_succ, Nat.descFactorial_one, mul_comm] - ring - ring + sorry theorem derivative_comp (p q : R[X]) : derivative (p.comp q) = derivative q * p.derivative.comp q := by From fce497cf0e8879b7f664d5a96c38a0c95209b347 Mon Sep 17 00:00:00 2001 From: Yuval Filmus Date: Mon, 5 Jan 2026 18:11:51 +0200 Subject: [PATCH 07/15] Update Mathlib/Algebra/Polynomial/Derivative.lean Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com> --- Mathlib/Algebra/Polynomial/Derivative.lean | 71 +--------------------- 1 file changed, 2 insertions(+), 69 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean index 5dc020e5ee44f2..3f477ea99d3ed3 100644 --- a/Mathlib/Algebra/Polynomial/Derivative.lean +++ b/Mathlib/Algebra/Polynomial/Derivative.lean @@ -540,82 +540,15 @@ theorem iterate_derivative_mul_X_pow {n m} (p : R[X]) : rw [Nat.descFactorial_eq_zero_iff_lt.mpr (by grind)] simp -theorem iterate_derivative_mul_X_pow' {n m} (p : R[X]) : - derivative^[n] (p * X ^ m) = - ∑ k ∈ range m.succ, - ((n.choose k * m.descFactorial k) • (derivative^[n - k] p * X ^ (m - k))) := by - rw [iterate_derivative_mul_X_pow p] - by_cases! n ≤ m - case neg h => rw [min_eq_left_of_lt h] - case pos h => - rw [min_eq_right h, ← add_zero (∑ k ∈ range n.succ, _), - show range m.succ = range n.succ ∪ Ico n.succ m.succ by grind, - sum_union (by rw [range_eq_Ico]; apply Ico_disjoint_Ico_consecutive)] - congr 1 - refine (sum_eq_zero (fun k hk => ?_)).symm - rw [Nat.choose_eq_zero_of_lt (by grind)] - simp - -theorem iterate_derivative_mul_X_pow'' {n m} (p : R[X]) : - derivative^[n] (derivative^[m] p * X ^ m) = - ∑ k ∈ range m.succ, - ((n.choose k * m.descFactorial k) • (derivative^[n + (m - k)] p * X ^ (m - k))) := by - rw [iterate_derivative_mul_X_pow'] - congr! 1 with k hk - by_cases! k ≤ n - case pos h => - rw [← Function.iterate_add_apply, ← Nat.sub_add_comm h, - Nat.add_sub_assoc (mem_range_succ_iff.mp hk)] - case neg h => - simp [Nat.choose_eq_zero_of_lt h] - theorem iterate_derivative_mul_X {n} (p : R[X]) : - derivative^[n] (p * X) = (derivative^[n] p) * X + n • derivative^[n - 1] p := by - rw [← pow_one X, iterate_derivative_mul_X_pow', range_add_one, sum_insert notMem_range_self, - range_one, sum_singleton] - simp - ring - -theorem iterate_derivative_mul_X' {n} (p : R[X]) : derivative^[n] (derivative p * X) = (derivative^[n + 1] p) * X + n • derivative^[n] p := by - trans derivative^[n] (derivative^[1] p * X) - · rw [Function.iterate_one] - rw [← pow_one X, iterate_derivative_mul_X_pow'', range_add_one, sum_insert notMem_range_self, - range_one, sum_singleton] - simp - ring + sorry theorem iterate_derivative_mul_X_sq {n} (p : R[X]) : - derivative^[n] (p * X ^ 2) = - (derivative^[n] p) * X ^ 2 + (2 * n) • (derivative^[n - 1] p) * X + - (n * (n - 1)) • derivative^[n - 2] p := by - trans (n * (n - 1)) • derivative^[n - 2] p + ((2 * n) • (derivative^[n - 1] p) * X + - (derivative^[n] p) * X ^ 2) - · rw [iterate_derivative_mul_X_pow', range_add_one, sum_insert notMem_range_self, range_add_one, - sum_insert notMem_range_self, range_one, sum_singleton, Nat.sub_self, pow_zero, mul_one, - Nat.descFactorial_one, Nat.choose_one_right, pow_one, Nat.choose_zero_right, - Nat.descFactorial_zero, mul_one, one_smul, Nat.sub_zero, Nat.sub_zero] - congr 2 - · rw [Nat.descFactorial_self, mul_comm, ← Nat.descFactorial_eq_factorial_mul_choose, - Nat.descFactorial_succ, Nat.descFactorial_one, mul_comm] - ring - ring - -theorem iterate_derivative_mul_X_sq' {n} (p : R[X]) : derivative^[n] (derivative^[2] p * X ^ 2) = (derivative^[n + 2] p) * X ^ 2 + (2 * n) • (derivative^[n + 1] p) * X + (n * (n - 1)) • derivative^[n] p := by - trans (n * (n - 1)) • derivative^[n] p + ((2 * n) • (derivative^[n + 1] p) * X + - (derivative^[n + 2] p) * X ^ 2) - · rw [iterate_derivative_mul_X_pow'', range_add_one, sum_insert notMem_range_self, range_add_one, - sum_insert notMem_range_self, range_one, sum_singleton, Nat.sub_self, pow_zero, mul_one, - Nat.descFactorial_one, Nat.choose_one_right, pow_one, Nat.choose_zero_right, - Nat.descFactorial_zero, mul_one, one_smul, Nat.sub_zero] - congr 2 - · rw [Nat.descFactorial_self, mul_comm, ← Nat.descFactorial_eq_factorial_mul_choose, - Nat.descFactorial_succ, Nat.descFactorial_one, mul_comm] - ring - ring + sorry theorem derivative_comp (p q : R[X]) : derivative (p.comp q) = derivative q * p.derivative.comp q := by From 31eca1025d5f10b57ef2d644817d27fc5a5e7da3 Mon Sep 17 00:00:00 2001 From: Yuval Filmus Date: Mon, 5 Jan 2026 18:32:04 +0200 Subject: [PATCH 08/15] Proved iterate_derivative_mul_X' --- Mathlib/Algebra/Polynomial/Derivative.lean | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean index 3f477ea99d3ed3..036c39aa0dea55 100644 --- a/Mathlib/Algebra/Polynomial/Derivative.lean +++ b/Mathlib/Algebra/Polynomial/Derivative.lean @@ -540,11 +540,19 @@ theorem iterate_derivative_mul_X_pow {n m} (p : R[X]) : rw [Nat.descFactorial_eq_zero_iff_lt.mpr (by grind)] simp -theorem iterate_derivative_mul_X {n} (p : R[X]) : +theorem iterate_derivative_mul_X' {n} (p : R[X]) : derivative^[n] (derivative p * X) = (derivative^[n + 1] p) * X + n • derivative^[n] p := by - sorry + trans derivative^[n] (derivative p * X ^ 1) + · simp + rw [iterate_derivative_mul_X_pow] + by_cases n = 0 + case pos h => simp [h] + case neg h => + rw [min_eq_left (by omega), show range 2 = {0, 1} by grind, + show derivative^[n] p = derivative^[n - 1 + 1] p by grind] + simp -theorem iterate_derivative_mul_X_sq {n} (p : R[X]) : +theorem iterate_derivative_mul_X_sq' {n} (p : R[X]) : derivative^[n] (derivative^[2] p * X ^ 2) = (derivative^[n + 2] p) * X ^ 2 + (2 * n) • (derivative^[n + 1] p) * X + (n * (n - 1)) • derivative^[n] p := by From 9cdd64702000e3294d094d6f96e24028c6a69f7c Mon Sep 17 00:00:00 2001 From: Yuval Filmus Date: Mon, 5 Jan 2026 18:57:59 +0200 Subject: [PATCH 09/15] Completed proof of iterate_derivative_mul_X_sq' --- Mathlib/Algebra/Polynomial/Derivative.lean | 25 +++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean index 036c39aa0dea55..a96968a0699f7e 100644 --- a/Mathlib/Algebra/Polynomial/Derivative.lean +++ b/Mathlib/Algebra/Polynomial/Derivative.lean @@ -556,7 +556,30 @@ theorem iterate_derivative_mul_X_sq' {n} (p : R[X]) : derivative^[n] (derivative^[2] p * X ^ 2) = (derivative^[n + 2] p) * X ^ 2 + (2 * n) • (derivative^[n + 1] p) * X + (n * (n - 1)) • derivative^[n] p := by - sorry + rw [iterate_derivative_mul_X_pow] + by_cases n = 0 + case pos h => simp [h] + case neg h => + by_cases n = 1 + case pos h' => + rw [h', min_eq_right (by norm_num), show range 2 = {0, 1} by grind] + simp; ring + case neg h' => + rw [min_eq_left (by omega), show range 3 = {0, 1, 2} by grind, + show derivative^[n] p = derivative^[n - 2 + 2] p by grind, + show derivative^[n + 1] p = derivative^[n - 1 + 2] p by grind] + have cf₁ : Nat.descFactorial 2 1 = 2 := by simp + have cf₂ : + (n.choose 2 : R[X]) * (Nat.descFactorial 2 2 : R[X]) = ((n * (n - 1) : ℕ) : R[X]) := by + norm_cast + congr 1 + rw [Nat.choose_two_right, Nat.descFactorial_self, Nat.factorial_two, Nat.div_mul_cancel] + cases n with + | zero => simp + | succ n => + rw [Nat.add_sub_cancel, mul_comm] + exact Nat.two_dvd_mul_add_one n + simp [-Nat.descFactorial_succ, cf₁, cf₂]; ring theorem derivative_comp (p q : R[X]) : derivative (p.comp q) = derivative q * p.derivative.comp q := by From de7daf168f6058dcb11cca6e820adf2176a81057 Mon Sep 17 00:00:00 2001 From: Yuval Filmus Date: Mon, 5 Jan 2026 19:32:19 +0200 Subject: [PATCH 10/15] Simplified proof --- Mathlib/Algebra/Polynomial/Derivative.lean | 8 ++------ Mathlib/Algebra/Ring/Parity.lean | 4 ++++ 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean index a96968a0699f7e..0a60408af0a5e3 100644 --- a/Mathlib/Algebra/Polynomial/Derivative.lean +++ b/Mathlib/Algebra/Polynomial/Derivative.lean @@ -573,12 +573,8 @@ theorem iterate_derivative_mul_X_sq' {n} (p : R[X]) : (n.choose 2 : R[X]) * (Nat.descFactorial 2 2 : R[X]) = ((n * (n - 1) : ℕ) : R[X]) := by norm_cast congr 1 - rw [Nat.choose_two_right, Nat.descFactorial_self, Nat.factorial_two, Nat.div_mul_cancel] - cases n with - | zero => simp - | succ n => - rw [Nat.add_sub_cancel, mul_comm] - exact Nat.two_dvd_mul_add_one n + grind [Nat.choose_two_right, Nat.descFactorial_self, Nat.factorial_two, + Nat.two_dvd_mul_sub_one] simp [-Nat.descFactorial_succ, cf₁, cf₂]; ring theorem derivative_comp (p q : R[X]) : diff --git a/Mathlib/Algebra/Ring/Parity.lean b/Mathlib/Algebra/Ring/Parity.lean index 4d2629c0d9a8c3..1cbb61cdde79c7 100644 --- a/Mathlib/Algebra/Ring/Parity.lean +++ b/Mathlib/Algebra/Ring/Parity.lean @@ -306,6 +306,10 @@ lemma one_add_div_two_mul_two_of_odd (h : Odd n) : 1 + n / 2 * 2 = n := by grind lemma two_dvd_mul_add_one (k : ℕ) : 2 ∣ k * (k + 1) := even_iff_two_dvd.mp (even_mul_succ_self k) +lemma two_dvd_mul_sub_one (k : ℕ) : 2 ∣ k * (k - 1) := + (@Nat.eq_zero_or_eq_sub_one_add_one k).elim (by grind) + (by grind [Nat.two_dvd_mul_add_one (k - 1)]) + -- Here are examples of how `parity_simps` can be used with `Nat`. example (m n : ℕ) (h : Even m) : ¬Even (n + 3) ↔ Even (m ^ 2 + m + n) := by simp [*, parity_simps] From 59d238f7e3f28f9f20ba322c24359211daca776e Mon Sep 17 00:00:00 2001 From: Yuval Filmus Date: Tue, 6 Jan 2026 16:10:19 +0200 Subject: [PATCH 11/15] Update Mathlib/Algebra/Polynomial/Derivative.lean Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com> --- Mathlib/Algebra/Polynomial/Derivative.lean | 26 +++++++++------------- 1 file changed, 10 insertions(+), 16 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean index 0a60408af0a5e3..ee88dd2081672e 100644 --- a/Mathlib/Algebra/Polynomial/Derivative.lean +++ b/Mathlib/Algebra/Polynomial/Derivative.lean @@ -516,29 +516,23 @@ theorem iterate_derivative_X_add_pow (n k : ℕ) (c : R) : Nat.cast_mul] ring -theorem iterate_derivative_mul_X_pow {n m} (p : R[X]) : +theorem iterate_derivative_mul_X_pow (n m : ℕ) (p : R[X]) : derivative^[n] (p * X ^ m) = ∑ k ∈ range (min m n).succ, - ((n.choose k * m.descFactorial k) • (derivative^[n - k] p * X ^ (m - k))) := by + (n.choose k * m.descFactorial k) • (derivative^[n - k] p * X ^ (m - k)) := by 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 - rw [iterate_derivative_mul] - congr! 1 with k hk - rw [iterate_derivative_X_pow_eq_smul, ← smul_smul] + (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 rw [hsum] - by_cases! n ≤ m - case pos h => simp [h] - case neg h => - rw [min_eq_left_of_lt h, ← add_zero (∑ k ∈ range m.succ, _), - show range n.succ = range m.succ ∪ Ico m.succ n.succ by grind, - sum_union (by rw [range_eq_Ico]; apply Ico_disjoint_Ico_consecutive)] - congr 1 - refine sum_eq_zero (fun k hk => ?_) - rw [Nat.descFactorial_eq_zero_iff_lt.mpr (by grind)] - simp + refine sum_congr_of_eq_on_inter (fun k hk hk' ↦ ?_) (by aesop) (by simp) + rcases le_or_gt k m with hkm | hkm + · replace hk' : n < k := by simpa [hkm] using hk' + simp [Nat.choose_eq_zero_of_lt hk'] + · simp [Nat.descFactorial_eq_zero_iff_lt.mpr hkm] theorem iterate_derivative_mul_X' {n} (p : R[X]) : derivative^[n] (derivative p * X) = (derivative^[n + 1] p) * X + n • derivative^[n] p := by From 811f5ddee85c771925ce6a2e7265c35c1ca26c12 Mon Sep 17 00:00:00 2001 From: Yuval Filmus Date: Tue, 6 Jan 2026 16:10:30 +0200 Subject: [PATCH 12/15] Update Mathlib/Algebra/Polynomial/Derivative.lean Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com> --- Mathlib/Algebra/Polynomial/Derivative.lean | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean index ee88dd2081672e..fa761127ba1d1e 100644 --- a/Mathlib/Algebra/Polynomial/Derivative.lean +++ b/Mathlib/Algebra/Polynomial/Derivative.lean @@ -534,17 +534,10 @@ theorem iterate_derivative_mul_X_pow (n m : ℕ) (p : R[X]) : simp [Nat.choose_eq_zero_of_lt hk'] · simp [Nat.descFactorial_eq_zero_iff_lt.mpr hkm] -theorem iterate_derivative_mul_X' {n} (p : R[X]) : +theorem iterate_derivative_derivative_mul_X {n : ℕ} (p : R[X]) : derivative^[n] (derivative p * X) = (derivative^[n + 1] p) * X + n • derivative^[n] p := by - trans derivative^[n] (derivative p * X ^ 1) - · simp - rw [iterate_derivative_mul_X_pow] - by_cases n = 0 - case pos h => simp [h] - case neg h => - rw [min_eq_left (by omega), show range 2 = {0, 1} by grind, - show derivative^[n] p = derivative^[n - 1 + 1] p by grind] - simp + convert (derivative p).iterate_derivative_mul_X_pow n 1; · simp + rcases n with rfl | n <;> simp [sum_range_succ] theorem iterate_derivative_mul_X_sq' {n} (p : R[X]) : derivative^[n] (derivative^[2] p * X ^ 2) = From f0b5b5add780c4a2e9f8a67acb9fc112ef4fbcd4 Mon Sep 17 00:00:00 2001 From: Yuval Filmus Date: Tue, 6 Jan 2026 16:10:40 +0200 Subject: [PATCH 13/15] Update Mathlib/Algebra/Polynomial/Derivative.lean Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com> --- Mathlib/Algebra/Polynomial/Derivative.lean | 32 +++++++--------------- 1 file changed, 10 insertions(+), 22 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean index fa761127ba1d1e..fb7d47a5c549d3 100644 --- a/Mathlib/Algebra/Polynomial/Derivative.lean +++ b/Mathlib/Algebra/Polynomial/Derivative.lean @@ -539,30 +539,18 @@ theorem iterate_derivative_derivative_mul_X {n : ℕ} (p : R[X]) : convert (derivative p).iterate_derivative_mul_X_pow n 1; · simp rcases n with rfl | n <;> simp [sum_range_succ] -theorem iterate_derivative_mul_X_sq' {n} (p : R[X]) : +theorem iterate_derivative_derivative_mul_X_sq {n : ℕ} (p : R[X]) : derivative^[n] (derivative^[2] p * X ^ 2) = (derivative^[n + 2] p) * X ^ 2 + (2 * n) • (derivative^[n + 1] p) * X + - (n * (n - 1)) • derivative^[n] p := by - rw [iterate_derivative_mul_X_pow] - by_cases n = 0 - case pos h => simp [h] - case neg h => - by_cases n = 1 - case pos h' => - rw [h', min_eq_right (by norm_num), show range 2 = {0, 1} by grind] - simp; ring - case neg h' => - rw [min_eq_left (by omega), show range 3 = {0, 1, 2} by grind, - show derivative^[n] p = derivative^[n - 2 + 2] p by grind, - show derivative^[n + 1] p = derivative^[n - 1 + 2] p by grind] - have cf₁ : Nat.descFactorial 2 1 = 2 := by simp - have cf₂ : - (n.choose 2 : R[X]) * (Nat.descFactorial 2 2 : R[X]) = ((n * (n - 1) : ℕ) : R[X]) := by - norm_cast - congr 1 - grind [Nat.choose_two_right, Nat.descFactorial_self, Nat.factorial_two, - Nat.two_dvd_mul_sub_one] - simp [-Nat.descFactorial_succ, cf₁, cf₂]; ring + (n * (n - 1)) • derivative^[n] p := by + convert (derivative^[2] p).iterate_derivative_mul_X_pow n 2 + rcases n with rfl | n; · simp + rcases n with rfl | n; · simp [sum_range_succ, ← mul_assoc] + suffices ((n + 1 + 1) * (n + 1) / 2) * 2 = (n + 1 + 1) * (n + 1) by + simp [this, -nsmul_eq_mul, sum_range_succ, Nat.choose_two_right] + ring + rw [mul_comm (n + 1 + 1)] + exact Nat.div_mul_cancel (Nat.two_dvd_mul_add_one _) theorem derivative_comp (p q : R[X]) : derivative (p.comp q) = derivative q * p.derivative.comp q := by From b921db7bf0d6d56c9dfe8b1358de1b11b4c6ac84 Mon Sep 17 00:00:00 2001 From: Yuval Filmus Date: Tue, 6 Jan 2026 16:11:04 +0200 Subject: [PATCH 14/15] Update Mathlib/Algebra/Ring/Parity.lean Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com> --- Mathlib/Algebra/Ring/Parity.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Ring/Parity.lean b/Mathlib/Algebra/Ring/Parity.lean index 1cbb61cdde79c7..bc6dc698e21575 100644 --- a/Mathlib/Algebra/Ring/Parity.lean +++ b/Mathlib/Algebra/Ring/Parity.lean @@ -306,9 +306,9 @@ lemma one_add_div_two_mul_two_of_odd (h : Odd n) : 1 + n / 2 * 2 = n := by grind lemma two_dvd_mul_add_one (k : ℕ) : 2 ∣ k * (k + 1) := even_iff_two_dvd.mp (even_mul_succ_self k) -lemma two_dvd_mul_sub_one (k : ℕ) : 2 ∣ k * (k - 1) := - (@Nat.eq_zero_or_eq_sub_one_add_one k).elim (by grind) - (by grind [Nat.two_dvd_mul_add_one (k - 1)]) +lemma two_dvd_mul_sub_one (k : ℕ) : 2 ∣ k * (k - 1) := by + rcases k with rfl | k; · simp + simpa [mul_comm (k + 1)] using k.two_dvd_mul_add_one -- Here are examples of how `parity_simps` can be used with `Nat`. example (m n : ℕ) (h : Even m) : ¬Even (n + 3) ↔ Even (m ^ 2 + m + n) := by From 3acf37586faa28f1868b09f64d5e392827209ca8 Mon Sep 17 00:00:00 2001 From: Yuval Filmus Date: Tue, 6 Jan 2026 16:47:44 +0200 Subject: [PATCH 15/15] Added iterate_derivative_mul_X --- Mathlib/Algebra/Polynomial/Derivative.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean index fb7d47a5c549d3..83e722ea2c1fdc 100644 --- a/Mathlib/Algebra/Polynomial/Derivative.lean +++ b/Mathlib/Algebra/Polynomial/Derivative.lean @@ -534,6 +534,11 @@ theorem iterate_derivative_mul_X_pow (n m : ℕ) (p : R[X]) : simp [Nat.choose_eq_zero_of_lt hk'] · simp [Nat.descFactorial_eq_zero_iff_lt.mpr hkm] +theorem iterate_derivative_mul_X {n : ℕ} (p : R[X]) : + derivative^[n] (p * X) = (derivative^[n] p) * X + n • derivative^[n - 1] p := by + convert p.iterate_derivative_mul_X_pow n 1; · simp + rcases n with rfl | n <;> simp [sum_range_succ] + theorem iterate_derivative_derivative_mul_X {n : ℕ} (p : R[X]) : derivative^[n] (derivative p * X) = (derivative^[n + 1] p) * X + n • derivative^[n] p := by convert (derivative p).iterate_derivative_mul_X_pow n 1; · simp