awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
b : R
m : ℕ
monomial :
  HAdd.hAdd (α := R[X]) (β := R[X])
      ((Polynomial.monomial (m + 1 + 0 - 1) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
      ((Polynomial.monomial (m + 1 + 0 - 1) : (a : R) → R[X]) (a * (b * (↑0 : R))) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X])
      ((Polynomial.monomial (m + 1 - 1 + 0) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
      ((Polynomial.monomial (m + 1 + HSub.hSub (α := ℕ) 0 1) : (a : R) → R[X]) (a * (b * (↑0 : R))) : R[X])
monomial₁ :
  ∀ (n : ℕ),
    HAdd.hAdd (α := R[X]) (β := R[X])
        ((Polynomial.monomial (m + 1 + (n + 1) - 1) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
        ((Polynomial.monomial (m + 1 + (n + 1) - 1) : (a : R) → R[X]) (a * (b * (↑(n + 1) : R))) : R[X]) =
      HAdd.hAdd (α := R[X]) (β := R[X])
        ((Polynomial.monomial (m + 1 - 1 + (n + 1)) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
        ((Polynomial.monomial (m + 1 + (n + 1 - 1)) : (a : R) → R[X]) (a * (b * (↑(n + 1) : R))) : R[X])
⊢ HAdd.hAdd (α := R[X]) (β := R[X])
      ((Polynomial.monomial (m + 1 + n - 1) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
      ((Polynomial.monomial (m + 1 + n - 1) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X])
      ((Polynomial.monomial (m + 1 - 1 + n) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
      ((Polynomial.monomial (m + 1 + (n - 1)) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X])

Tactic:
cases n with
  | zero => simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]
  | succ n => grind

Premises used: map_zero, MulZeroClass.mul_zero, Nat.cast_zero, add_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
m : ℕ
a : R
n : ℕ
b : R
monomial :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((Polynomial.monomial (0 + n - 1) : (a : R) → R[X]) (a * (b * (↑0 : R))) : R[X])
      ((Polynomial.monomial (0 + n - 1) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X])
      ((Polynomial.monomial (HSub.hSub (α := ℕ) 0 1 + n) : (a : R) → R[X]) (a * (b * (↑0 : R))) : R[X])
      ((Polynomial.monomial (0 + (n - 1)) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X])
monomial₁ :
  ∀ (m : ℕ),
    HAdd.hAdd (α := R[X]) (β := R[X])
        ((Polynomial.monomial (m + 1 + n - 1) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
        ((Polynomial.monomial (m + 1 + n - 1) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X]) =
      HAdd.hAdd (α := R[X]) (β := R[X])
        ((Polynomial.monomial (m + 1 - 1 + n) : (a : R) → R[X]) (a * (b * (↑(m + 1) : R))) : R[X])
        ((Polynomial.monomial (m + 1 + (n - 1)) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X])
⊢ HAdd.hAdd (α := R[X]) (β := R[X]) ((Polynomial.monomial (m + n - 1) : (a : R) → R[X]) (a * (b * (↑m : R))) : R[X])
      ((Polynomial.monomial (m + n - 1) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((Polynomial.monomial (m - 1 + n) : (a : R) → R[X]) (a * (b * (↑m : R))) : R[X])
      ((Polynomial.monomial (m + (n - 1)) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X])

Tactic:
cases m with
  | zero => simp only [zero_add, Nat.cast_zero, mul_zero, map_zero]
  | succ m =>
  cases n with
  | zero => simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]
  | succ n => grind

Premises used: map_zero, zero_add, MulZeroClass.mul_zero, Nat.cast_zero, add_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
simp_rw :
  eval x
      (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.sum fun (n : ℕ) (a : R) ↦ a * (↑n : R) * x ^ (n - 1)
simp_rw₁ :
  Eq (α := R)
    (p.sum fun (n : ℕ) (a : R) ↦
      eval x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))))
    (p.sum fun (n : ℕ) (a : R) ↦ a * (↑n : R) * x ^ (n - 1))
simp_rw₂ :
  Eq (α := R) (p.sum fun (n : ℕ) (a : R) ↦ eval x ((C : (a : R) → R[X]) (a * (↑n : R))) * x ^ (n - 1))
    (p.sum fun (n : ℕ) (a : R) ↦ a * (↑n : R) * x ^ (n - 1))
⊢ eval x ((derivative : (a : R[X]) → R[X]) p) = p.sum fun (n : ℕ) (a : R) ↦ a * (↑n : R) * x ^ (n - 1)

Tactic:
simp_rw [derivative_apply, eval_sum, eval_mul_X_pow, eval_C]

Premises used: Polynomial.eval_C, Polynomial.eval_mul_X_pow, Polynomial.eval_sum, Polynomial.derivative_apply
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
rw :
  ((map f p).sum fun (n : ℕ) (a : S) ↦
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (a * (↑n : S)) : S[X]) (HPow.hPow (α := S[X]) X (n - 1))) =
    map f
      (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)))
⊢ (derivative : (a : S[X]) → S[X]) (map f p) = map f ((derivative : (a : R[X]) → R[X]) p)

Tactic:
rw [derivative_apply, derivative_apply]

Premises used: Polynomial.derivative_apply
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
rw :
  ((map f p).sum fun (n : ℕ) (a : S) ↦
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (a * (↑n : S)) : S[X]) (HPow.hPow (α := S[X]) X (n - 1))) =
    map f
      (∑ a ∈ range (n + 1),
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff a * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)))
rw₁ :
  ∀ (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
⊢ ((map f p).sum fun (n : ℕ) (a : S) ↦
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (a * (↑n : S)) : S[X]) (HPow.hPow (α := S[X]) X (n - 1))) =
    map f
      (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)))

Tactic:
rw [sum_over_range' _ _ (n + 1) ((le_max_left _ _).trans_lt (lt_add_one _))]

Premises used: lt_add_one, HAdd.hAdd, Polynomial.sum_over_range', OfNat.ofNat, le_max_left, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
rw :
  ∑ a ∈ range (n + 1),
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((map f p).coeff a * (↑a : S)) : S[X])
        (HPow.hPow (α := S[X]) X (a - 1)) =
    map f
      (∑ a ∈ range (n + 1),
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff a * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)))
rw₁ :
  ∀ (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
⊢ ((map f p).sum fun (n : ℕ) (a : S) ↦
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (a * (↑n : S)) : S[X]) (HPow.hPow (α := S[X]) X (n - 1))) =
    map f
      (∑ a ∈ range (n + 1),
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff a * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)))

