awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : 0 ∈ p.support
h_1 : 0 ≠ n + 1
h₀ : (p.coeff 0 * 0 * if n = HSub.hSub (α := ℕ) 0 1 then 1 else 0) = 0
h₁ : HMul.hMul (α := R) 0 (if n = HSub.hSub (α := ℕ) 0 1 then 1 else 0) = 0
h₂ h₃ : Eq.{u + 1} (α := R) 0 0
⊢ (p.coeff 0 * (↑0 : R) * if n = HSub.hSub (α := ℕ) 0 1 then 1 else 0) = 0

Tactic:
rw [Nat.cast_zero, mul_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, Nat.cast_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
n n_1 : ℕ
h : n_1 + 1 ∈ p.support
H : n_1 + 1 ≠ n + 1
h₀ : (p.coeff (n_1 + 1) * (↑(n_1 + 1) : R) * if n = n_1 then 1 else 0) = 0
h₁ : p.coeff (n_1 + 1) * (↑(n_1 + 1) : R) * 0 = 0
h₂ h₃ : Eq.{u + 1} (α := R) 0 0
⊢ (p.coeff (n_1 + 1) * (↑(n_1 + 1) : R) * if n = n_1 + 1 - 1 then 1 else 0) = 0

Tactic:
rw [Nat.add_one_sub_one, if_neg (mt (congr_arg Nat.succ) H.symm), mul_zero]

Premises used: Nat.add_one_sub_one, mt, Ne.symm, MulZeroClass.mul_zero, congr_arg, Nat.succ, if_neg
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ n + 1 ∉ p.support → (p.coeff (n + 1) * (↑(n + 1) : R) * if n = n + 1 - 1 then 1 else 0) = 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) 0) 0

Tactic:
derivative.map_zero

Premises used: Polynomial.derivative, LinearMap.map_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
k : ℕ
⊢ Eq.{u + 1} (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] 0) 0

Tactic:
iterate_map_zero derivative k

Premises used: Polynomial.derivative, iterate_map_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
hf :
  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
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) a) : R[X])
    ((monomial (n - 1) : (a : R) → R[X]) (a * (↑n : R)) : R[X])

Tactic:
rw [derivative_apply, sum_monomial_index, C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.sum_monomial_index, Polynomial.derivative_apply
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
a : R
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

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
rw :
  Eq (α := R[X]) ((monomial (n + 1 - 1) : (a : R) → R[X]) (a * (↑(n + 1) : R)) : R[X])
    ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
rw₁ :
  Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (a * (↑(n + 1) : R)) : R[X])
    ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
rw₂ :
  Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) (↑1 : R)) : R[X])
    ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
rw₃ rw₄ :
  Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
    ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial (n + 1) : (a : R) → R[X]) a) : R[X])
    ((monomial n : (a : R) → R[X]) (a * HAdd.hAdd (α := R) (↑n : R) 1) : R[X])

Tactic:
rw [derivative_monomial, add_tsub_cancel_right, Nat.cast_add, Nat.cast_one]

Premises used: Polynomial.derivative_monomial, Nat.cast_add, add_tsub_cancel_right, Nat.cast_one
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
a : R
⊢ Eq (α := R[X])
    ((derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X) : R[X])
    ((C : (a : R) → R[X]) a : R[X])

Tactic:
simp [C_mul_X_eq_monomial, mul_one]

Premises used: Polynomial.C_mul_X_eq_monomial, mul_one
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
rw :
  (derivative : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) a) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))
rw₁ :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) a) : R[X])
    ((monomial (n - 1) : (a : R) → R[X]) (a * (↑n : R)) : R[X])
rw₂ rw₃ :
  Eq (α := R[X]) ((monomial (n - 1) : (a : R) → R[X]) (a * (↑n : R)) : R[X])
    ((monomial (n - 1) : (a : R) → R[X]) (a * (↑n : R)) : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑n : R)) : R[X]) (HPow.hPow (α := R[X]) X (n - 1))

