awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
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))
⊢ 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:
congr! 2 with k hk
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
k : ℕ
hk : k ∈ range n.succ
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))
⊢ (⇑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:
norm_cast
-- Module: Mathlib.Algebra.Polynomial.Derivative
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 * 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:
ring
-- Module: Mathlib.Algebra.Polynomial.Derivative
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))

Tactic:
have hsum : derivative^[n] (p * X ^ m) =
      ∑ k ∈ range n.succ,
        (n.choose k * m.descFactorial k) • (derivative^[n - k] p * X ^ (m - k)) := by
    simp_rw [iterate_derivative_mul, iterate_derivative_X_pow_eq_smul, mul_smul]
    congr! 2 with k hk
    norm_cast
    ring
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
    ∑ k ∈ range n.succ,
      (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
rw :
  Eq.{u + 1} (α := R[X])
    (∑ k ∈ range n.succ,
      (n.choose k * m.descFactorial k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)))
    (∑ k ∈ range (min m n).succ,
      (n.choose k * m.descFactorial k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)))
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
    ∑ k ∈ range (min m n).succ,
      (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))

Tactic:
rw [hsum]
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
    ∑ k ∈ range n.succ,
      (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
⊢ ∀ a ∈ range (min m n).succ,
    a ∉ range n.succ →
      (n.choose a * m.descFactorial a) •
          ((⇑derivative : (a : R[X]) → R[X])^[n - a] p * HPow.hPow (α := R[X]) X (m - a)) =
        0

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
    ∑ k ∈ range n.succ,
      (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
⊢ ∀ a ∈ range n.succ,
    a ∈ range (min m n).succ →
      (n.choose a * m.descFactorial a) •
          ((⇑derivative : (a : R[X]) → R[X])^[n - a] p * HPow.hPow (α := R[X]) X (m - a)) =
        (n.choose a * m.descFactorial a) •
          ((⇑derivative : (a : R[X]) → R[X])^[n - a] p * HPow.hPow (α := R[X]) X (m - a))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
    ∑ k ∈ range n.succ,
      (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
refine :
  ∀ (k : ℕ) (hk : k ∈ range n.succ) (hk' : k ∉ range (min m n).succ),
    (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)) =
      0
⊢ Eq.{u + 1} (α := R[X])
    (∑ k ∈ range n.succ,
      (n.choose k * m.descFactorial k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)))
    (∑ k ∈ range (min m n).succ,
      (n.choose k * m.descFactorial k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)))

Tactic:
refine sum_congr_of_eq_on_inter (fun k hk hk' ↦ ?_) (by simp_all) (by simp)

Premises used: Finset.sum_congr_of_eq_on_inter
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
    ∑ k ∈ range n.succ,
      (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
inl :
  ∀ (hkm : k ≤ m),
    (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)) =
      0
inr :
  ∀ (hkm : m < k),
    (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)) =
      0
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)) = 0

Tactic:
rcases le_or_gt k m with hkm | hkm

Premises used: le_or_gt
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
    ∑ k ∈ range n.succ,
      (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
hkm : k ≤ m
⊢ n < k

Tactic:
simpa [hkm] using hk'
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
    ∑ k ∈ range n.succ,
      (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
hkm : k ≤ m
⊢ n < k

Tactic:
replace hk' : n < k := by simpa [hkm] using hk'
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
    ∑ k ∈ range n.succ,
      (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
k : ℕ
hk : k ∈ range n.succ
hkm : k ≤ m
hk' : n < k
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)) = 0

Tactic:
simp [Nat.choose_eq_zero_of_lt hk']

Premises used: Nat.choose_eq_zero_of_lt
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
hsum :
  (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) X m) =
    ∑ k ∈ range n.succ,
      (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k))
k : ℕ
hk : k ∈ range n.succ
hk' : k ∉ range (min m n).succ
hkm : m < k
⊢ (n.choose k * m.descFactorial k) • ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (m - k)) = 0

Tactic:
simp [Nat.descFactorial_eq_zero_iff_lt.mpr hkm]

Premises used: Iff.mpr, Nat.descFactorial_eq_zero_iff_lt
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] (p * HPow.hPow (α := R[X]) (β := ℕ) X 1) =
    ∑ k ∈ range (min 1 n).succ,
      (n.choose k * Nat.descFactorial 1 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (1 - k))

Tactic:
p.iterate_derivative_mul_X_pow n 1

Premises used: Polynomial.iterate_derivative_mul_X_pow, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
h : X = HPow.hPow (α := R[X]) (β := ℕ) X 1
h₁ :
  (⇑derivative : (a : R[X]) → R[X])^[n] p * X + n • (⇑derivative : (a : R[X]) → R[X])^[n - 1] p =
    ∑ k ∈ range (min 1 n).succ,
      (n.choose k * Nat.descFactorial 1 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (1 - k))
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] (p * X) =
    (⇑derivative : (a : R[X]) → R[X])^[n] p * X + n • (⇑derivative : (a : R[X]) → R[X])^[n - 1] p

Tactic:
convert! p.iterate_derivative_mul_X_pow n 1

