awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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])
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])
⊢ (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 * p) ((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 q : R[X]
n : ℕ
dvd : q ^ n ∣ p
⊢ q ^ (n - 1) ∣ (derivative : (a : R[X]) → R[X]) p
have obtain : ∀ (r : R[X]), q ^ (n - 1) ∣ (derivative : (a : R[X]) → R[X]) (q ^ n * r)
Tactic: obtain ⟨r, rfl⟩ := dvd
Cleared hypotheses: p, dvd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
q : R[X]
n : ℕ
r : R[X]
⊢ q ^ (n - 1) ∣ (derivative : (a : R[X]) → R[X]) (q ^ n * r)
have rw : q ^ (n - 1) ∣
  HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑n : R) * q ^ (n - 1)) ((derivative : (a : R[X]) → R[X]) q : R[X]) * r +
    HMul.hMul (β := R[X]) (q ^ n) ((derivative : (a : R[X]) → R[X]) r : R[X])
Tactic: rw [derivative_mul, derivative_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
q : R[X]
n m : ℕ
ih : ∀ {p : R[X]} (dvd : q ^ n ∣ p), q ^ (n - m) ∣ (⇑derivative : (a : R[X]) → R[X])^[m] p
p : R[X]
dvd : q ^ n ∣ p
⊢ q ^ (n - (m + 1)) ∣ (⇑derivative : (a : R[X]) → R[X])^[m + 1] p
have succ : q ^ (n - m).pred ∣ ((⇑derivative : (a : R[X]) → R[X]) ∘ (⇑derivative : (a : R[X]) → R[X])^[m]) p
Tactic: rw [Nat.sub_succ, Function.iterate_succ']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
n m : ℕ
dvd : q ^ n ∣ p
⊢ q ^ (n - m) ∣ (⇑derivative : (a : R[X]) → R[X])^[m] p
have zero : ∀ {p : R[X]} (dvd : q ^ n ∣ p), q ^ (n - 0) ∣ (⇑derivative : (a : R[X]) → R[X])^[0] p
Tactic: induction m generalizing p with
  | zero => simpa
  | succ m ih =>
    rw [Nat.sub_succ, Function.iterate_succ']
    exact pow_sub_one_dvd_derivative_of_pow_dvd (ih dvd)
Cleared hypotheses: p, m, dvd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
n m : ℕ
dvd : q ^ n ∣ p
zero : ∀ {p : R[X]} (dvd : q ^ n ∣ p), q ^ (n - 0) ∣ (⇑derivative : (a : R[X]) → R[X])^[0] p
⊢ q ^ (n - m) ∣ (⇑derivative : (a : R[X]) → R[X])^[m] p
have succ : ∀ (m : ℕ) (ih : ∀ {p : R[X]} (dvd : q ^ n ∣ p), q ^ (n - m) ∣ (⇑derivative : (a : R[X]) → R[X])^[m] p) {p : R[X]}
  (dvd : q ^ n ∣ p), q ^ (n - (m + 1)) ∣ (⇑derivative : (a : R[X]) → R[X])^[m + 1] p
Tactic: induction m generalizing p with
  | zero => simpa
  | succ m ih =>
    rw [Nat.sub_succ, Function.iterate_succ']
    exact pow_sub_one_dvd_derivative_of_pow_dvd (ih dvd)
Cleared hypotheses: p, m, dvd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n m : ℕ
c : R
hm : m ≠ 0
⊢ (↑n : R) ∣ eval c ((⇑derivative : (a : R[X]) → R[X])^[m] (f ^ n))
have obtain : ∀ (m : ℕ) (hm : m.succ ≠ 0), (↑n : R) ∣ eval c ((⇑derivative : (a : R[X]) → R[X])^[m.succ] (f ^ n))
Tactic: obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ (↑n : R) ∣ eval c ((⇑derivative : (a : R[X]) → R[X])^[m.succ] (f ^ n))
have rw : (↑n : R) ∣
  (↑n : R) *
    eval c
      ((⇑derivative : (a : R[X]) → R[X])^[m]
        (HMul.hMul (β := R[X]) (f ^ (n - 1)) ((derivative : (a : R[X]) → R[X]) f : R[X])))
Tactic: rw [Function.iterate_succ_apply, derivative_pow, mul_assoc, C_eq_natCast,
    iterate_derivative_natCast_mul, eval_mul, eval_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
⊢ (⇑derivative : (a : R[X]) → R[X])^[0] (HPow.hPow (α := R[X]) X n) =
    (↑(n.descFactorial 0) : R[X]) * HPow.hPow (α := R[X]) X (n - 0)
have zero : HPow.hPow (α := R[X]) X n = (↑(n.descFactorial 0) : R[X]) * HPow.hPow (α := R[X]) X (n - 0)
Tactic: rw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
zero : HPow.hPow (α := R[X]) X n = (↑(n.descFactorial 0) : R[X]) * HPow.hPow (α := R[X]) X (n - 0)
⊢ (⇑derivative : (a : R[X]) → R[X])^[0] (HPow.hPow (α := R[X]) X n) =
    (↑(n.descFactorial 0) : R[X]) * HPow.hPow (α := R[X]) X (n - 0)
have zero₁ : HPow.hPow (α := R[X]) X n = (↑(n.descFactorial 0) : R[X]) * HPow.hPow (α := R[X]) X n
Tactic: rw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
zero : HPow.hPow (α := R[X]) X n = (↑(n.descFactorial 0) : R[X]) * HPow.hPow (α := R[X]) X (n - 0)
zero₁ : HPow.hPow (α := R[X]) X n = (↑(n.descFactorial 0) : R[X]) * HPow.hPow (α := R[X]) X n
⊢ (⇑derivative : (a : R[X]) → R[X])^[0] (HPow.hPow (α := R[X]) X n) =
    (↑(n.descFactorial 0) : R[X]) * HPow.hPow (α := R[X]) X (n - 0)
have zero₂ : HPow.hPow (α := R[X]) X n = (↑1 : R[X]) * HPow.hPow (α := R[X]) X n
Tactic: rw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
zero : HPow.hPow (α := R[X]) X n = (↑(n.descFactorial 0) : R[X]) * HPow.hPow (α := R[X]) X (n - 0)
zero₁ : HPow.hPow (α := R[X]) X n = (↑(n.descFactorial 0) : R[X]) * HPow.hPow (α := R[X]) X n
zero₂ : HPow.hPow (α := R[X]) X n = (↑1 : R[X]) * HPow.hPow (α := R[X]) X n
⊢ (⇑derivative : (a : R[X]) → R[X])^[0] (HPow.hPow (α := R[X]) X n) =
    (↑(n.descFactorial 0) : R[X]) * HPow.hPow (α := R[X]) X (n - 0)
have zero₃ : HPow.hPow (α := R[X]) X n = 1 * HPow.hPow (α := R[X]) X n
Tactic: rw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
zero : HPow.hPow (α := R[X]) X n = (↑(n.descFactorial 0) : R[X]) * HPow.hPow (α := R[X]) X (n - 0)
zero₁ : HPow.hPow (α := R[X]) X n = (↑(n.descFactorial 0) : R[X]) * HPow.hPow (α := R[X]) X n
zero₂ : HPow.hPow (α := R[X]) X n = (↑1 : R[X]) * HPow.hPow (α := R[X]) X n
zero₃ : HPow.hPow (α := R[X]) X n = 1 * HPow.hPow (α := R[X]) X n
⊢ (⇑derivative : (a : R[X]) → R[X])^[0] (HPow.hPow (α := R[X]) X n) =
    (↑(n.descFactorial 0) : R[X]) * HPow.hPow (α := R[X]) X (n - 0)
have zero₄ : HPow.hPow (α := R[X]) X n = HPow.hPow (α := R[X]) X n
Tactic: rw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n k : ℕ
ih :
  (⇑derivative : (a : R[X]) → R[X])^[k] (HPow.hPow (α := R[X]) X n) =
    (↑(n.descFactorial k) : R[X]) * HPow.hPow (α := R[X]) X (n - k)
⊢ (⇑derivative : (a : R[X]) → R[X])^[k + 1] (HPow.hPow (α := R[X]) X n) =
    (↑(n.descFactorial (k + 1)) : R[X]) * HPow.hPow (α := R[X]) X (n - (k + 1))
have succ : (↑(n.descFactorial k) : R[X]) * ((↑(n - k) : R[X]) * HPow.hPow (α := R[X]) X (n - (k + 1))) =
  HMul.hMul (α := R[X]) (↑(n - k) : R[X]) (↑(n.descFactorial k) : R[X]) * HPow.hPow (α := R[X]) X (n - (k + 1))
Tactic: rw [Function.iterate_succ_apply', ih, derivative_natCast_mul, derivative_X_pow, C_eq_natCast,
      Nat.descFactorial_succ, Nat.sub_sub, Nat.cast_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n k : ℕ
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (HPow.hPow (α := R[X]) X n) =
    (↑(n.descFactorial k) : R[X]) * HPow.hPow (α := R[X]) X (n - k)
have zero : (⇑derivative : (a : R[X]) → R[X])^[0] (HPow.hPow (α := R[X]) X n) =
  (↑(n.descFactorial 0) : R[X]) * HPow.hPow (α := R[X]) X (n - 0)
Tactic: induction k with
  | zero =>
    rw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]
  | succ k ih =>
    rw [Function.iterate_succ_apply', ih, derivative_natCast_mul, derivative_X_pow, C_eq_natCast,
      Nat.descFactorial_succ, Nat.sub_sub, Nat.cast_mul]
    simp [mul_assoc, mul_left_comm]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n k : ℕ
zero :
  (⇑derivative : (a : R[X]) → R[X])^[0] (HPow.hPow (α := R[X]) X n) =
    (↑(n.descFactorial 0) : R[X]) * HPow.hPow (α := R[X]) X (n - 0)
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (HPow.hPow (α := R[X]) X n) =
    (↑(n.descFactorial k) : R[X]) * HPow.hPow (α := R[X]) X (n - k)
have succ : ∀ (k : ℕ)
  (ih :
    (⇑derivative : (a : R[X]) → R[X])^[k] (HPow.hPow (α := R[X]) X n) =
      (↑(n.descFactorial k) : R[X]) * HPow.hPow (α := R[X]) X (n - k)),
  (⇑derivative : (a : R[X]) → R[X])^[k + 1] (HPow.hPow (α := R[X]) X n) =
    (↑(n.descFactorial (k + 1)) : R[X]) * HPow.hPow (α := R[X]) X (n - (k + 1))
Tactic: induction k with
  | zero =>
    rw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]
  | succ k ih =>
    rw [Function.iterate_succ_apply', ih, derivative_natCast_mul, derivative_X_pow, C_eq_natCast,
      Nat.descFactorial_succ, Nat.sub_sub, Nat.cast_mul]
    simp [mul_assoc, mul_left_comm]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n k : ℕ
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (HPow.hPow (α := R[X]) X n) =
    (C : (a : R) → R[X]) (↑(n.descFactorial k) : R) * HPow.hPow (α := R[X]) X (n - k)
have rw : (↑(n.descFactorial k) : R[X]) * HPow.hPow (α := R[X]) X (n - k) =
  (C : (a : R) → R[X]) (↑(n.descFactorial k) : R) * HPow.hPow (α := R[X]) X (n - k)
Tactic: rw [iterate_derivative_X_pow_eq_natCast_mul n k, C_eq_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n k : ℕ
rw :
  (↑(n.descFactorial k) : R[X]) * HPow.hPow (α := R[X]) X (n - k) =
    (C : (a : R) → R[X]) (↑(n.descFactorial k) : R) * HPow.hPow (α := R[X]) X (n - k)
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (HPow.hPow (α := R[X]) X n) =
    (C : (a : R) → R[X]) (↑(n.descFactorial k) : R) * HPow.hPow (α := R[X]) X (n - k)
have rw₁ : (↑(n.descFactorial k) : R[X]) * HPow.hPow (α := R[X]) X (n - k) =
  (↑(n.descFactorial k) : R[X]) * HPow.hPow (α := R[X]) X (n - k)
Tactic: rw [iterate_derivative_X_pow_eq_natCast_mul n k, C_eq_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n k : ℕ
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (HPow.hPow (α := R[X]) X n) =
    HSMul.hSMul (α := R) (↑(n.descFactorial k) : R) (HPow.hPow (α := R[X]) X (n - k))
have rw : (C : (a : R) → R[X]) (↑(n.descFactorial k) : R) * HPow.hPow (α := R[X]) X (n - k) =
  HSMul.hSMul (α := R) (↑(n.descFactorial k) : R) (HPow.hPow (α := R[X]) X (n - k))
Tactic: rw [iterate_derivative_X_pow_eq_C_mul n k, smul_eq_C_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n k : ℕ
rw :
  (C : (a : R) → R[X]) (↑(n.descFactorial k) : R) * HPow.hPow (α := R[X]) X (n - k) =
    HSMul.hSMul (α := R) (↑(n.descFactorial k) : R) (HPow.hPow (α := R[X]) X (n - k))
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (HPow.hPow (α := R[X]) X n) =
    HSMul.hSMul (α := R) (↑(n.descFactorial k) : R) (HPow.hPow (α := R[X]) X (n - k))
have rw₁ : (C : (a : R) → R[X]) (↑(n.descFactorial k) : R) * HPow.hPow (α := R[X]) X (n - k) =
  (C : (a : R) → R[X]) (↑(n.descFactorial k) : R) * HPow.hPow (α := R[X]) X (n - k)
Tactic: rw [iterate_derivative_X_pow_eq_C_mul n k, smul_eq_C_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
c : R
m : ℕ
⊢ (derivative : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ m) =
    (C : (a : R) → R[X]) (↑m : R) * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
have rw : HMul.hMul (β := R[X])
    ((C : (a : R) → R[X]) (↑m : R) * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1))
    ((derivative : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X]) =
  (C : (a : R) → R[X]) (↑m : R) * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
Tactic: rw [derivative_pow, derivative_X_add_C, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
c : R
m : ℕ
rw :
  HMul.hMul (β := R[X])
      ((C : (a : R) → R[X]) (↑m : R) * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1))
      ((derivative : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X]) =
    (C : (a : R) → R[X]) (↑m : R) * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
⊢ (derivative : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ m) =
    (C : (a : R) → R[X]) (↑m : R) * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
have rw₁ : (C : (a : R) → R[X]) (↑m : R) * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1) * 1 =
  (C : (a : R) → R[X]) (↑m : R) * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
Tactic: rw [derivative_pow, derivative_X_add_C, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
c : R
m : ℕ
rw :
  HMul.hMul (β := R[X])
      ((C : (a : R) → R[X]) (↑m : R) * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1))
      ((derivative : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X]) =
    (C : (a : R) → R[X]) (↑m : R) * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
rw₁ :
  (C : (a : R) → R[X]) (↑m : R) * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1) * 1 =
    (C : (a : R) → R[X]) (↑m : R) * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
⊢ (derivative : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ m) =
    (C : (a : R) → R[X]) (↑m : R) * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
have rw₂ : (C : (a : R) → R[X]) (↑m : R) * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1) =
  (C : (a : R) → R[X]) (↑m : R) * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
Tactic: rw [derivative_pow, derivative_X_add_C, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
c : R
⊢ (derivative : (a : R[X]) → R[X])
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) 2) =
    (C : (a : R) → R[X]) 2 * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
have rw : HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) 2 * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]))
    ((derivative : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X]) =
  (C : (a : R) → R[X]) 2 * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
