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 : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
_ :
  ((⇑derivative : (a : R[X]) → R[X])^[k + 1] p).coeff m =
    (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1
_₁ :
  (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1 =
    ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ)
⊢ ((⇑derivative : (a : R[X]) → R[X])^[k + 1] p).coeff m = (m + (k + 1)).descFactorial (k + 1) • p.coeff (m + (k + 1))
have _₂ : ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ) =
  (m.succ + k).descFactorial k.succ • p.coeff (m + k.succ)
Tactic: calc
        (derivative^[k + 1] p).coeff m
        _ = Nat.descFactorial (Nat.succ (m + k)) k • p.coeff (m + k.succ) * (m + 1) := by
          rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]
        _ = ((m + 1) * Nat.descFactorial (Nat.succ (m + k)) k) • p.coeff (m + k.succ) := by
          rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul]
        _ = Nat.descFactorial (m.succ + k) k.succ • p.coeff (m + k.succ) := by
          rw [← Nat.succ_add, Nat.descFactorial_succ, add_tsub_cancel_right]
        _ = Nat.descFactorial (m + k.succ) k.succ • p.coeff (m + k.succ) := by
          rw [Nat.succ_add_eq_add_succ]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
ih : ∀ (m : ℕ), ((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
m : ℕ
_ :
  ((⇑derivative : (a : R[X]) → R[X])^[k + 1] p).coeff m =
    (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1
_₁ :
  (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1 =
    ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ)
_₂ :
  ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ) =
    (m.succ + k).descFactorial k.succ • p.coeff (m + k.succ)
⊢ ((⇑derivative : (a : R[X]) → R[X])^[k + 1] p).coeff m = (m + (k + 1)).descFactorial (k + 1) • p.coeff (m + (k + 1))
have _₃ : (m.succ + k).descFactorial k.succ • p.coeff (m + k.succ) = (m + k.succ).descFactorial k.succ • p.coeff (m + k.succ)
Tactic: calc
        (derivative^[k + 1] p).coeff m
        _ = Nat.descFactorial (Nat.succ (m + k)) k • p.coeff (m + k.succ) * (m + 1) := by
          rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]
        _ = ((m + 1) * Nat.descFactorial (Nat.succ (m + k)) k) • p.coeff (m + k.succ) := by
          rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul]
        _ = Nat.descFactorial (m.succ + k) k.succ • p.coeff (m + k.succ) := by
          rw [← Nat.succ_add, Nat.descFactorial_succ, add_tsub_cancel_right]
        _ = Nat.descFactorial (m + k.succ) k.succ • p.coeff (m + k.succ) := by
          rw [Nat.succ_add_eq_add_succ]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
k : ℕ
p : R[X]
m : ℕ
⊢ ((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
have zero : ∀ (m : ℕ), ((⇑derivative : (a : R[X]) → R[X])^[0] p).coeff m = (m + 0).descFactorial 0 • p.coeff (m + 0)
Tactic: induction k generalizing m with
  | zero => simp
  | succ k ih =>
      calc
        (derivative^[k + 1] p).coeff m
        _ = Nat.descFactorial (Nat.succ (m + k)) k • p.coeff (m + k.succ) * (m + 1) := by
          rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]
        _ = ((m + 1) * Nat.descFactorial (Nat.succ (m + k)) k) • p.coeff (m + k.succ) := by
          rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul]
        _ = Nat.descFactorial (m.succ + k) k.succ • p.coeff (m + k.succ) := by
          rw [← Nat.succ_add, Nat.descFactorial_succ, add_tsub_cancel_right]
        _ = Nat.descFactorial (m + k.succ) k.succ • p.coeff (m + k.succ) := by
          rw [Nat.succ_add_eq_add_succ]
Cleared hypotheses: k, m
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
k : ℕ
p : R[X]
m : ℕ
zero : ∀ (m : ℕ), ((⇑derivative : (a : R[X]) → R[X])^[0] p).coeff m = (m + 0).descFactorial 0 • p.coeff (m + 0)
⊢ ((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
have succ : ∀ (k : ℕ)
  (ih : ∀ (m : ℕ), ((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k))
  (m : ℕ),
  ((⇑derivative : (a : R[X]) → R[X])^[k + 1] p).coeff m = (m + (k + 1)).descFactorial (k + 1) • p.coeff (m + (k + 1))
Tactic: induction k generalizing m with
  | zero => simp
  | succ k ih =>
      calc
        (derivative^[k + 1] p).coeff m
        _ = Nat.descFactorial (Nat.succ (m + k)) k • p.coeff (m + k.succ) * (m + 1) := by
          rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]
        _ = ((m + 1) * Nat.descFactorial (Nat.succ (m + k)) k) • p.coeff (m + k.succ) := by
          rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul]
        _ = Nat.descFactorial (m.succ + k) k.succ • p.coeff (m + k.succ) := by
          rw [← Nat.succ_add, Nat.descFactorial_succ, add_tsub_cancel_right]
        _ = Nat.descFactorial (m + k.succ) k.succ • p.coeff (m + k.succ) := by
          rw [Nat.succ_add_eq_add_succ]
Cleared hypotheses: k, m
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
| (⇑derivative : (a : R[X]) → R[X])^[k] p
have rw : ∑ i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff i) : R[X])
    (HPow.hPow (α := R[X]) X i)