Tactic:
rw [sum_over_range' _ _ (n + 1) ((le_max_right _ _).trans_lt (lt_add_one _))]

Premises used: le_max_right, lt_add_one, HAdd.hAdd, Polynomial.sum_over_range', OfNat.ofNat, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
on_goal :
  ∑ a ∈ range (n + 1),
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((map f p).coeff a * (↑a : S)) : S[X])
        (HPow.hPow (α := S[X]) X (a - 1)) =
    map f
      (∑ a ∈ range (n + 1),
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff a * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)))
on_goal₁ :
  ∀ (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
⊢ ((map f p).sum fun (n : ℕ) (a : S) ↦
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (a * (↑n : S)) : S[X]) (HPow.hPow (α := S[X]) X (n - 1))) =
    map f
      (∑ a ∈ range (n + 1),
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff a * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)))

Tactic:
on_goal 1 => rw [sum_over_range' _ _ (n + 1) ((le_max_right _ _).trans_lt (lt_add_one _))]

Premises used: le_max_right, lt_add_one, HAdd.hAdd, Polynomial.sum_over_range', OfNat.ofNat, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
f : R →+* S
n : ℕ := max p.natDegree (map f p).natDegree
⊢ ∑ a ∈ range (n + 1),
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((map f p).coeff a * (↑a : S)) : S[X])
        (HPow.hPow (α := S[X]) X (a - 1)) =
    map f
      (∑ a ∈ range (n + 1),
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff a * (↑a : R)) : R[X]) (HPow.hPow (α := R[X]) X (a - 1)))