Premises used: Polynomial.iterate_derivative_mul_X_pow, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
⊢ X = HPow.hPow (α := R[X]) (β := ℕ) X 1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
h :
  (⇑derivative : (a : R[X]) → R[X])^[0] p * X +
      HSMul.hSMul (α := ℕ) 0 ((⇑derivative : (a : R[X]) → R[X])^[HSub.hSub (α := ℕ) 0 1] p) =
    ∑ k ∈ range (Nat.succ (min 1 0)),
      (Nat.choose 0 k * Nat.descFactorial 1 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[0 - k] p * HPow.hPow (α := R[X]) X (1 - k))
h₁ :
  ∀ (n : ℕ),
    (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X + (n + 1) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 - 1] p =
      ∑ k ∈ range (min 1 (n + 1)).succ,
        ((n + 1).choose k * Nat.descFactorial 1 k) •
          ((⇑derivative : (a : R[X]) → R[X])^[n + 1 - k] p * HPow.hPow (α := R[X]) X (1 - k))
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] p * X + n • (⇑derivative : (a : R[X]) → R[X])^[n - 1] p =
    ∑ k ∈ range (min 1 n).succ,
      (n.choose k * Nat.descFactorial 1 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - k] p * HPow.hPow (α := R[X]) X (1 - k))

Tactic:
rcases n with rfl | n

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[0] p * X +
      HSMul.hSMul (α := ℕ) 0 ((⇑derivative : (a : R[X]) → R[X])^[HSub.hSub (α := ℕ) 0 1] p) =
    ∑ k ∈ range (Nat.succ (min 1 0)),
      (Nat.choose 0 k * Nat.descFactorial 1 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[0 - k] p * HPow.hPow (α := R[X]) X (1 - k))

Tactic:
simp [sum_range_succ]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n : ℕ
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X + (n + 1) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 - 1] p =
    ∑ k ∈ range (min 1 (n + 1)).succ,
      ((n + 1).choose k * Nat.descFactorial 1 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n + 1 - k] p * HPow.hPow (α := R[X]) X (1 - k))

Tactic:
simp [sum_range_succ]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[n]
      (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 1)) =
    ∑ k ∈ range (min 1 n).succ,
      (n.choose k * Nat.descFactorial 1 k) •
        HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n - k] ((derivative : (a : R[X]) → R[X]) p) : R[X])
          (HPow.hPow (α := R[X]) X (1 - k))

Tactic:
(derivative p).iterate_derivative_mul_X_pow n 1

Premises used: Polynomial.derivative, Polynomial.iterate_derivative_mul_X_pow, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
h : X = HPow.hPow (α := R[X]) (β := ℕ) X 1
h₁ :
  (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X + n • (⇑derivative : (a : R[X]) → R[X])^[n] p =
    ∑ k ∈ range (min 1 n).succ,
      (n.choose k * Nat.descFactorial 1 k) •
        HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n - k] ((derivative : (a : R[X]) → R[X]) p) : R[X])
          (HPow.hPow (α := R[X]) X (1 - k))
⊢ (⇑derivative : (a : R[X]) → R[X])^[n]
      (HMul.hMul (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) X) =
    (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X + n • (⇑derivative : (a : R[X]) → R[X])^[n] p

Tactic:
convert! (derivative p).iterate_derivative_mul_X_pow n 1

Premises used: Polynomial.derivative, Polynomial.iterate_derivative_mul_X_pow, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
h :
  (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] p * X +
      HSMul.hSMul (α := ℕ) 0 ((⇑derivative : (a : R[X]) → R[X])^[0] p) =
    ∑ k ∈ range (Nat.succ (min 1 0)),
      (Nat.choose 0 k * Nat.descFactorial 1 k) •
        HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[0 - k] ((derivative : (a : R[X]) → R[X]) p) : R[X])
          (HPow.hPow (α := R[X]) X (1 - k))
h₁ :
  ∀ (n : ℕ),
    (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1] p * X + (n + 1) • (⇑derivative : (a : R[X]) → R[X])^[n + 1] p =
      ∑ k ∈ range (min 1 (n + 1)).succ,
        ((n + 1).choose k * Nat.descFactorial 1 k) •
          HMul.hMul (α := R[X])
            ((⇑derivative : (a : R[X]) → R[X])^[n + 1 - k] ((derivative : (a : R[X]) → R[X]) p) : R[X])
            (HPow.hPow (α := R[X]) X (1 - k))
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X + n • (⇑derivative : (a : R[X]) → R[X])^[n] p =
    ∑ k ∈ range (min 1 n).succ,
      (n.choose k * Nat.descFactorial 1 k) •
        HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[n - k] ((derivative : (a : R[X]) → R[X]) p) : R[X])
          (HPow.hPow (α := R[X]) X (1 - k))

Tactic:
rcases n with rfl | n

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] p * X +
      HSMul.hSMul (α := ℕ) 0 ((⇑derivative : (a : R[X]) → R[X])^[0] p) =
    ∑ k ∈ range (Nat.succ (min 1 0)),
      (Nat.choose 0 k * Nat.descFactorial 1 k) •
        HMul.hMul (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[0 - k] ((derivative : (a : R[X]) → R[X]) p) : R[X])
          (HPow.hPow (α := R[X]) X (1 - k))

