awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n_1 : ℕ := max p.natDegree (map f p).natDegree
n : ℕ
⊢ HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (HMul.hMul (α := S) 0 (↑n : S)) : S[X])
      (HPow.hPow (α := S[X]) X (n - 1)) =
    0
have rw : (C : (a : S) → S[X]) 0 * HPow.hPow (α := S[X]) X (n - 1) = 0
Tactic: rw [zero_mul, C_0, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n_1 : ℕ := max p.natDegree (map f p).natDegree
n : ℕ
rw : (C : (a : S) → S[X]) 0 * HPow.hPow (α := S[X]) X (n - 1) = 0
⊢ HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (HMul.hMul (α := S) 0 (↑n : S)) : S[X])
      (HPow.hPow (α := S[X]) X (n - 1)) =
    0
have rw₁ : 0 * HPow.hPow (α := S[X]) X (n - 1) = 0
Tactic: rw [zero_mul, C_0, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n_1 : ℕ := max p.natDegree (map f p).natDegree
n : ℕ
rw : (C : (a : S) → S[X]) 0 * HPow.hPow (α := S[X]) X (n - 1) = 0
rw₁ : 0 * HPow.hPow (α := S[X]) X (n - 1) = 0
⊢ HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (HMul.hMul (α := S) 0 (↑n : S)) : S[X])
      (HPow.hPow (α := S[X]) X (n - 1)) =
    0
have rw₂ : Eq.{v + 1} (α := S[X]) 0 0
Tactic: rw [zero_mul, C_0, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n_1 : ℕ := max p.natDegree (map f p).natDegree
n : ℕ
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HMul.hMul (α := R) 0 (↑n : R)) : R[X])
      (HPow.hPow (α := R[X]) X (n - 1)) =
    0
have rw : (C : (a : R) → R[X]) 0 * HPow.hPow (α := R[X]) X (n - 1) = 0
Tactic: rw [zero_mul, C_0, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n_1 : ℕ := max p.natDegree (map f p).natDegree
n : ℕ
rw : (C : (a : R) → R[X]) 0 * HPow.hPow (α := R[X]) X (n - 1) = 0
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HMul.hMul (α := R) 0 (↑n : R)) : R[X])
      (HPow.hPow (α := R[X]) X (n - 1)) =
    0
have rw₁ : 0 * HPow.hPow (α := R[X]) X (n - 1) = 0
Tactic: rw [zero_mul, C_0, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n_1 : ℕ := max p.natDegree (map f p).natDegree
n : ℕ
rw : (C : (a : R) → R[X]) 0 * HPow.hPow (α := R[X]) X (n - 1) = 0
rw₁ : 0 * HPow.hPow (α := R[X]) X (n - 1) = 0
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HMul.hMul (α := R) 0 (↑n : R)) : R[X])
      (HPow.hPow (α := R[X]) X (n - 1)) =
    0
have rw₂ : Eq.{u + 1} (α := R[X]) 0 0
Tactic: rw [zero_mul, C_0, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
k : ℕ
⊢ (⇑derivative : (a : S[X]) → S[X])^[k] (map f p) = map f ((⇑derivative : (a : R[X]) → R[X])^[k] p)
have zero : ∀ (p : R[X]), (⇑derivative : (a : S[X]) → S[X])^[0] (map f p) = map f ((⇑derivative : (a : R[X]) → R[X])^[0] p)
Tactic: induction k generalizing p with
  | zero => simp
  | succ k ih =>
    simp only [ih, Function.iterate_succ, Polynomial.derivative_map, Function.comp_apply]
Cleared hypotheses: p, k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
k : ℕ
zero : ∀ (p : R[X]), (⇑derivative : (a : S[X]) → S[X])^[0] (map f p) = map f ((⇑derivative : (a : R[X]) → R[X])^[0] p)
⊢ (⇑derivative : (a : S[X]) → S[X])^[k] (map f p) = map f ((⇑derivative : (a : R[X]) → R[X])^[k] p)
have succ : ∀ (k : ℕ)
  (ih : ∀ (p : R[X]), (⇑derivative : (a : S[X]) → S[X])^[k] (map f p) = map f ((⇑derivative : (a : R[X]) → R[X])^[k] p))
  (p : R[X]), (⇑derivative : (a : S[X]) → S[X])^[k + 1] (map f p) = map f ((⇑derivative : (a : R[X]) → R[X])^[k + 1] p)
Tactic: induction k generalizing p with
  | zero => simp
  | succ k ih =>
    simp only [ih, Function.iterate_succ, Polynomial.derivative_map, Function.comp_apply]
Cleared hypotheses: p, k
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
n k : ℕ
f : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] ((↑n : R[X]) * f) = (↑n : R[X]) * (⇑derivative : (a : R[X]) → R[X])^[k] f
have zero : ∀ {f : R[X]},
  (⇑derivative : (a : R[X]) → R[X])^[0] ((↑n : R[X]) * f) = (↑n : R[X]) * (⇑derivative : (a : R[X]) → R[X])^[0] f