Tactic: rw [(derivative^[k] p).as_sum_support_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] p =
    ∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
        (HPow.hPow (α := R[X]) X x)
have conv_lhs : Eq.{u + 1} (α := R[X])
  (∑ i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff i) : R[X])
      (HPow.hPow (α := R[X]) X i))
  (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
      (HPow.hPow (α := R[X]) X x))
Tactic: conv_lhs => rw [(derivative^[k] p).as_sum_support_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
⊢ Eq.{u + 1} (α := R[X])
    (∑ i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff i) : R[X])
        (HPow.hPow (α := R[X]) X i))
    (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
        (HPow.hPow (α := R[X]) X x))
have refine : ∀ i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff i) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i)
Tactic: refine sum_congr rfl fun i _ ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k i : ℕ
h : i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff i) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i)
have rw : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
    (HPow.hPow (α := R[X]) X i) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
    (HPow.hPow (α := R[X]) X i)
Tactic: rw [coeff_iterate_derivative, Nat.descFactorial_eq_factorial_mul_choose]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k i : ℕ
h : i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i)
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff i) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i)
have rw₁ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((k ! * (i + k).choose k) • p.coeff (i + k)) : R[X])
    (HPow.hPow (α := R[X]) X i) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((k ! * (i + k).choose k) • p.coeff (i + k)) : R[X])
    (HPow.hPow (α := R[X]) X i)
Tactic: rw [coeff_iterate_derivative, Nat.descFactorial_eq_factorial_mul_choose]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
| (⇑derivative : (a : R[X]) → R[X])^[k] p
have rw : ∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
    (HPow.hPow (α := R[X]) X x)
Tactic: rw [iterate_derivative_eq_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] p =
    HSMul.hSMul (β := R[X]) k !
      (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).choose k • p.coeff (x + k)) : R[X])
          (HPow.hPow (α := R[X]) X x))
have conv_lhs : ∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
      (HPow.hPow (α := R[X]) X x) =
  HSMul.hSMul (β := R[X]) k !
    (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).choose k • p.coeff (x + k)) : R[X])
        (HPow.hPow (α := R[X]) X x))
Tactic: conv_lhs => rw [iterate_derivative_eq_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
⊢ ∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
        (HPow.hPow (α := R[X]) X x) =
    HSMul.hSMul (β := R[X]) k !
      (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).choose k • p.coeff (x + k)) : R[X])
          (HPow.hPow (α := R[X]) X x))
have rw : Eq.{u + 1} (α := R[X])
  (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
      (HPow.hPow (α := R[X]) X x))
  (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
    k ! •
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).choose k • p.coeff (x + k)) : R[X])
        (HPow.hPow (α := R[X]) X x))
Tactic: rw [smul_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
⊢ Eq.{u + 1} (α := R[X])
    (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).descFactorial k • p.coeff (x + k)) : R[X])
        (HPow.hPow (α := R[X]) X x))
    (∑ x ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
      k ! •
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((x + k).choose k • p.coeff (x + k)) : R[X])
          (HPow.hPow (α := R[X]) X x))
have refine : ∀ i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support,
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    k ! •
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).choose k • p.coeff (i + k)) : R[X])
        (HPow.hPow (α := R[X]) X i)
Tactic: refine sum_congr rfl fun i _ ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k i : ℕ
h : i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    k ! •
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).choose k • p.coeff (i + k)) : R[X])
        (HPow.hPow (α := R[X]) X i)
have rw : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
    (HPow.hPow (α := R[X]) X i) =
  HSMul.hSMul (β := R[X]) k ! ((C : (a : R) → R[X]) ((i + k).choose k • p.coeff (i + k)) : R[X]) *
    HPow.hPow (α := R[X]) X i
Tactic: rw [← smul_mul_assoc, smul_C, smul_smul, Nat.descFactorial_eq_factorial_mul_choose]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k i : ℕ
h : i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    HSMul.hSMul (β := R[X]) k ! ((C : (a : R) → R[X]) ((i + k).choose k • p.coeff (i + k)) : R[X]) *
      HPow.hPow (α := R[X]) X i
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    k ! •
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).choose k • p.coeff (i + k)) : R[X])
        (HPow.hPow (α := R[X]) X i)
have rw₁ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
    (HPow.hPow (α := R[X]) X i) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (k ! • (i + k).choose k • p.coeff (i + k)) : R[X])
    (HPow.hPow (α := R[X]) X i)