Tactic:
rw [C_mul_X_pow_eq_monomial, C_mul_X_pow_eq_monomial, derivative_monomial]

Premises used: Polynomial.derivative_monomial, Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
a : R
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * (↑2 : R)) : R[X])
      (HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1)) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) X
rw₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) (HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1)) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) X
rw₂ rw₃ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) X =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) X
⊢ (derivative : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2)) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (a * 2) : R[X]) X

Tactic:
rw [derivative_C_mul_X_pow, Nat.cast_two, pow_one]

Premises used: pow_one, Polynomial.derivative_C_mul_X_pow, Nat.cast_two
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ (derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) 1 * HPow.hPow (α := R[X]) X n) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HMul.hMul (α := R) 1 (↑n : R)) : R[X])
      (HPow.hPow (α := R[X]) X (n - 1))

Tactic:
derivative_C_mul_X_pow (1 : R) n

Premises used: Polynomial.derivative_C_mul_X_pow, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
n : ℕ
h : HPow.hPow (α := R[X]) X n = (C : (a : R) → R[X]) 1 * HPow.hPow (α := R[X]) X n
h₁ : (↑n : R) = HMul.hMul (α := R) 1 (↑n : R)
⊢ (derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X n) =
    (C : (a : R) → R[X]) (↑n : R) * HPow.hPow (α := R[X]) X (n - 1)

Tactic:
convert! derivative_C_mul_X_pow (1 : R) n

Premises used: Polynomial.derivative_C_mul_X_pow, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ HPow.hPow (α := R[X]) X n = (C : (a : R) → R[X]) 1 * HPow.hPow (α := R[X]) X n

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ (↑n : R) = HMul.hMul (α := R) 1 (↑n : R)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ (derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HAdd.hAdd (α := R) (↑n : R) 1) : R[X]) (HPow.hPow (α := R[X]) X n)

Tactic:
simp [derivative_X_pow]

Premises used: Polynomial.derivative_X_pow
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
rw :
  (C : (a : R) → R[X]) (↑2 : R) * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X
rw₁ :
  (C : (a : R) → R[X]) 2 * HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 2 1) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X
rw₂ rw₃ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X
⊢ (derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 2) X

Tactic:
rw [derivative_X_pow, Nat.cast_two, pow_one]

Premises used: pow_one, Polynomial.derivative_X_pow, Nat.cast_two
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
a : R
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) a) : R[X]) (0 : R[X])

Tactic:
simp [derivative_apply]

Premises used: Polynomial.derivative_apply
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree = 0
rw : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) (p.coeff 0)) : R[X]) (0 : R[X])
rw₁ rw₂ : Eq.{u + 1} (α := R[X]) 0 0
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])

Tactic:
rw [eq_C_of_natDegree_eq_zero hp, derivative_C]

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, Polynomial.derivative_C
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
⊢ Eq (α := R[X]) ((monomial (HSub.hSub (α := ℕ) 1 1) : (a : R) → R[X]) (HMul.hMul (α := R) 1 (↑1 : R)) : R[X])
    (1 : R[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) 1) 0

Tactic:
derivative_C

Premises used: Polynomial.derivative_C
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
f g : R[X]
⊢ (derivative : (a : R[X]) → R[X]) (f + g) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X])
      ((derivative : (a : R[X]) → R[X]) g : R[X])

Tactic:
derivative.map_add f g

Premises used: Polynomial.derivative, LinearMap.map_add
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
c : R
rw :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) X : R[X])
      ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) c) : R[X]) =
    1
rw₁ :
  HAdd.hAdd (α := R[X]) (β := R[X]) (1 : R[X]) ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) c) : R[X]) = 1
rw₂ : HAdd.hAdd (α := R[X]) 1 0 = 1
rw₃ rw₄ : Eq.{u + 1} (α := R[X]) 1 1
⊢ Eq (α := 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])
    (1 : R[X])