Tactic: induction k generalizing f
Cleared hypotheses: k, f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
n k : ℕ
f : R[X]
zero :
  ∀ {f : R[X]},
    (⇑derivative : (a : R[X]) → R[X])^[0] ((↑n : R[X]) * f) = (↑n : R[X]) * (⇑derivative : (a : R[X]) → R[X])^[0] f
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] ((↑n : R[X]) * f) = (↑n : R[X]) * (⇑derivative : (a : R[X]) → R[X])^[k] f
have succ : ∀ (n_1 : ℕ),
  (∀ {f : R[X]},
      (⇑derivative : (a : R[X]) → R[X])^[n_1] ((↑n : R[X]) * f) =
        (↑n : R[X]) * (⇑derivative : (a : R[X]) → R[X])^[n_1] f) →
    ∀ {f : R[X]},
      (⇑derivative : (a : R[X]) → R[X])^[n_1 + 1] ((↑n : R[X]) * f) =
        (↑n : R[X]) * (⇑derivative : (a : R[X]) → R[X])^[n_1 + 1] f
Tactic: induction k generalizing f
Cleared hypotheses: k, f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
n : ℕ
⊢ n ∈ support.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ↔ n + 1 ∈ p.support
have suffices : ¬p.coeff (n + 1) * (↑(n + 1) : R) = 0 ↔ p.coeff (n + 1) ≠ 0
Tactic: suffices ¬p.coeff (n + 1) * (n + 1 : ℕ) = 0 ↔ coeff p (n + 1) ≠ 0 by
    simpa only [mem_support_iff, coeff_derivative, Ne, Nat.cast_succ]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
n : ℕ
⊢ ¬p.coeff (n + 1) * (↑(n + 1) : R) = 0 ↔ p.coeff (n + 1) ≠ 0
have rw : ¬(n + 1 = 0 ∨ p.coeff (n + 1) = 0) ↔ p.coeff (n + 1) ≠ 0
Tactic: rw [← nsmul_eq_mul', smul_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
⊢ degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) = (↑(p.natDegree - 1) : WithBot ℕ)
have a : degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ≤ (↑(p.natDegree - 1) : WithBot ℕ)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
a : degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ≤ (↑(p.natDegree - 1) : WithBot ℕ)
⊢ degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) = (↑(p.natDegree - 1) : WithBot ℕ)
have a₁ : (↑(p.natDegree - 1) : WithBot ℕ) ≤ degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
⊢ degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ≤ (↑(p.natDegree - 1) : WithBot ℕ)
have a : degree (R := R)
    (p.sum fun (n : ℕ) (a : R) ↦
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) ≤
  (↑(p.natDegree - 1) : WithBot ℕ)
Tactic: rw [derivative_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
⊢ degree (R := R)
      (p.sum fun (n : ℕ) (a : R) ↦
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))) ≤
    (↑(p.natDegree - 1) : WithBot ℕ)
have apply : ∀ b ∈ p.support,
  degree.{u} (R := R)
      ((fun (n : ℕ) (a : R) ↦
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
        b (p.coeff b)) ≤
    (↑(p.natDegree - 1) : WithBot ℕ)
Tactic: apply le_trans (degree_sum_le _ _) (Finset.sup_le _)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
n : ℕ
hn : n ∈ p.support
⊢ degree.{u} (R := R)
      ((fun (n : ℕ) (a : R) ↦
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1)))
        n (p.coeff n)) ≤
    (↑(p.natDegree - 1) : WithBot ℕ)