Tactic: rw [derivative_sq, derivative_X_add_C, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
c : R
rw :
  HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) 2 * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]))
      ((derivative : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X]) =
    (C : (a : R) → R[X]) 2 * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
⊢ (derivative : (a : R[X]) → R[X])
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) 2) =
    (C : (a : R) → R[X]) 2 * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
have rw₁ : (C : (a : R) → R[X]) 2 * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) * 1 =
  (C : (a : R) → R[X]) 2 * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
Tactic: rw [derivative_sq, derivative_X_add_C, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
c : R
rw :
  HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) 2 * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]))
      ((derivative : (a : R[X]) → R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X]) =
    (C : (a : R) → R[X]) 2 * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
rw₁ :
  (C : (a : R) → R[X]) 2 * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) * 1 =
    (C : (a : R) → R[X]) 2 * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
⊢ (derivative : (a : R[X]) → R[X])
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) 2) =
    (C : (a : R) → R[X]) 2 * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
have rw₂ : (C : (a : R) → R[X]) 2 * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) =
  (C : (a : R) → R[X]) 2 * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])
Tactic: rw [derivative_sq, derivative_X_add_C, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
c : R
k : ℕ
IH :
  (⇑derivative : (a : R[X]) → R[X])^[k] (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
    n.descFactorial k • HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - k)
⊢ (⇑derivative : (a : R[X]) → R[X])^[k + 1] (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
    n.descFactorial (k + 1) • HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - (k + 1))
have succ : (↑(n.descFactorial k) : R[X]) *
    ((↑(n - k) : R[X]) * HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - k - 1)) =
  HMul.hMul (α := R[X]) (↑(n - k) : R[X]) (↑(n.descFactorial k) : R[X]) *
    HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - k - 1)