Tactic:
rw [derivative_add, derivative_X, derivative_C, add_zero]

Premises used: Polynomial.derivative_X, Polynomial.derivative_C, add_zero, Polynomial.derivative_add
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
ι : Type y
inst : Semiring R
s : Finset ι
f : ι → R[X]
⊢ Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) (∑ b ∈ s, f b))
    (∑ b ∈ s, (derivative : (a : R[X]) → R[X]) (f b))

Tactic:
map_sum ..

Premises used: map_sum
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
ι : Type y
inst : Semiring R
k : ℕ
s : Finset ι
f : ι → R[X]
simp_rw :
  Eq (α := R[X]) ((HPow.hPow (α := Module.End R R[X]) derivative k : (a : R[X]) → R[X]) (∑ b ∈ s, f b))
    (∑ x ∈ s, (HPow.hPow (α := Module.End R R[X]) derivative k : (a : R[X]) → R[X]) (f x))
⊢ Eq.{u + 1} (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] (∑ b ∈ s, f b))
    (∑ b ∈ s, (⇑derivative : (a : R[X]) → R[X])^[k] (f b))

Tactic:
simp_rw [← Module.End.pow_apply, map_sum]

Premises used: Module.End.pow_apply, map_sum
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p : R[X]
⊢ (derivative : (a : R[X]) → R[X]) (s • p) = HSMul.hSMul (β := R[X]) s ((derivative : (a : R[X]) → R[X]) p : R[X])

Tactic:
derivative.map_smul_of_tower s p

Premises used: Polynomial.derivative, LinearMap.map_smul_of_tower
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[0] (s • p) = s • (⇑derivative : (a : R[X]) → R[X])^[0] p

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
k : ℕ
ih : ∀ (p : R[X]), (⇑derivative : (a : R[X]) → R[X])^[k] (s • p) = s • (⇑derivative : (a : R[X]) → R[X])^[k] p
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[k + 1] (s • p) = s • (⇑derivative : (a : R[X]) → R[X])^[k + 1] p

Tactic:
simp [ih]
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p : R[X]
k : ℕ
zero : ∀ (p : R[X]), (⇑derivative : (a : R[X]) → R[X])^[0] (s • p) = s • (⇑derivative : (a : R[X]) → R[X])^[0] p
succ :
  ∀ (k : ℕ)
    (ih : ∀ (p : R[X]), (⇑derivative : (a : R[X]) → R[X])^[k] (s • p) = s • (⇑derivative : (a : R[X]) → R[X])^[k] p)
    (p : R[X]), (⇑derivative : (a : R[X]) → R[X])^[k + 1] (s • p) = s • (⇑derivative : (a : R[X]) → R[X])^[k + 1] p
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (s • p) = s • (⇑derivative : (a : R[X]) → R[X])^[k] p

Tactic:
induction k generalizing p with
  | zero => simp
  | succ k ih => simp [ih]
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
a : R
p : R[X]
k : ℕ
simp_rw : (⇑derivative : (a : R[X]) → R[X])^[k] (a • p) = a • (⇑derivative : (a : R[X]) → R[X])^[k] p
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] p)

Tactic:
simp_rw [← smul_eq_C_mul, iterate_derivative_smul]

Premises used: Polynomial.smul_eq_C_mul, Polynomial.iterate_derivative_smul
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
a : R
p : R[X]
⊢ (derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X])

Tactic:
iterate_derivative_C_mul _ _ 1

Premises used: Nat.iterate, Polynomial.iterate_derivative_C_mul, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n ∈ support.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p)
h1 : p.coeff (n + 1) = 0
rw : p.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1 = 0
rw₁ : 0 * HAdd.hAdd (α := R) (↑n : R) 1 = 0
rw₂ rw₃ : Eq.{u + 1} (α := R) 0 0
⊢ Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) p) n) 0