have apply : n ≤ p.natDegree
Tactic: apply le_trans (degree_C_mul_X_pow_le _ _) (WithBot.coe_le_coe.2 (tsub_le_tsub_right _ _))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
⊢ (↑(p.natDegree - 1) : WithBot ℕ) ≤ degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p)
have a : p.natDegree - 1 ∈ support.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p)
Tactic: refine le_sup ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
⊢ p.natDegree - 1 ∈ support.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p)
have a : p.coeff p.natDegree ≠ 0
Tactic: rw [mem_support_derivative, tsub_add_cancel_of_le, mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
a : p.coeff p.natDegree ≠ 0
⊢ p.natDegree - 1 ∈ support.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p)
have a₁ : 1 ≤ p.natDegree
Tactic: rw [mem_support_derivative, tsub_add_cancel_of_le, mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
⊢ p.coeff p.natDegree ≠ 0
have a : ¬p = 0
Tactic: rw [coeff_natDegree, Ne, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Derivative (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
h : p = 0
⊢ False
have hp₁ : LT.lt (α := ℕ) 0 0
Tactic: rw [h, natDegree_zero] at hp
Cleared hypotheses: hp, h
-- 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
have rw : coeff ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] p)) m =
  (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1
Tactic: rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.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 : ℕ
rw :
  coeff ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] p)) m =
    (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1
⊢ ((⇑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
have rw₁ : ((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff (m + 1) * HAdd.hAdd (α := R) (↑m : R) 1 =
  (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1
Tactic: rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.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 : ℕ
rw :
  coeff ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] p)) m =
    (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1
rw₁ :
  ((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff (m + 1) * HAdd.hAdd (α := R) (↑m : R) 1 =
    (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1
⊢ ((⇑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
have rw₂ : (m.succ + k).descFactorial k • p.coeff (m.succ + k) * HAdd.hAdd (α := R) (↑m : R) 1 =
  (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1
Tactic: rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.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 : ℕ
rw :
  coeff ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] p)) m =
    (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1
rw₁ :
  ((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff (m + 1) * HAdd.hAdd (α := R) (↑m : R) 1 =
    (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1
rw₂ :
  (m.succ + k).descFactorial k • p.coeff (m.succ + k) * HAdd.hAdd (α := R) (↑m : R) 1 =
    (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1
⊢ ((⇑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
have rw₃ : (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
Tactic: rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.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 : ℕ
rw :
  coeff ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] p)) m =
    (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1
rw₁ :
  ((⇑derivative : (a : R[X]) → R[X])^[k] p).coeff (m + 1) * HAdd.hAdd (α := R) (↑m : R) 1 =
    (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1
rw₂ :
  (m.succ + k).descFactorial k • p.coeff (m.succ + k) * HAdd.hAdd (α := R) (↑m : R) 1 =
    (m + k).succ.descFactorial k • p.coeff (m + k.succ) * HAdd.hAdd (α := R) (↑m : R) 1
rw₃ :
  (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
⊢ ((⇑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
have rw₄ : (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
Tactic: rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.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 : ℕ
⊢ (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)
have rw : (m + k).succ.descFactorial k • p.coeff (m + k.succ) * (↑(m + 1) : R) =
  ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ)
Tactic: rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul]
-- 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 : ℕ
rw :
  (m + k).succ.descFactorial k • p.coeff (m + k.succ) * (↑(m + 1) : R) =
    ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ)
⊢ (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)
have rw₁ : (m + 1) • (m + k).succ.descFactorial k • p.coeff (m + k.succ) =
  ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ)
Tactic: rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul]
-- 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 : ℕ
rw :
  (m + k).succ.descFactorial k • p.coeff (m + k.succ) * (↑(m + 1) : R) =
    ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ)
rw₁ :
  (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 + 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)
have rw₂ : ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ) =
  ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ)
Tactic: rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul]
-- 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 : ℕ
⊢ ((m + 1) * (m + k).succ.descFactorial k) • p.coeff (m + k.succ) =
    (m.succ + k).descFactorial k.succ • p.coeff (m + k.succ)
have rw : ((m + 1) * (m.succ + k).descFactorial k) • p.coeff (m + k.succ) =
  (m.succ + k).descFactorial k.succ • p.coeff (m + k.succ)
Tactic: rw [← Nat.succ_add, Nat.descFactorial_succ, add_tsub_cancel_right]
-- 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 : ℕ
rw :
  ((m + 1) * (m.succ + k).descFactorial k) • p.coeff (m + k.succ) =
    (m.succ + k).descFactorial k.succ • 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)
have rw₁ : ((m + 1) * (m.succ + k).descFactorial k) • p.coeff (m + k.succ) =
  ((m.succ + k - k) * (m.succ + k).descFactorial k) • p.coeff (m + k.succ)
Tactic: rw [← Nat.succ_add, Nat.descFactorial_succ, add_tsub_cancel_right]
-- 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 : ℕ
rw :
  ((m + 1) * (m.succ + k).descFactorial k) • p.coeff (m + k.succ) =
    (m.succ + k).descFactorial k.succ • p.coeff (m + k.succ)
rw₁ :
  ((m + 1) * (m.succ + k).descFactorial k) • p.coeff (m + k.succ) =
    ((m.succ + k - k) * (m.succ + k).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)
have rw₂ : ((m + 1) * (m.succ + k).descFactorial k) • p.coeff (m + k.succ) =
  (m.succ * (m.succ + k).descFactorial k) • p.coeff (m + k.succ)
Tactic: rw [← Nat.succ_add, Nat.descFactorial_succ, add_tsub_cancel_right]
-- 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 : ℕ
⊢ (m.succ + k).descFactorial k.succ • p.coeff (m + k.succ) = (m + k.succ).descFactorial k.succ • p.coeff (m + k.succ)
have rw : (m + k.succ).descFactorial k.succ • p.coeff (m + k.succ) = (m + k.succ).descFactorial k.succ • p.coeff (m + k.succ)
Tactic: 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 + 1)).descFactorial (k + 1) • p.coeff (m + (k + 1))
have _ : ((⇑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
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
⊢ ((⇑derivative : (a : R[X]) → R[X])^[k + 1] p).coeff m = (m + (k + 1)).descFactorial (k + 1) • p.coeff (m + (k + 1))
have _₁ : (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)
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]