awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
ι : Type y
inst : CommSemiring R
inst_1 : DecidableEq ι
s : Finset ι
f : ι → R[X]
⊢ Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) (∏ b ∈ s, f b))
    (∑ a ∈ s,
      HMul.hMul (α := R[X]) (β := R[X]) (∏ b ∈ s.erase a, f b : R[X]) ((derivative : (a : R[X]) → R[X]) (f a) : R[X]))

Tactic:
simpa using derivative_prod

Premises used: Polynomial.derivative_prod
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Ring R
f : R[X]
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (-f) : R[X]) (-(derivative : (a : R[X]) → R[X]) f : R[X])

Tactic:
map_neg derivative f

Premises used: Polynomial.derivative, map_neg
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Ring R
f : R[X]
k : ℕ
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (-f) = -(⇑derivative : (a : R[X]) → R[X])^[k] f

Tactic:
iterate_map_neg derivative k f

Premises used: Polynomial.derivative, iterate_map_neg
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Ring R
f g : R[X]
⊢ (derivative : (a : R[X]) → R[X]) (f - g) =
    HSub.hSub (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X])
      ((derivative : (a : R[X]) → R[X]) g : R[X])

Tactic:
map_sub derivative f g

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

Tactic:
rw [derivative_sub, derivative_X, derivative_C, sub_zero]

Premises used: Polynomial.derivative_X, sub_zero, Polynomial.derivative_sub, Polynomial.derivative_C
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Ring R
k : ℕ
f g : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (f - g) =
    (⇑derivative : (a : R[X]) → R[X])^[k] f - (⇑derivative : (a : R[X]) → R[X])^[k] g

Tactic:
iterate_map_sub derivative k f g

Premises used: Polynomial.derivative, iterate_map_sub
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Ring 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 [← C_eq_intCast n]

Premises used: Polynomial.C_eq_intCast
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Ring 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 : Ring 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 : Ring 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 : Ring 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 : Ring 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 : Ring 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 : CommRing R
p : R[X]
⊢ (derivative : (a : R[X]) → R[X]) (p.comp (HSub.hSub (α := R[X]) 1 X)) =
    -comp ((derivative : (a : R[X]) → R[X]) p) (HSub.hSub (α := R[X]) 1 X)

Tactic:
simp [derivative_comp]

Premises used: Polynomial.derivative_comp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[0] (p.comp (HSub.hSub (α := R[X]) 1 X)) =
    HPow.hPow (α := R[X]) (β := ℕ) (-1) 0 * ((⇑derivative : (a : R[X]) → R[X])^[0] p).comp (HSub.hSub (α := R[X]) 1 X)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
k : ℕ
ih :
  ∀ (p : R[X]),
    (⇑derivative : (a : R[X]) → R[X])^[k] (p.comp (HSub.hSub (α := R[X]) 1 X)) =
      HPow.hPow (α := R[X]) (-1) k * ((⇑derivative : (a : R[X]) → R[X])^[k] p).comp (HSub.hSub (α := R[X]) 1 X)
p : R[X]
⊢ (⇑derivative : (a : R[X]) → R[X])^[k + 1] (p.comp (HSub.hSub (α := R[X]) 1 X)) =
    HPow.hPow (α := R[X]) (-1) (k + 1) * ((⇑derivative : (a : R[X]) → R[X])^[k + 1] p).comp (HSub.hSub (α := R[X]) 1 X)

Tactic:
simp [ih (derivative p), derivative_comp, pow_succ]

Premises used: Polynomial.derivative, pow_succ, Polynomial.derivative_comp, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
p : R[X]
k : ℕ
zero :
  ∀ (p : R[X]),
    (⇑derivative : (a : R[X]) → R[X])^[0] (p.comp (HSub.hSub (α := R[X]) 1 X)) =
      HPow.hPow (α := R[X]) (β := ℕ) (-1) 0 * ((⇑derivative : (a : R[X]) → R[X])^[0] p).comp (HSub.hSub (α := R[X]) 1 X)
succ :
  ∀ (k : ℕ)
    (ih :
      ∀ (p : R[X]),
        (⇑derivative : (a : R[X]) → R[X])^[k] (p.comp (HSub.hSub (α := R[X]) 1 X)) =
          HPow.hPow (α := R[X]) (-1) k * ((⇑derivative : (a : R[X]) → R[X])^[k] p).comp (HSub.hSub (α := R[X]) 1 X))
    (p : R[X]),
    (⇑derivative : (a : R[X]) → R[X])^[k + 1] (p.comp (HSub.hSub (α := R[X]) 1 X)) =
      HPow.hPow (α := R[X]) (-1) (k + 1) *
        ((⇑derivative : (a : R[X]) → R[X])^[k + 1] p).comp (HSub.hSub (α := R[X]) 1 X)
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (p.comp (HSub.hSub (α := R[X]) 1 X)) =
    HPow.hPow (α := R[X]) (-1) k * ((⇑derivative : (a : R[X]) → R[X])^[k] p).comp (HSub.hSub (α := R[X]) 1 X)