Tactic:
rw [coeff_derivative, h1, zero_mul]

Premises used: Polynomial.coeff_derivative, MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
⊢ degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.degree

Tactic:
(Finset.sup_lt_iff <| bot_lt_iff_ne_bot.2 <| mt degree_eq_bot.1 hp).2 fun n hp =>
    lt_of_lt_of_le (WithBot.coe_lt_coe.2 n.lt_succ_self) <|
      Finset.le_sup <| of_mem_support_derivative hp

Premises used: Iff.mpr, Polynomial.of_mem_support_derivative, mt, Nat.lt_succ_self, bot_lt_iff_ne_bot, Polynomial.degree, Finset.sup_lt_iff, WithBot.coe_lt_coe, Finset.max, Iff.mp, Polynomial.degree_eq_bot, lt_of_lt_of_le, Finset.le_sup
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
this : DecidableEq R := Classical.decEq R
H : p = 0
rw : degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) 0) = degree.{u} (R := R) 0
rw₁ rw₂ : degree.{u} (R := R) 0 = degree.{u} (R := R) 0
⊢ degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) = p.degree

Tactic:
rw [H, derivative_zero]

Premises used: Polynomial.derivative_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
inl :
  ∀ (hp' : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])),
    natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.natDegree
inr :
  ∀ (hp' : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])),
    natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.natDegree
⊢ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.natDegree

Tactic:
rcases eq_or_ne (derivative p) 0 with hp' | hp'

Premises used: Polynomial.derivative, eq_or_ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
inl : 0 < p.natDegree
⊢ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.natDegree

Tactic:
rw [hp', Polynomial.natDegree_zero]

Premises used: Polynomial.natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
⊢ 0 < p.natDegree

Tactic:
hp.bot_lt

Premises used: Ne.bot_lt
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
⊢ 0 < p.natDegree

Tactic:
exact hp.bot_lt

Premises used: Ne.bot_lt
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
inr : degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.degree
⊢ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.natDegree

Tactic:
rw [natDegree_lt_natDegree_iff hp']

Premises used: Polynomial.natDegree_lt_natDegree_iff
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
⊢ degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.degree

Tactic:
degree_derivative_lt fun h => hp (h.symm ▸ natDegree_zero)

Premises used: Eq.rec, Polynomial.degree_derivative_lt, Polynomial.natDegree_zero, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
⊢ degree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.degree

Tactic:
exact degree_derivative_lt fun h => hp (h.symm ▸ natDegree_zero)
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
pos : ∀ (p0 : p.natDegree = 0), natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ≤ p.natDegree - 1
neg : ∀ (p0 : ¬p.natDegree = 0), natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ≤ p.natDegree - 1
⊢ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ≤ p.natDegree - 1

Tactic:
by_cases p0 : p.natDegree = 0

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
p0 : p.natDegree = 0
⊢ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ≤ p.natDegree - 1

Tactic:
simp [p0, derivative_of_natDegree_zero]

Premises used: Polynomial.derivative_of_natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
p0 : ¬p.natDegree = 0
⊢ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ≤ p.natDegree - 1

Tactic:
Nat.le_sub_one_of_lt (natDegree_derivative_lt p0)

Premises used: Nat.le_sub_one_of_lt, Polynomial.natDegree_derivative_lt
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
p0 : ¬p.natDegree = 0
⊢ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) ≤ p.natDegree - 1

Tactic:
exact Nat.le_sub_one_of_lt (natDegree_derivative_lt p0)

Premises used: Nat.le_sub_one_of_lt, Polynomial.natDegree_derivative_lt
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
zero : p.natDegree ≤ p.natDegree - 0
zero₁ zero₂ : p.natDegree ≤ p.natDegree
⊢ ((⇑derivative : (a : R[X]) → R[X])^[0] p).natDegree ≤ p.natDegree - 0

Tactic:
rw [Function.iterate_zero_apply, Nat.sub_zero]

Premises used: Nat.sub_zero, Function.iterate_zero_apply
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
d : ℕ
hd : ((⇑derivative : (a : R[X]) → R[X])^[d] p).natDegree ≤ p.natDegree - d
succ :
  natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[d] p)) ≤
    p.natDegree - d - 1
⊢ ((⇑derivative : (a : R[X]) → R[X])^[d + 1] p).natDegree ≤ p.natDegree - (d + 1)

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

Premises used: Function.iterate_succ_apply', Nat.sub_succ'
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
d : ℕ
hd : ((⇑derivative : (a : R[X]) → R[X])^[d] p).natDegree ≤ p.natDegree - d
⊢ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[d] p)) ≤
    p.natDegree - d - 1