Tactic: rw [← smul_mul_assoc, smul_C, smul_smul, Nat.descFactorial_eq_factorial_mul_choose]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k i : ℕ
h : i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    HSMul.hSMul (β := R[X]) k ! ((C : (a : R) → R[X]) ((i + k).choose k • p.coeff (i + k)) : R[X]) *
      HPow.hPow (α := R[X]) X i
rw₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (k ! • (i + k).choose k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i)
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    k ! •
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).choose k • p.coeff (i + k)) : R[X])
        (HPow.hPow (α := R[X]) X i)
have rw₂ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
    (HPow.hPow (α := R[X]) X i) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((k ! * (i + k).choose k) • p.coeff (i + k)) : R[X])
    (HPow.hPow (α := R[X]) X i)
Tactic: rw [← smul_mul_assoc, smul_C, smul_smul, Nat.descFactorial_eq_factorial_mul_choose]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
k i : ℕ
h : i ∈ ((⇑derivative : (a : R[X]) → R[X])^[k] p).support
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    HSMul.hSMul (β := R[X]) k ! ((C : (a : R) → R[X]) ((i + k).choose k • p.coeff (i + k)) : R[X]) *
      HPow.hPow (α := R[X]) X i
rw₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (k ! • (i + k).choose k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i)
rw₂ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((k ! * (i + k).choose k) • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i)
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).descFactorial k • p.coeff (i + k)) : R[X])
      (HPow.hPow (α := R[X]) X i) =
    k ! •
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((i + k).choose k • p.coeff (i + k)) : R[X])
        (HPow.hPow (α := R[X]) X i)
have rw₃ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((k ! * (i + k).choose k) • p.coeff (i + k)) : R[X])
    (HPow.hPow (α := R[X]) X i) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((k ! * (i + k).choose k) • p.coeff (i + k)) : R[X])
    (HPow.hPow (α := R[X]) X i)
Tactic: rw [← smul_mul_assoc, smul_C, smul_smul, Nat.descFactorial_eq_factorial_mul_choose]
-- 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)
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 1] (p * q) =
    (derivative : (a : R[X]) → R[X])
      (∑ 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 rw : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n] (p * q)) : R[X])
  ((derivative : (a : R[X]) → R[X])
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)) :
    R[X])
Tactic: rw [Function.iterate_succ_apply', IH]
-- 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)
rw :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n] (p * q)) : R[X])
    ((derivative : (a : R[X]) → R[X])
        (∑ k ∈ range n.succ,
          n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)) :
      R[X])
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 1] (p * q) =
    (derivative : (a : R[X]) → R[X])
      (∑ 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 rw₁ : Eq.{u + 1} (α := R[X])
  ((derivative : (a : R[X]) → R[X])
    (∑ 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])
    (∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)))
Tactic: rw [Function.iterate_succ_apply', IH]
-- 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)
⊢ (derivative : (a : R[X]) → R[X])
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)) =
    HAdd.hAdd (α := R[X])
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k] q))
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q))
have simp_rw : ∑ b ∈ range n.succ,
    (derivative : (a : R[X]) → R[X])
      (n.choose b • ((⇑derivative : (a : R[X]) → R[X])^[n - b] p * (⇑derivative : (a : R[X]) → R[X])^[b] q)) =
  HAdd.hAdd (α := R[X])
    (∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k] q))
    (∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q))
Tactic: simp_rw [derivative_sum, derivative_smul, derivative_mul, Function.iterate_succ_apply',
          smul_add, sum_add_distrib]
-- 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)
simp_rw :
  ∑ b ∈ range n.succ,
      (derivative : (a : R[X]) → R[X])
        (n.choose b • ((⇑derivative : (a : R[X]) → R[X])^[n - b] p * (⇑derivative : (a : R[X]) → R[X])^[b] q)) =
    HAdd.hAdd (α := R[X])
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k] q))
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q))
⊢ (derivative : (a : R[X]) → R[X])
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k] q)) =
    HAdd.hAdd (α := R[X])
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k] q))
      (∑ k ∈ range n.succ,
        n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q))
have simp_rw₁ : ∑ x ∈ range n.succ,
    HSMul.hSMul (β := R[X]) (n.choose x)
      ((derivative : (a : R[X]) → R[X])
          ((⇑derivative : (a : R[X]) → R[X])^[n - x] p * (⇑derivative : (a : R[X]) → R[X])^[x] q) :
        R[X]) =
  HAdd.hAdd (α := R[X])
    (∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k + 1] p * (⇑derivative : (a : R[X]) → R[X])^[k] q))
    (∑ k ∈ range n.succ,
      n.choose k • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * (⇑derivative : (a : R[X]) → R[X])^[k + 1] q))
Tactic: simp_rw [derivative_sum, derivative_smul, derivative_mul, Function.iterate_succ_apply',
          smul_add, sum_add_distrib]