awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
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
⊢ ∀ m < p.natDegree,
    ∀ {p : R[X]} {x : ℕ} (hx : p.natDegree < x) (h : p.natDegree = m), (⇑derivative : (a : R[X]) → R[X])^[x] p = 0

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

Tactic:
obtain ⟨t, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (pos_of_gt hx).ne'

Premises used: pos_of_gt, LT.lt.ne', Nat.exists_eq_succ_of_ne_zero, rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
ih :
  ∀ m < p.natDegree,
    ∀ {p : R[X]} {x : ℕ} (hx : p.natDegree < x) (h : p.natDegree = m), (⇑derivative : (a : R[X]) → R[X])^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
h : Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[t] ((derivative : (a : R[X]) → R[X]) p) : R[X]) (0 : R[X])
⊢ (⇑derivative : (a : R[X]) → R[X])^[t.succ] p = 0

Tactic:
rw [Function.iterate_succ_apply]

Premises used: Function.iterate_succ_apply
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
ih :
  ∀ m < p.natDegree,
    ∀ {p : R[X]} {x : ℕ} (hx : p.natDegree < x) (h : p.natDegree = m), (⇑derivative : (a : R[X]) → R[X])^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
pos :
  ∀ (hp : p.natDegree = 0),
    Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[t] ((derivative : (a : R[X]) → R[X]) p) : R[X]) (0 : R[X])
neg :
  ∀ (hp : ¬p.natDegree = 0),
    Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[t] ((derivative : (a : R[X]) → R[X]) p) : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[t] ((derivative : (a : R[X]) → R[X]) p) : R[X]) (0 : R[X])

Tactic:
by_cases hp : p.natDegree = 0

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
ih :
  ∀ m < p.natDegree,
    ∀ {p : R[X]} {x : ℕ} (hx : p.natDegree < x) (h : p.natDegree = m), (⇑derivative : (a : R[X]) → R[X])^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : p.natDegree = 0
pos : Eq.{u + 1} (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[t] 0) 0
pos₁ pos₂ : Eq.{u + 1} (α := R[X]) 0 0
⊢ Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[t] ((derivative : (a : R[X]) → R[X]) p) : R[X]) (0 : R[X])

Tactic:
rw [derivative_of_natDegree_zero hp, iterate_derivative_zero]

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

Tactic:
have := natDegree_derivative_lt hp
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
ih :
  ∀ m < p.natDegree,
    ∀ {p : R[X]} {x : ℕ} (hx : p.natDegree < x) (h : p.natDegree = m), (⇑derivative : (a : R[X]) → R[X])^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : ¬p.natDegree = 0
this : natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.natDegree
⊢ Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[t] ((derivative : (a : R[X]) → R[X]) p) : R[X]) (0 : R[X])

Tactic:
ih _ this (this.trans_le <| Nat.le_of_lt_succ hx) rfl

Premises used: LT.lt.trans_le, Nat.le_of_lt_succ, rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
p : R[X]
ih :
  ∀ m < p.natDegree,
    ∀ {p : R[X]} {x : ℕ} (hx : p.natDegree < x) (h : p.natDegree = m), (⇑derivative : (a : R[X]) → R[X])^[x] p = 0
t : ℕ
hx : p.natDegree < t.succ
hp : ¬p.natDegree = 0
this : natDegree.{u} (R := R) ((derivative : (a : R[X]) → R[X]) p) < p.natDegree
⊢ Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[t] ((derivative : (a : R[X]) → R[X]) p) : R[X]) (0 : R[X])

Tactic:
exact ih _ this (this.trans_le <| Nat.le_of_lt_succ hx) rfl

Premises used: LT.lt.trans_le, Nat.le_of_lt_succ, rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
a : R
inst : Semiring R
k : ℕ
h : 0 < k
⊢ Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[k] ((C : (a : R) → R[X]) a) : R[X]) (0 : R[X])

Tactic:
iterate_derivative_eq_zero <| (natDegree_C _).trans_lt h

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

Tactic:
iterate_derivative_C h

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

Tactic:
iterate_derivative_eq_zero <| natDegree_X_le.trans_lt h

Premises used: Polynomial.iterate_derivative_eq_zero, Polynomial.natDegree_X_le, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
inl : ∀ (h : Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) 0) 0), natDegree.{u} (R := R) 0 = 0
inr : ∀ (hf : f ≠ 0), f.natDegree = 0
⊢ f.natDegree = 0