Tactic: rw [Nat.sub_succ', Function.iterate_succ_apply', IH, derivative_smul,
        derivative_X_add_C_pow, map_natCast, Nat.descFactorial_succ, nsmul_eq_mul, nsmul_eq_mul,
        Nat.cast_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n k : ℕ
c : R
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
    n.descFactorial k • HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - k)
have zero : (⇑derivative : (a : R[X]) → R[X])^[0] (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
  n.descFactorial 0 • HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - 0)
Tactic: induction k with
  | zero => simp
  | succ k IH =>
      rw [Nat.sub_succ', Function.iterate_succ_apply', IH, derivative_smul,
        derivative_X_add_C_pow, map_natCast, Nat.descFactorial_succ, nsmul_eq_mul, nsmul_eq_mul,
        Nat.cast_mul]
      ring
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n k : ℕ
c : R
zero :
  (⇑derivative : (a : R[X]) → R[X])^[0] (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
    n.descFactorial 0 • HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - 0)
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
    n.descFactorial k • HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - k)
have succ : ∀ (k : ℕ)
  (IH :
    (⇑derivative : (a : R[X]) → R[X])^[k] (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
      n.descFactorial k • HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - k)),
  (⇑derivative : (a : R[X]) → R[X])^[k + 1] (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
    n.descFactorial (k + 1) • HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - (k + 1))