Tactic:
(natDegree_derivative_le _).trans <| Nat.sub_le_sub_right hd 1

Premises used: Polynomial.natDegree_derivative_le, Nat.sub_le_sub_right, LE.le.trans, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
d : ℕ
hd : ((⇑derivative : (a : R[X]) → R[X])^[d] p).natDegree ≤ p.natDegree - d
⊢ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) ((⇑derivative : (a : R[X]) → R[X])^[d] p)) ≤
    p.natDegree - d - 1

Tactic:
exact (natDegree_derivative_le _).trans <| Nat.sub_le_sub_right hd 1

Premises used: Polynomial.natDegree_derivative_le, Nat.sub_le_sub_right, LE.le.trans, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
k : ℕ
zero : ((⇑derivative : (a : R[X]) → R[X])^[0] p).natDegree ≤ p.natDegree - 0
succ :
  ∀ (d : ℕ) (hd : ((⇑derivative : (a : R[X]) → R[X])^[d] p).natDegree ≤ p.natDegree - d),
    ((⇑derivative : (a : R[X]) → R[X])^[d + 1] p).natDegree ≤ p.natDegree - (d + 1)
⊢ ((⇑derivative : (a : R[X]) → R[X])^[k] p).natDegree ≤ p.natDegree - k

Tactic:
induction k with
  | zero => rw [Function.iterate_zero_apply, Nat.sub_zero]
  | succ d hd =>
      rw [Function.iterate_succ_apply', Nat.sub_succ']
      exact (natDegree_derivative_le _).trans <| Nat.sub_le_sub_right hd 1

Premises used: Function.iterate_succ_apply', Nat.sub_succ', Polynomial.natDegree_derivative_le, Nat.sub_zero, LE.le.trans, Function.iterate_zero_apply
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
n : ℕ
rw : Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) (↑n : R)) : R[X]) (0 : R[X])
⊢ Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) (↑n : R[X])) 0

Tactic:
rw [← map_natCast C n]

Premises used: Polynomial.C, map_natCast
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) (↑n : R)) : R[X]) (0 : R[X])

Tactic:
derivative_C

Premises used: Polynomial.derivative_C
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) (↑n : R)) : R[X]) (0 : R[X])

Tactic:
exact derivative_C

Premises used: Polynomial.derivative_C
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) (OfNat.ofNat n)) 0

Tactic:
derivative_natCast

Premises used: Polynomial.derivative_natCast
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : ℕ
hx : p.natDegree < x
h :
  ∀ (n : ℕ)
    (ih :
      ∀ m < n,
        ∀ {p : R[X]} {x : ℕ} (hx : p.natDegree < x) (h : p.natDegree = m), (⇑derivative : (a : R[X]) → R[X])^[x] p = 0)
    {p : R[X]} {x : ℕ} (hx : p.natDegree < x) (h : p.natDegree = n), (⇑derivative : (a : R[X]) → R[X])^[x] p = 0
⊢ (⇑derivative : (a : R[X]) → R[X])^[x] p = 0

Tactic:
induction h : p.natDegree using Nat.strong_induction_on generalizing p x with | _ _ ih

Premises used: Polynomial.natDegree