awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n_1 n : ℕ
ih :
  (derivative : (a : R[X]) → R[X]) (p ^ (n + 1)) =
    HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n : R) 1) : R[X]) (p ^ n))
      ((derivative : (a : R[X]) → R[X]) p : R[X])
rw :
  HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑n : R) * p ^ n * p + p ^ n * p)
        ((derivative : (a : R[X]) → R[X]) p : R[X]) +
      HMul.hMul (β := R[X]) (p ^ n * p) ((derivative : (a : R[X]) → R[X]) p : R[X]) =
    HMul.hMul (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n.succ : R) 1) : R[X]) (p ^ n) * p)
      ((derivative : (a : R[X]) → R[X]) p : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (p ^ (n.succ + 1)) =
    HMul.hMul (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n.succ : R) 1) : R[X]) (p ^ n.succ))
      ((derivative : (a : R[X]) → R[X]) p : R[X])

Tactic:
rw [pow_succ, derivative_mul, ih, Nat.add_one, mul_right_comm, C_add,
      add_mul, add_mul, pow_succ, ← mul_assoc, C_1, one_mul]

Premises used: add_mul, Polynomial.derivative_mul, Polynomial.C_1, pow_succ, mul_assoc, mul_right_comm, Nat.add_one, Polynomial.C_add, one_mul
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n_1 n : ℕ
ih :
  (derivative : (a : R[X]) → R[X]) (p ^ (n + 1)) =
    HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n : R) 1) : R[X]) (p ^ n))
      ((derivative : (a : R[X]) → R[X]) p : R[X])
⊢ HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑n : R) * p ^ n * p + p ^ n * p)
        ((derivative : (a : R[X]) → R[X]) p : R[X]) +
      HMul.hMul (β := R[X]) (p ^ n * p) ((derivative : (a : R[X]) → R[X]) p : R[X]) =
    HMul.hMul (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n.succ : R) 1) : R[X]) (p ^ n) * p)
      ((derivative : (a : R[X]) → R[X]) p : R[X])

Tactic:
simp [add_mul]

Premises used: add_mul
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n : ℕ
⊢ (derivative : (a : R[X]) → R[X]) (p ^ Nat.zero) =
    HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑Nat.zero : R) * p ^ (Nat.zero - 1))
      ((derivative : (a : R[X]) → R[X]) p : R[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n_1 n : ℕ
rw :
  HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n : R) 1) : R[X]) (p ^ n))
      ((derivative : (a : R[X]) → R[X]) p : R[X]) =
    HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑n.succ : R) * p ^ (n.succ - 1))
      ((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) (↑n : R) 1) : R[X]) (p ^ n))
      ((derivative : (a : R[X]) → R[X]) p : R[X]) =
    HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑n.succ : R) * p ^ n) ((derivative : (a : R[X]) → R[X]) p : R[X])
rw₂ rw₃ :
  HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n : R) 1) : R[X]) (p ^ n))
      ((derivative : (a : R[X]) → R[X]) p : R[X]) =
    HMul.hMul (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n : R) 1) : R[X]) (p ^ n))
      ((derivative : (a : R[X]) → R[X]) p : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (p ^ n.succ) =
    HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑n.succ : R) * p ^ (n.succ - 1))
      ((derivative : (a : R[X]) → R[X]) p : R[X])

Tactic:
rw [p.derivative_pow_succ n, Nat.add_one_sub_one, n.cast_succ]

Premises used: Nat.cast_succ, Nat.add_one_sub_one, Polynomial.derivative_pow_succ
-- Module: Mathlib.Algebra.Polynomial.Derivative
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])
rw₃ 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])
⊢ (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])

Tactic:
rw [derivative_pow_succ, Nat.cast_one, one_add_one_eq_two, pow_one]

Premises used: Polynomial.derivative_pow_succ, one_add_one_eq_two, pow_one, Nat.cast_one
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
n : ℕ
dvd : q ^ n ∣ p
obtain : ∀ (r : R[X]), q ^ (n - 1) ∣ (derivative : (a : R[X]) → R[X]) (q ^ n * r)
⊢ q ^ (n - 1) ∣ (derivative : (a : R[X]) → R[X]) p