Tactic: induction k with
  | zero => simp
  | succ k IH =>
      rw [Nat.sub_succ', Function.iterate_succ_apply', IH, derivative_smul,
        derivative_X_add_C_pow, map_natCast, Nat.descFactorial_succ, nsmul_eq_mul, nsmul_eq_mul,
        Nat.cast_mul]
      ring
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
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 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 simp_rw : Eq.{u + 1} (α := R[X])
  (∑ x ∈ range n.succ,
    n.choose x •
      ((⇑derivative : (a : R[X]) → R[X])^[n - x] p *
        HSMul.hSMul (α := R) (↑(m.descFactorial x) : R) (HPow.hPow (α := R[X]) X (m - x))))
  (∑ x ∈ range n.succ,
    n.choose x • m.descFactorial x • ((⇑derivative : (a : R[X]) → R[X])^[n - x] p * HPow.hPow (α := R[X]) X (m - x)))
Tactic: simp_rw [iterate_derivative_mul, iterate_derivative_X_pow_eq_smul, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
⊢ Eq.{u + 1} (α := R[X])
    (∑ x ∈ range n.succ,
      n.choose x •
        ((⇑derivative : (a : R[X]) → R[X])^[n - x] p *
          HSMul.hSMul (α := R) (↑(m.descFactorial x) : R) (HPow.hPow (α := R[X]) X (m - x))))
    (∑ x ∈ range n.succ,
      n.choose x • m.descFactorial x • ((⇑derivative : (a : R[X]) → R[X])^[n - x] p * HPow.hPow (α := R[X]) X (m - x)))
have a : ∀ (k : ℕ) (hk : k ∈ range n.succ),
  (⇑derivative : (a : R[X]) → R[X])^[n - k] p *
      HSMul.hSMul (α := R) (↑(m.descFactorial k) : R) (HPow.hPow (α := R[X]) X (m - k)) =
    m.descFactorial k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
Tactic: congr! 2 with k hk
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
k : ℕ
hk : k ∈ range n.succ
⊢ (⇑derivative : (a : R[X]) → R[X])^[n - k] p *
      HSMul.hSMul (α := R) (↑(m.descFactorial k) : R) (HPow.hPow (α := R[X]) X (m - k)) =
    m.descFactorial k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
have a : (⇑derivative : (a : R[X]) → R[X])^[n - k] p * m.descFactorial k • HPow.hPow (α := R[X]) X (m - k) =
  m.descFactorial k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
Tactic: norm_cast