Tactic:
induction k generalizing p with
  | zero => simp
  | succ k ih => simp [ih (derivative p), derivative_comp, pow_succ]

Premises used: pow_succ, Polynomial.derivative_comp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
inst_1 : DecidableEq R
S : Multiset R
r : R
hr : r ∈ S
nth_rw :
  eval r
      ((derivative : (a : R[X]) → R[X])
        (Multiset.prod
          (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
            (r ::ₘ S.erase r)))) =
    Multiset.prod (Multiset.map (fun (a : R) ↦ r - a) (S.erase r))
⊢ eval r
      ((derivative : (a : R[X]) → R[X])
        (Multiset.prod
          (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) S))) =
    Multiset.prod (Multiset.map (fun (a : R) ↦ r - a) (S.erase r))

Tactic:
nth_rw 1 [← Multiset.cons_erase hr]

Premises used: Multiset.cons_erase
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
inst_1 : DecidableEq R
S : Multiset R
r : R
hr : r ∈ S
⊢ Eq (α := R)
    (((↑(evalRingHom r) : R[X] →* R) : (a : R[X]) → R)
        (Multiset.prod
          (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
            (S.erase r))) :
      R)
    (Multiset.prod
        (Multiset.map (α := R[X]) (⇑(↑(evalRingHom r) : R[X] →* R) : (a : R[X]) → R)
          (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
            (S.erase r))) :
      R)

Tactic:
have := (evalRingHom r).map_multiset_prod (Multiset.map (fun a => X - C a) (S.erase r))
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
inst_1 : DecidableEq R
S : Multiset R
r : R
hr : r ∈ S
this :
  Eq (α := R)
    (((↑(evalRingHom r) : R[X] →* R) : (a : R[X]) → R)
        (Multiset.prod
          (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
            (S.erase r))) :
      R)
    (Multiset.prod
        (Multiset.map (α := R[X]) (⇑(↑(evalRingHom r) : R[X] →* R) : (a : R[X]) → R)
          (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
            (S.erase r))) :
      R)
⊢ eval r
      ((derivative : (a : R[X]) → R[X])
        (Multiset.prod
          (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
            (r ::ₘ S.erase r)))) =
    Multiset.prod (Multiset.map (fun (a : R) ↦ r - a) (S.erase r))

Tactic:
simpa using this
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
c : R
m : ℕ
rw :
  HMul.hMul (β := R[X])
      ((C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1))
      ((derivative : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) : R[X]) =
    (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
rw₁ :
  (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1) * 1 =
    (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
rw₂ rw₃ :
  (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1) =
    (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)
⊢ (derivative : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ m) =
    (C : (a : R) → R[X]) (↑m : R) * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (m - 1)

Tactic:
rw [derivative_pow, derivative_X_sub_C, mul_one]

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

Tactic:
rw [derivative_sq, derivative_X_sub_C, mul_one]

Premises used: Polynomial.derivative_sq, mul_one, Polynomial.derivative_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
n k : ℕ
c : R
rw :
  (⇑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)
rw₁ :
  (⇑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)
rw₂ rw₃ :
  n.descFactorial k • HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-c) : R[X]) ^ (n - k) =
    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] (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
    n.descFactorial k • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - k)

Tactic:
rw [sub_eq_add_neg, ← C_neg, iterate_derivative_X_add_pow]

Premises used: Polynomial.iterate_derivative_X_add_pow, sub_eq_add_neg, Polynomial.C_neg
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
n : ℕ
c : R
rw : n.descFactorial n • HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ (n - n) = (↑n ! : R[X])
rw₁ :
  n.descFactorial n • HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X])) 0 =
    (↑n ! : R[X])
rw₂ : HSMul.hSMul (β := R[X]) (n.descFactorial n) 1 = (↑n ! : R[X])
rw₃ : Eq.{u + 1} (α := R[X]) (↑(n.descFactorial n) : R[X]) (↑n ! : R[X])
rw₄ rw₅ : Eq.{u + 1} (α := R[X]) (↑n ! : R[X]) (↑n ! : R[X])
⊢ (⇑derivative : (a : R[X]) → R[X])^[n] (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) c : R[X]) ^ n) =
    (↑n ! : R[X])

Tactic:
rw [iterate_derivative_X_sub_pow, n.sub_self, pow_zero, nsmul_one, n.descFactorial_self]