Tactic:
rcases eq_or_ne f 0 with (rfl | hf)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
h : Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) 0) 0
⊢ natDegree.{u} (R := R) 0 = 0

Tactic:
natDegree_zero

Premises used: Polynomial.natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
h : Eq.{u + 1} (α := R[X]) ((derivative : (a : R[X]) → R[X]) 0) 0
⊢ natDegree.{u} (R := R) 0 = 0

Tactic:
exact natDegree_zero

Premises used: Polynomial.natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hf : f ≠ 0
inr : f.degree ≤ 0
⊢ f.natDegree = 0

Tactic:
rw [natDegree_eq_zero_iff_degree_le_zero]

Premises used: Polynomial.natDegree_eq_zero_iff_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hf : f ≠ 0
inr : ∀ (f_nat_degree_pos : 0 < f.degree), False
⊢ f.degree ≤ 0

Tactic:
by_contra! f_nat_degree_pos
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hf : f ≠ 0
f_nat_degree_pos : 0 < f.degree
⊢ 0 < f.natDegree

Tactic:
rw [← natDegree_pos_iff_degree_pos] at f_nat_degree_pos

Premises used: Polynomial.natDegree_pos_iff_degree_pos
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
⊢ m + 1 = f.natDegree

Tactic:
have hm : m + 1 = f.natDegree := tsub_add_cancel_of_le f_nat_degree_pos
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
⊢ coeff ((derivative : (a : R[X]) → R[X]) f) m = f.coeff (m + 1) * HAdd.hAdd (α := R) (↑m : R) 1

Tactic:
have h2 := coeff_derivative f m
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : coeff ((derivative : (a : R[X]) → R[X]) f) m = f.coeff (m + 1) * HAdd.hAdd (α := R) (↑m : R) 1
⊢ ∀ (n : ℕ), Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) f) n) (coeff 0 n)

Tactic:
rw [Polynomial.ext_iff] at h

Premises used: Polynomial.ext_iff
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : coeff ((derivative : (a : R[X]) → R[X]) f) m = f.coeff (m + 1) * HAdd.hAdd (α := R) (↑m : R) 1
h₁ : ∀ (n : ℕ), Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) f) n) (coeff 0 n)
⊢ f ≠ 0

Tactic:
rw [Polynomial.ext_iff] at h

Premises used: Polynomial.ext_iff
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : coeff ((derivative : (a : R[X]) → R[X]) f) m = f.coeff (m + 1) * HAdd.hAdd (α := R) (↑m : R) 1
h₁ : ∀ (n : ℕ), Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) f) n) (coeff 0 n)
hf₁ : f ≠ 0
⊢ 0 < f.natDegree

Tactic:
rw [Polynomial.ext_iff] at h

Premises used: Polynomial.ext_iff
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : coeff ((derivative : (a : R[X]) → R[X]) f) m = f.coeff (m + 1) * HAdd.hAdd (α := R) (↑m : R) 1
h₁ : ∀ (n : ℕ), Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) f) n) (coeff 0 n)
hf₁ : f ≠ 0
f_nat_degree_pos₁ : 0 < f.natDegree
⊢ let m := f.natDegree - 1;
  m + 1 = f.natDegree

Tactic:
rw [Polynomial.ext_iff] at h

Premises used: Polynomial.ext_iff
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : coeff ((derivative : (a : R[X]) → R[X]) f) m = f.coeff (m + 1) * HAdd.hAdd (α := R) (↑m : R) 1
h₁ : ∀ (n : ℕ), Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) f) n) (coeff 0 n)
hf₁ : f ≠ 0
f_nat_degree_pos₁ : 0 < f.natDegree
hm₁ :
  let m := f.natDegree - 1;
  m + 1 = f.natDegree
⊢ let m := f.natDegree - 1;
  coeff ((derivative : (a : R[X]) → R[X]) f) m = f.coeff (m + 1) * HAdd.hAdd (α := R) (↑m : R) 1

Tactic:
rw [Polynomial.ext_iff] at h

Premises used: Polynomial.ext_iff
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : ∀ (n : ℕ), Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) f) n) (coeff 0 n)
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : coeff ((derivative : (a : R[X]) → R[X]) f) m = f.coeff (m + 1) * HAdd.hAdd (α := R) (↑m : R) 1
⊢ m + 1 = 0 ∨ f.coeff (m + 1) = 0