Tactic:
obtain ⟨r, rfl⟩ := dvd

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
q : R[X]
n : ℕ
r : R[X]
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])
⊢ q ^ (n - 1) ∣ (derivative : (a : R[X]) → R[X]) (q ^ n * r)

Tactic:
rw [derivative_mul, derivative_pow]

Premises used: Polynomial.derivative_mul, Polynomial.derivative_pow
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
q : R[X]
n : ℕ
r : R[X]
⊢ 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:
(((dvd_mul_left _ _).mul_right _).mul_right _).add ((pow_dvd_pow q n.pred_le).mul_right _)

Premises used: Dvd.dvd.mul_right, pow_dvd_pow, Dvd.dvd.add, dvd_mul_left, Nat.pred_le
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
q : R[X]
n : ℕ
r : R[X]
⊢ 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:
exact (((dvd_mul_left _ _).mul_right _).mul_right _).add ((pow_dvd_pow q n.pred_le).mul_right _)

Premises used: Dvd.dvd.mul_right, pow_dvd_pow, Dvd.dvd.add, dvd_mul_left, Nat.pred_le
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
q : R[X]
n : ℕ
p : R[X]
dvd : q ^ n ∣ p
⊢ q ^ (n - 0) ∣ (⇑derivative : (a : R[X]) → R[X])^[0] p

Tactic:
simpa
-- Module: Mathlib.Algebra.Polynomial.Derivative
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
succ : q ^ (n - m).pred ∣ ((⇑derivative : (a : R[X]) → R[X]) ∘ (⇑derivative : (a : R[X]) → R[X])^[m]) p
⊢ q ^ (n - (m + 1)) ∣ (⇑derivative : (a : R[X]) → R[X])^[m + 1] p

Tactic:
rw [Nat.sub_succ, Function.iterate_succ']

Premises used: Function.iterate_succ', Nat.sub_succ
-- Module: Mathlib.Algebra.Polynomial.Derivative
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).pred ∣ ((⇑derivative : (a : R[X]) → R[X]) ∘ (⇑derivative : (a : R[X]) → R[X])^[m]) p

Tactic:
pow_sub_one_dvd_derivative_of_pow_dvd (ih dvd)

Premises used: Polynomial.pow_sub_one_dvd_derivative_of_pow_dvd, Nat.pred
-- Module: Mathlib.Algebra.Polynomial.Derivative
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).pred ∣ ((⇑derivative : (a : R[X]) → R[X]) ∘ (⇑derivative : (a : R[X]) → R[X])^[m]) p

Tactic:
exact pow_sub_one_dvd_derivative_of_pow_dvd (ih dvd)

Premises used: Polynomial.pow_sub_one_dvd_derivative_of_pow_dvd
-- Module: Mathlib.Algebra.Polynomial.Derivative
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
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
⊢ q ^ (n - m) ∣ (⇑derivative : (a : R[X]) → R[X])^[m] 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)

Premises used: Function.iterate_succ', Nat.sub_succ
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n m : ℕ
⊢ p ^ (n - m) ∣ (⇑derivative : (a : R[X]) → R[X])^[m] (p ^ n)

Tactic:
pow_sub_dvd_iterate_derivative_of_pow_dvd m dvd_rfl

Premises used: Polynomial.pow_sub_dvd_iterate_derivative_of_pow_dvd, dvd_rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n m : ℕ
c : R
hm : m ≠ 0
obtain : ∀ (m : ℕ) (hm : m.succ ≠ 0), (↑n : R) ∣ eval c ((⇑derivative : (a : R[X]) → R[X])^[m.succ] (f ^ n))
⊢ (↑n : R) ∣ eval c ((⇑derivative : (a : R[X]) → R[X])^[m] (f ^ n))

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hm

Premises used: Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
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])))
⊢ (↑n : R) ∣ eval c ((⇑derivative : (a : R[X]) → R[X])^[m.succ] (f ^ n))

Tactic:
rw [Function.iterate_succ_apply, derivative_pow, mul_assoc, C_eq_natCast,
    iterate_derivative_natCast_mul, eval_mul, eval_natCast]