Premises used: Polynomial.iterate_derivative_X_sub_pow, pow_zero, Nat.sub_self, Nat.descFactorial_self, nsmul_one
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
k : ℕ
P : R[X]
h : P.degree < (↑k : WithBot ℕ)
induction : ∀ {P : R[X]} (h : P.degree < (↑0 : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[0] P = 0
succ :
  ∀ (n : ℕ),
    (∀ {P : R[X]} (h : P.degree < (↑n : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[n] P = 0) →
      ∀ {P : R[X]} (h : P.degree < (↑(n + 1) : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[n + 1] P = 0
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] P = 0

Tactic:
induction k generalizing P
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
P : R[X]
h : P.degree < (↑0 : WithBot ℕ)
⊢ (⇑derivative : (a : R[X]) → R[X])^[0] P = 0

Tactic:
degree_eq_bot.mp <| WithBot.lt_coe_bot.mp h

Premises used: WithBot.lt_coe_bot, Iff.mp, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
P : R[X]
h : P.degree < (↑0 : WithBot ℕ)
⊢ (⇑derivative : (a : R[X]) → R[X])^[0] P = 0

Tactic:
exact degree_eq_bot.mp <| WithBot.lt_coe_bot.mp h

Premises used: WithBot.lt_coe_bot, Iff.mp, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
P : R[X]
h : P.degree < (↑0 : WithBot ℕ)
⊢ (⇑derivative : (a : R[X]) → R[X])^[0] P = 0

Tactic:
case zero => exact degree_eq_bot.mp <| WithBot.lt_coe_bot.mp h

Premises used: WithBot.lt_coe_bot, Iff.mp, Polynomial.degree_eq_bot
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
pos : P = 0 → (⇑derivative : (a : R[X]) → R[X])^[k + 1] P = 0
neg : ¬P = 0 → (⇑derivative : (a : R[X]) → R[X])^[k + 1] P = 0
⊢ (⇑derivative : (a : R[X]) → R[X])^[k + 1] P = 0

Tactic:
by_cases P = 0
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : P = 0
⊢ (⇑derivative : (a : R[X]) → R[X])^[k + 1] P = 0

Tactic:
simp [hP]
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
h_1 : P = 0
⊢ (⇑derivative : (a : R[X]) → R[X])^[k + 1] P = 0

Tactic:
case pos hP => simp [hP]
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
rw : Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] ((derivative : (a : R[X]) → R[X]) P) : R[X]) (0 : R[X])
⊢ (⇑derivative : (a : R[X]) → R[X])^[k + 1] P = 0

Tactic:
rw [Function.iterate_add_apply, Function.iterate_one]

Premises used: Function.iterate_add_apply, Function.iterate_one
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
pos :
  Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X]) →
    Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] ((derivative : (a : R[X]) → R[X]) P) : R[X]) (0 : R[X])
neg :
  ¬Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X]) →
    Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] ((derivative : (a : R[X]) → R[X]) P) : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] ((derivative : (a : R[X]) → R[X]) P) : R[X]) (0 : R[X])

Tactic:
by_cases derivative P = 0

Premises used: Polynomial.derivative, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
hP' : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] ((derivative : (a : R[X]) → R[X]) P) : R[X]) (0 : R[X])

Tactic:
simp [hP']
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
h_1 : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] ((derivative : (a : R[X]) → R[X]) P) : R[X]) (0 : R[X])

Tactic:
case pos hP' => simp [hP']
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
hP' : ¬Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
contrapose : ∀ (hP' : P.natDegree = 0), Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
⊢ P.natDegree ≠ 0

Tactic:
contrapose hP'
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
hP' : P.natDegree = 0
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])

Tactic:
derivative_of_natDegree_zero hP'

Premises used: Polynomial.derivative_of_natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
hP' : P.natDegree = 0
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])

Tactic:
exact derivative_of_natDegree_zero hP'

Premises used: Polynomial.derivative_of_natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
hP' : ¬Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
⊢ P.natDegree ≠ 0

Tactic:
have hP'' : P.natDegree ≠ 0 := by
          contrapose hP'
          exact derivative_of_natDegree_zero hP'
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
hP' : ¬Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
hP'' : P.natDegree ≠ 0
⊢ Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] ((derivative : (a : R[X]) → R[X]) P) : R[X]) (0 : R[X])

Tactic:
ind <| (natDegree_lt_iff_degree_lt hP').mp ?_

Premises used: Polynomial.natDegree_lt_iff_degree_lt, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
hP' : ¬Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
hP'' : P.natDegree ≠ 0
refine : natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) P) < k
⊢ Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] ((derivative : (a : R[X]) → R[X]) P) : R[X]) (0 : R[X])

Tactic:
refine ind <| (natDegree_lt_iff_degree_lt hP').mp ?_

Premises used: Polynomial.natDegree_lt_iff_degree_lt, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
k : ℕ
ind : ∀ {P : R[X]} (h : P.degree < (↑k : WithBot ℕ)), (⇑derivative : (a : R[X]) → R[X])^[k] P = 0
P : R[X]
h : P.degree < (↑(k + 1) : WithBot ℕ)
hP : ¬P = 0
hP' : ¬Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
hP'' : P.natDegree ≠ 0
linarith :
  k ≤ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) P) →
    -1 + HSub.hSub (α := ℤ) (↑k : ℤ) (↑(natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) P)) : ℤ) +
          (HAdd.hAdd (α := ℤ) (↑P.natDegree : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1) +
        (HAdd.hAdd (α := ℤ) (↑(natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) P)) : ℤ) 1 -
          (↑P.natDegree : ℤ)) =
      0
⊢ natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) P) < k

Tactic:
linarith [(natDegree_lt_iff_degree_lt hP).mpr h, natDegree_derivative_lt hP'']

Premises used: Iff.mpr, Polynomial.natDegree_lt_iff_degree_lt, Polynomial.natDegree_derivative_lt