Tactic:
rw [h m, coeff_zero, ← Nat.cast_add_one, ← nsmul_eq_mul', eq_comm, smul_eq_zero] at h2

Premises used: eq_comm, nsmul_eq_mul', Polynomial.coeff_zero, Nat.cast_add_one, smul_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : ∀ (n : ℕ), Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) f) n) (coeff 0 n)
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : m + 1 = 0 ∨ f.coeff (m + 1) = 0
⊢ f.coeff (m + 1) = 0

Tactic:
replace h2 := h2.resolve_left m.succ_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : ∀ (n : ℕ), Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) f) n) (coeff 0 n)
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : f.coeff (m + 1) = 0
⊢ f = 0

Tactic:
rw [hm, ← leadingCoeff, leadingCoeff_eq_zero] at h2

Premises used: Polynomial.leadingCoeff, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : ∀ (n : ℕ), Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) f) n) (coeff 0 n)
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : f = 0
⊢ False

Tactic:
hf h2
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : ∀ (n : ℕ), Eq.{u + 1} (α := R) (coeff ((derivative : (a : R[X]) → R[X]) f) n) (coeff 0 n)
hf : f ≠ 0
f_nat_degree_pos : 0 < f.natDegree
m : ℕ := f.natDegree - 1
hm : m + 1 = f.natDegree
h2 : f = 0
⊢ False

Tactic:
exact hf h2
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : IsAddTorsionFree R
f : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
⊢ f = (C : (a : R) → R[X]) (f.coeff 0)

Tactic:
eq_C_of_natDegree_eq_zero <| natDegree_eq_zero_of_derivative_eq_zero h

Premises used: Polynomial.natDegree_eq_zero_of_derivative_eq_zero, Polynomial.eq_C_of_natDegree_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
g p q : R[X]
h :
  (derivative : (a : R[X]) → R[X]) (p * g) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) g +
      HMul.hMul (β := R[X]) p ((derivative : (a : R[X]) → R[X]) g : R[X])
h_1 :
  (derivative : (a : R[X]) → R[X]) (q * g) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) g +
      HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) g : R[X])
⊢ (derivative : (a : R[X]) → R[X]) ((p + q) * g) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) (p + q) : R[X]) g +
      HMul.hMul (β := R[X]) (p + q) ((derivative : (a : R[X]) → R[X]) g : R[X])

Tactic:
simp only [add_mul, map_add, add_assoc, add_left_comm, *]

Premises used: add_mul, add_left_comm, add_assoc, map_add
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
g : R[X]
m : ℕ
a : R
⊢ (derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((monomial m : (a : R) → R[X]) a : R[X]) g) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial m : (a : R) → R[X]) a) : R[X]) g +
      HMul.hMul (α := R[X]) (β := R[X]) ((monomial m : (a : R) → R[X]) a : R[X])
        ((derivative : (a : R[X]) → R[X]) g : R[X])

Tactic:
?_
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
f g : R[X]
monomial :
  ∀ (m : ℕ) (a : R),
    (derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((Polynomial.monomial m : (a : R) → R[X]) a : R[X]) g) =
      HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((Polynomial.monomial m : (a : R) → R[X]) a) : R[X]) g +
        HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial m : (a : R) → R[X]) a : R[X])
          ((derivative : (a : R[X]) → R[X]) g : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (f * g) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g +
      HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X])

Tactic:
induction f using Polynomial.induction_on' with
  | add => simp only [add_mul, map_add, add_assoc, add_left_comm, *]
  | monomial m a => ?_

Premises used: add_mul, add_left_comm, add_assoc, map_add, Polynomial.monomial
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
m : ℕ
a : R
p q : R[X]
h :
  (derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((monomial m : (a : R) → R[X]) a : R[X]) p) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial m : (a : R) → R[X]) a) : R[X]) p +
      HMul.hMul (α := R[X]) (β := R[X]) ((monomial m : (a : R) → R[X]) a : R[X])
        ((derivative : (a : R[X]) → R[X]) p : R[X])
h_1 :
  (derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((monomial m : (a : R) → R[X]) a : R[X]) q) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial m : (a : R) → R[X]) a) : R[X]) q +
      HMul.hMul (α := R[X]) (β := R[X]) ((monomial m : (a : R) → R[X]) a : R[X])
        ((derivative : (a : R[X]) → R[X]) q : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((monomial m : (a : R) → R[X]) a : R[X]) (p + q)) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial m : (a : R) → R[X]) a) : R[X]) (p + q) +
      HMul.hMul (α := R[X]) (β := R[X]) ((monomial m : (a : R) → R[X]) a : R[X])
        ((derivative : (a : R[X]) → R[X]) (p + q) : R[X])