Tactic:
simp only [Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_C, map_mul, coeff_map,
      map_natCast, Polynomial.map_natCast, Polynomial.map_pow, map_X]

Premises used: Polynomial.map_mul, Polynomial.coeff_map, Polynomial.map_pow, Polynomial.map_X, map_mul, map_natCast, Polynomial.map_sum, Polynomial.map_C, Polynomial.map_natCast
-- Module: Mathlib.Algebra.Polynomial.Derivative
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
rw₂ rw₃ : Eq.{v + 1} (α := S[X]) 0 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

Tactic:
rw [zero_mul, C_0, zero_mul]

Premises used: Polynomial.C_0, MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Polynomial.Derivative
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
rw₂ rw₃ : Eq.{u + 1} (α := R[X]) 0 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

Tactic:
rw [zero_mul, C_0, zero_mul]

Premises used: Polynomial.C_0, MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
⊢ (⇑derivative : (a : S[X]) → S[X])^[0] (map f p) = map f ((⇑derivative : (a : R[X]) → R[X])^[0] p)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
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:
simp only [ih, Function.iterate_succ, Polynomial.derivative_map, Function.comp_apply]

Premises used: Function.iterate_succ, Function.comp_apply, Polynomial.derivative_map
-- Module: Mathlib.Algebra.Polynomial.Derivative
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)
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)
⊢ (⇑derivative : (a : S[X]) → S[X])^[k] (map f p) = map f ((⇑derivative : (a : R[X]) → R[X])^[k] p)

Tactic:
induction k generalizing p with
  | zero => simp
  | succ k ih =>
    simp only [ih, Function.iterate_succ, Polynomial.derivative_map, Function.comp_apply]

Premises used: Function.iterate_succ, Function.comp_apply, Polynomial.derivative_map
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
n : ℕ
f : R[X]
⊢ (derivative : (a : R[X]) → R[X]) ((↑n : R[X]) * f) =
    HMul.hMul (α := R[X]) (β := R[X]) ((↑n : R[X]) : R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
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
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
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] ((↑n : R[X]) * f) = (↑n : R[X]) * (⇑derivative : (a : R[X]) → R[X])^[k] f

Tactic:
induction k generalizing f
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
n : ℕ
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:
simp [*]
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
n n_1 : ℕ
h :
  ∀ {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:
simp [*]
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
n : ℕ
this : ¬p.coeff (n + 1) * (↑(n + 1) : R) = 0 ↔ p.coeff (n + 1) ≠ 0
⊢ n ∈ support.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ↔ n + 1 ∈ p.support

Tactic:
simpa only [mem_support_iff, coeff_derivative, Ne, Nat.cast_succ]

Premises used: Polynomial.coeff_derivative, Nat.cast_succ, Polynomial.mem_support_iff, Ne
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
n : ℕ
suffices : ¬p.coeff (n + 1) * (↑(n + 1) : R) = 0 ↔ p.coeff (n + 1) ≠ 0
⊢ n ∈ support.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ↔ n + 1 ∈ p.support

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]
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
n : ℕ
rw : ¬(n + 1 = 0 ∨ p.coeff (n + 1) = 0) ↔ p.coeff (n + 1) ≠ 0
⊢ ¬p.coeff (n + 1) * (↑(n + 1) : R) = 0 ↔ p.coeff (n + 1) ≠ 0

Tactic:
rw [← nsmul_eq_mul', smul_eq_zero]

Premises used: nsmul_eq_mul', smul_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
n : ℕ
⊢ ¬(n + 1 = 0 ∨ p.coeff (n + 1) = 0) ↔ p.coeff (n + 1) ≠ 0

Tactic:
simp only [Nat.succ_ne_zero, false_or]

Premises used: false_or, Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
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 ℕ)
a₁ : (↑(p.natDegree - 1) : WithBot ℕ) ≤ degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p)
⊢ degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) = (↑(p.natDegree - 1) : WithBot ℕ)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
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 ℕ)
⊢ degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ≤ (↑(p.natDegree - 1) : WithBot ℕ)