Tactic:
simp [sum_range_succ]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n : ℕ
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1] p * X + (n + 1) • (⇑derivative : (a : R[X]) → R[X])^[n + 1] p =
    ∑ k ∈ range (min 1 (n + 1)).succ,
      ((n + 1).choose k * Nat.descFactorial 1 k) •
        HMul.hMul (α := R[X])
          ((⇑derivative : (a : R[X]) → R[X])^[n + 1 - k] ((derivative : (a : R[X]) → R[X]) p) : R[X])
          (HPow.hPow (α := R[X]) X (1 - k))

Tactic:
simp [sum_range_succ]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] ((⇑derivative : (a : R[X]) → R[X])^[2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2) =
    ∑ k ∈ range (min 2 n).succ,
      (n.choose k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))

Tactic:
(derivative^[2] p).iterate_derivative_mul_X_pow n 2

Premises used: Polynomial.derivative, Nat.iterate, Polynomial.iterate_derivative_mul_X_pow, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
h :
  (⇑derivative : (a : R[X]) → R[X])^[n + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * n) • (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X +
      (n * (n - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n] p =
    ∑ k ∈ range (min 2 n).succ,
      (n.choose k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] ((⇑derivative : (a : R[X]) → R[X])^[2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2) =
    (⇑derivative : (a : R[X]) → R[X])^[n + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * n) • (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X +
      (n * (n - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n] p

Tactic:
convert! (derivative^[2] p).iterate_derivative_mul_X_pow n 2

Premises used: Polynomial.derivative, Nat.iterate, Polynomial.iterate_derivative_mul_X_pow, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : R[X]
h :
  (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        HMul.hMul (α := ℕ) 2 0 • (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] p * X +
      (0 * HSub.hSub (α := ℕ) 0 1) • (⇑derivative : (a : R[X]) → R[X])^[0] p =
    ∑ k ∈ range (Nat.succ (min 2 0)),
      (Nat.choose 0 k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[0 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))
h₁ :
  ∀ (n : ℕ),
    (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          (2 * (n + 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1] p * X +
        ((n + 1) * (n + 1 - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1] p =
      ∑ k ∈ range (min 2 (n + 1)).succ,
        ((n + 1).choose k * Nat.descFactorial 2 k) •
          ((⇑derivative : (a : R[X]) → R[X])^[n + 1 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
            HPow.hPow (α := R[X]) X (2 - k))
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * n) • (⇑derivative : (a : R[X]) → R[X])^[n + 1] p * X +
      (n * (n - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n] p =
    ∑ k ∈ range (min 2 n).succ,
      (n.choose k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))

Tactic:
rcases n with rfl | n

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        HMul.hMul (α := ℕ) 2 0 • (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] p * X +
      (0 * HSub.hSub (α := ℕ) 0 1) • (⇑derivative : (a : R[X]) → R[X])^[0] p =
    ∑ k ∈ range (Nat.succ (min 2 0)),
      (Nat.choose 0 k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[0 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n : ℕ
h :
  (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1 + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * HAdd.hAdd (α := ℕ) 0 1) • (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1 + 1] p * X +
      (HAdd.hAdd (α := ℕ) 0 1 * (HAdd.hAdd (α := ℕ) 0 1 - 1)) •
        (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] p =
    ∑ k ∈ range (min 2 (HAdd.hAdd (α := ℕ) 0 1)).succ,
      ((HAdd.hAdd (α := ℕ) 0 1).choose k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))
h₁ :
  ∀ (n : ℕ),
    (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          (2 * (n + 1 + 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 + 1] p * X +
        ((n + 1 + 1) * (n + 1 + 1 - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1] p =
      ∑ k ∈ range (min 2 (n + 1 + 1)).succ,
        ((n + 1 + 1).choose k * Nat.descFactorial 2 k) •
          ((⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
            HPow.hPow (α := R[X]) X (2 - k))
⊢ (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * (n + 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1 + 1] p * X +
      ((n + 1) * (n + 1 - 1)) • (⇑derivative : (a : R[X]) → R[X])^[n + 1] p =
    ∑ k ∈ range (min 2 (n + 1)).succ,
      ((n + 1).choose k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[n + 1 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))

Tactic:
rcases n with rfl | n

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1 + 2] p * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        (2 * HAdd.hAdd (α := ℕ) 0 1) • (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1 + 1] p * X +
      (HAdd.hAdd (α := ℕ) 0 1 * (HAdd.hAdd (α := ℕ) 0 1 - 1)) •
        (⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] p =
    ∑ k ∈ range (min 2 (HAdd.hAdd (α := ℕ) 0 1)).succ,
      ((HAdd.hAdd (α := ℕ) 0 1).choose k * Nat.descFactorial 2 k) •
        ((⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1 - k] ((⇑derivative : (a : R[X]) → R[X])^[2] p) *
          HPow.hPow (α := R[X]) X (2 - k))

Tactic:
simp [sum_range_succ, ← mul_assoc]

Premises used: mul_assoc, Finset.sum_range_succ