Tactic:
simp only [mul_add, map_add, add_assoc, add_left_comm, *]

Premises used: add_left_comm, add_assoc, map_add, mul_add
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
m : ℕ
a : R
n : ℕ
b : R
⊢ (derivative : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((monomial m : (a : R) → R[X]) a : R[X])
        ((monomial n : (a : R) → R[X]) b : R[X])) =
    HMul.hMul (α := R[X]) (β := R[X]) ((derivative : (a : R[X]) → R[X]) ((monomial m : (a : R) → R[X]) a) : R[X])
        ((monomial n : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((monomial m : (a : R) → R[X]) a : R[X])
        ((derivative : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) b) : R[X])

Tactic:
?_
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
g : R[X]
m : ℕ
a : R
monomial :
  ∀ (n : ℕ) (b : R),
    (derivative : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial m : (a : R) → R[X]) a : R[X])
          ((Polynomial.monomial n : (a : R) → R[X]) b : R[X])) =
      HMul.hMul (α := R[X]) (β := R[X])
          ((derivative : (a : R[X]) → R[X]) ((Polynomial.monomial m : (a : R) → R[X]) a) : R[X])
          ((Polynomial.monomial n : (a : R) → R[X]) b : R[X]) +
        HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial m : (a : R) → R[X]) a : R[X])
          ((derivative : (a : R[X]) → R[X]) ((Polynomial.monomial n : (a : R) → R[X]) b) : R[X])
⊢ (derivative : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((Polynomial.monomial m : (a : R) → R[X]) a : R[X]) g) =
    HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) ((Polynomial.monomial m : (a : R) → R[X]) a) : R[X]) g +
      HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial m : (a : R) → R[X]) a : R[X])
        ((derivative : (a : R[X]) → R[X]) g : R[X])

Tactic:
induction g using Polynomial.induction_on' with
  | add => simp only [mul_add, map_add, add_assoc, add_left_comm, *]
  | monomial n b => ?_

Premises used: add_left_comm, add_assoc, map_add, Polynomial.monomial, mul_add
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
m : ℕ
a : R
n : ℕ
b : R
monomial :
  (Polynomial.monomial (m + n - 1) : (a : R) → R[X]) (a * b * (↑(m + n) : R)) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((Polynomial.monomial (m - 1 + n) : (a : R) → R[X]) (a * (↑m : R) * b) : R[X])
      ((Polynomial.monomial (m + (n - 1)) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X])
⊢ (derivative : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial m : (a : R) → R[X]) a : R[X])
        ((Polynomial.monomial n : (a : R) → R[X]) b : R[X])) =
    HMul.hMul (α := R[X]) (β := R[X])
        ((derivative : (a : R[X]) → R[X]) ((Polynomial.monomial m : (a : R) → R[X]) a) : R[X])
        ((Polynomial.monomial n : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.monomial m : (a : R) → R[X]) a : R[X])
        ((derivative : (a : R[X]) → R[X]) ((Polynomial.monomial n : (a : R) → R[X]) b) : R[X])

Tactic:
simp only [monomial_mul_monomial, derivative_monomial]

Premises used: Polynomial.derivative_monomial, Polynomial.monomial_mul_monomial
-- 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 (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])
⊢ (Polynomial.monomial (m + n - 1) : (a : R) → R[X]) (a * b * (↑(m + n) : R)) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((Polynomial.monomial (m - 1 + n) : (a : R) → R[X]) (a * (↑m : R) * b) : R[X])
      ((Polynomial.monomial (m + (n - 1)) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X])

Tactic:
simp only [mul_assoc, (Nat.cast_commute _ _).eq, Nat.cast_add, mul_add, map_add]

Premises used: mul_assoc, map_add, Nat.cast_add, mul_add, Commute.eq, Nat.cast_commute
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
b : R
⊢ HAdd.hAdd (α := R[X]) (β := R[X]) ((monomial (0 + n - 1) : (a : R) → R[X]) (a * (b * (↑0 : R))) : R[X])
      ((monomial (0 + n - 1) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X])
      ((monomial (HSub.hSub (α := ℕ) 0 1 + n) : (a : R) → R[X]) (a * (b * (↑0 : R))) : R[X])
      ((monomial (0 + (n - 1)) : (a : R) → R[X]) (a * (b * (↑n : R))) : R[X])

Tactic:
simp only [zero_add, Nat.cast_zero, mul_zero, map_zero]

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

Tactic:
simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]

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

Tactic:
grind