Tactic:
rw [derivative_apply]

Premises used: Polynomial.derivative_apply
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
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 ℕ)
⊢ 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:
apply le_trans (degree_sum_le _ _) (Finset.sup_le _)

Premises used: Polynomial.degree_sum_le, Finset.sup_le, le_trans
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
n : ℕ
hn : n ∈ p.support
apply : n ≤ p.natDegree
⊢ 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 ℕ)

Tactic:
apply le_trans (degree_C_mul_X_pow_le _ _) (WithBot.coe_le_coe.2 (tsub_le_tsub_right _ _))

Premises used: Iff.mpr, Polynomial.degree_C_mul_X_pow_le, WithBot.coe_le_coe, tsub_le_tsub_right, le_trans
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
n : ℕ
hn : n ∈ p.support
⊢ n ≤ p.natDegree

Tactic:
apply le_natDegree_of_mem_supp _ hn

Premises used: Polynomial.le_natDegree_of_mem_supp
-- Module: Mathlib.Algebra.Polynomial.Derivative
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)

Tactic:
le_sup ?_

Premises used: WithBot.some, Polynomial.degree, Finset.max, Finset.le_sup
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
a : p.natDegree - 1 ∈ support.{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)

Tactic:
refine le_sup ?_

Premises used: Finset.le_sup
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
a : p.coeff p.natDegree ≠ 0
a₁ : 1 ≤ p.natDegree
⊢ p.natDegree - 1 ∈ support.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p)

Tactic:
rw [mem_support_derivative, tsub_add_cancel_of_le, mem_support_iff]

Premises used: Polynomial.mem_support_derivative, tsub_add_cancel_of_le, Polynomial.mem_support_iff
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
a : ¬p = 0
⊢ p.coeff p.natDegree ≠ 0

Tactic:
rw [coeff_natDegree, Ne, leadingCoeff_eq_zero]

Premises used: Polynomial.coeff_natDegree, Ne, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
h : p = 0
⊢ LT.lt (α := ℕ) 0 0

Tactic:
rw [h, natDegree_zero] at hp

Premises used: Polynomial.natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
h : p = 0
hp₁ : LT.lt (α := ℕ) 0 0
⊢ p = 0

Tactic:
rw [h, natDegree_zero] at hp

Premises used: Polynomial.natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : LT.lt (α := ℕ) 0 0
h : p = 0
⊢ False

Tactic:
hp.false

Premises used: LT.lt.false
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : LT.lt (α := ℕ) 0 0
h : p = 0
⊢ False

Tactic:
exact hp.false

Premises used: LT.lt.false
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
⊢ 1 ≤ p.natDegree

Tactic:
hp

Premises used: Nat.lt
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
p : R[X]
hp : 0 < p.natDegree
⊢ 1 ≤ p.natDegree

Tactic:
exact hp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
m : ℕ
⊢ ((⇑derivative : (a : R[X]) → R[X])^[0] p).coeff m = (m + 0).descFactorial 0 • p.coeff (m + 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
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
rw₄ 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

Tactic:
rw [Function.iterate_succ_apply', coeff_derivative, ih m.succ, Nat.succ_add, Nat.add_succ]

Premises used: Polynomial.coeff_derivative, Function.iterate_succ_apply', Nat.add_succ, Nat.succ_add, Nat.succ
-- Module: Mathlib.Algebra.Polynomial.Derivative
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)
rw₂ 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)

Tactic:
rw [← Nat.cast_add_one, ← nsmul_eq_mul', smul_smul]

Premises used: smul_smul, nsmul_eq_mul', Nat.cast_add_one
-- Module: Mathlib.Algebra.Polynomial.Derivative
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)
rw₂ 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)
⊢ ((m + 1) * (m + k).succ.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]

Premises used: Nat.descFactorial_succ, add_tsub_cancel_right, Nat.succ_add