Premises used: Polynomial.C_eq_natCast, mul_assoc, Polynomial.eval_natCast, Polynomial.iterate_derivative_natCast_mul, Polynomial.eval_mul, Polynomial.derivative_pow, Function.iterate_succ_apply
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ (↑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:
dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n : ℕ
c : R
m : ℕ
hm : m.succ ≠ 0
⊢ (↑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:
exact dvd_mul_right _ _

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.Polynomial.Derivative
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
zero₄ zero₅ : HPow.hPow (α := R[X]) X n = 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)

Tactic:
rw [Function.iterate_zero_apply, tsub_zero, Nat.descFactorial_zero, Nat.cast_one, one_mul]

Premises used: tsub_zero, Nat.descFactorial_zero, Function.iterate_zero_apply, Nat.cast_one, one_mul
-- Module: Mathlib.Algebra.Polynomial.Derivative
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)
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))
⊢ (⇑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:
rw [Function.iterate_succ_apply', ih, derivative_natCast_mul, derivative_X_pow, C_eq_natCast,
      Nat.descFactorial_succ, Nat.sub_sub, Nat.cast_mul]

Premises used: Function.iterate_succ_apply', Polynomial.C_eq_natCast, Polynomial.derivative_natCast_mul, Nat.sub_sub, Nat.descFactorial_succ, Nat.cast_mul, Polynomial.derivative_X_pow
-- Module: Mathlib.Algebra.Polynomial.Derivative
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)
⊢ (↑(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:
simp [mul_assoc, mul_left_comm]

Premises used: mul_assoc, mul_left_comm
-- Module: Mathlib.Algebra.Polynomial.Derivative
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)
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))
⊢ (⇑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)

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]

Premises used: Function.iterate_succ_apply', Polynomial.C_eq_natCast, mul_assoc, Polynomial.derivative_natCast_mul, Nat.sub_sub, mul_left_comm, Nat.descFactorial_succ, tsub_zero, Nat.cast_mul, Polynomial.derivative_X_pow, Nat.descFactorial_zero, Function.iterate_zero_apply, Nat.cast_one, one_mul
-- Module: Mathlib.Algebra.Polynomial.Derivative
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)
rw₁ 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)
⊢ (⇑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)

Tactic:
rw [iterate_derivative_X_pow_eq_natCast_mul n k, C_eq_natCast]

Premises used: Polynomial.C_eq_natCast, Polynomial.iterate_derivative_X_pow_eq_natCast_mul
-- Module: Mathlib.Algebra.Polynomial.Derivative
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))
rw₁ 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)
⊢ (⇑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))

Tactic:
rw [iterate_derivative_X_pow_eq_C_mul n k, smul_eq_C_mul]

Premises used: Polynomial.smul_eq_C_mul, Polynomial.iterate_derivative_X_pow_eq_C_mul
-- Module: Mathlib.Algebra.Polynomial.Derivative
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)
rw₂ 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)
⊢ (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)

Tactic:
rw [derivative_pow, derivative_X_add_C, mul_one]

Premises used: Polynomial.derivative_X_add_C, Polynomial.derivative_pow, mul_one
-- Module: Mathlib.Algebra.Polynomial.Derivative
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])
rw₂ 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])
⊢ (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])

Tactic:
rw [derivative_sq, derivative_X_add_C, mul_one]

Premises used: Polynomial.derivative_X_add_C, Polynomial.derivative_sq, mul_one
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
c : R
⊢ (⇑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:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
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)
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)
⊢ (⇑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:
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]

Premises used: Function.iterate_succ_apply', Polynomial.derivative_smul, Nat.sub_succ', Nat.descFactorial_succ, Nat.cast_mul, map_natCast, nsmul_eq_mul, Polynomial.derivative_X_add_C_pow
-- Module: Mathlib.Algebra.Polynomial.Derivative
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)
⊢ (↑(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:
ring
-- Module: Mathlib.Algebra.Polynomial.Derivative
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)
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))
⊢ (⇑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)

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

Premises used: Function.iterate_succ_apply', Polynomial.derivative_smul, Nat.sub_succ', Nat.descFactorial_succ, Nat.cast_mul, map_natCast, nsmul_eq_mul, Polynomial.derivative_X_add_C_pow
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
n m : ℕ
p : R[X]
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)))
⊢ (⇑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:
simp_rw [iterate_derivative_mul, iterate_derivative_X_pow_eq_smul, mul_smul]

Premises used: Polynomial.iterate_derivative_X_pow_eq_smul, Polynomial.iterate_derivative_mul, SemigroupAction.mul_smul