awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
S : Finset R
k : ℕ
hk : k + 1 ≤ #S
ind :
  (⇑derivative : (a : R[X]) → R[X])^[k] (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    HMul.hMul (α := R[X]) (↑k ! : R[X])
      (∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
⊢ HAdd.hAdd (α := R[X]) (↑k : R[X]) 1 *
      ∑ T ∈ powersetCard (#S - (k + 1)) S,
        ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) =
    HMul.hMul (α := R[X]) (↑(k + 1) : R[X])
      (∑ T ∈ powersetCard (#S - (k + 1)) S,
        ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))

Tactic:
grind
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommRing R
k : ℕ
S : Finset R
hk : k ≤ #S
induction :
  ∀ (hk : 0 ≤ #S),
    (⇑derivative : (a : R[X]) → R[X])^[0]
        (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
      HMul.hMul (α := R[X]) (↑0! : R[X])
        (∑ T ∈ powersetCard (#S - 0) S, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
succ succ₁ :
  ∀ (n : ℕ),
    (∀ (hk : n ≤ #S),
        (⇑derivative : (a : R[X]) → R[X])^[n]
            (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
          HMul.hMul (α := R[X]) (↑n ! : R[X])
            (∑ T ∈ powersetCard (#S - n) S,
              ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))) →
      ∀ (hk : n + 1 ≤ #S),
        (⇑derivative : (a : R[X]) → R[X])^[n + 1]
            (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
          HMul.hMul (α := R[X]) (↑(n + 1)! : R[X])
            (∑ T ∈ powersetCard (#S - (n + 1)) S,
              ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
⊢ (⇑derivative : (a : R[X]) → R[X])^[k] (∏ a ∈ S, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
    HMul.hMul (α := R[X]) (↑k ! : R[X])
      (∑ T ∈ powersetCard (#S - k) S, ∏ a ∈ T, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))

Tactic:
classical
  induction k
  case zero => simp
  case succ k ind =>
    specialize ind (Nat.le_of_succ_le hk)
    nth_rewrite 1 [add_comm]
    rw [Function.iterate_add_apply, Function.iterate_one, ind, ← nsmul_eq_mul, derivative_smul,
      nsmul_eq_mul, derivative_sum, Nat.factorial_succ, mul_comm (k + 1), Nat.cast_mul, mul_assoc]
    congr 1
    calc
      ∑ T ∈ S.powersetCard (#S - k), derivative (∏ a ∈ T, (X - C a)) =
      ∑ T ∈ S.powersetCard (#S - k), ∑ i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        congr! with T hT
        simp_rw [derivative_prod_finset, derivative_X_sub_C, mul_one]
      _ = ∑ (T ∈ S.powersetCard (#S - k)) (i ∈ S) with i ∈ T, ∏ a ∈ T.erase i, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = ∑ (T ∈ S.powersetCard (#S - (k + 1))) (i ∈ S) with i ∉ T, ∏ a ∈ T, (X - C a) := by
        apply sum_bij' (fun ⟨T, i⟩ _ => ⟨T.erase i, i⟩) (fun ⟨T, i⟩ _ => ⟨insert i T, i⟩)
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        · intro r hr; dsimp at hr ⊢; congr 1; grind
        all_goals grind
      _ = ∑ T ∈ S.powersetCard (#S - (k + 1)), ∑ i ∈ S \ T, ∏ a ∈ T, (X - C a) := by
        rw [← sum_finset_product']
        grind
      _ = (k + 1) * ∑ T ∈ S.powersetCard (#S - (k + 1)), ∏ a ∈ T, (X - C a) := by
        rw [mul_sum]
        congr! 1 with T hT
        simp [sum_const, show #(S \ T) = k + 1 by grind]
      _ = _ := by grind

Premises used: Polynomial.derivative_sum, Polynomial.derivative_smul, Function.iterate_add_apply, Nat.factorial_succ, mul_assoc, HSub.hSub, add_comm, Nat.cast_mul, Function.iterate_one, HAdd.hAdd, Finset.powersetCard, mul_comm, Finset.card, nsmul_eq_mul, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
P : R[X]
h : P ∣ (derivative : (a : R[X]) → R[X]) P
pos : ∀ (hP : P = 0), Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
neg : ∀ (hP : ¬P = 0), Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])

Tactic:
by_cases hP : P = 0
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
P : R[X]
h : P ∣ (derivative : (a : R[X]) → R[X]) P
hP : P = 0
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])

Tactic:
simp only [hP, derivative_zero]

Premises used: Polynomial.derivative_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
P : R[X]
h : P ∣ (derivative : (a : R[X]) → R[X]) P
hP : ¬P = 0
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])

Tactic:
eq_zero_of_dvd_of_degree_lt h (degree_derivative_lt hP)

Premises used: Polynomial.degree_derivative_lt, Polynomial.eq_zero_of_dvd_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
P : R[X]
h : P ∣ (derivative : (a : R[X]) → R[X]) P
hP : ¬P = 0
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])

Tactic:
exact eq_zero_of_dvd_of_degree_lt h (degree_derivative_lt hP)

Premises used: Polynomial.degree_derivative_lt, Polynomial.eq_zero_of_dvd_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
P : R[X]
h : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) P : R[X]) (0 : R[X])
⊢ P ∣ (derivative : (a : R[X]) → R[X]) P

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
n : ℕ
chn : Ne.{u + 1} (α := R) (↑n : R) 0
a : R[X]
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
n : ℕ
chn : Ne.{u + 1} (α := R) (↑n : R) 0
a : R[X]
inst_2 : Nontrivial R
rw :
  ∀ (chn : Ne.{u + 1} (α := R[X]) (↑n : R[X]) 0) {a : R[X]},
    Nontrivial R →
      (Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (a ^ n) : R[X]) (0 : R[X]) ↔
        Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X]))
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (a ^ n) : R[X]) (0 : R[X]) ↔
    Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X])

Tactic:
rw [← C_ne_zero, C_eq_natCast] at chn

Premises used: Polynomial.C_eq_natCast, Polynomial.C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Derivative
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
n : ℕ
chn : Ne.{u + 1} (α := R[X]) (↑n : R[X]) 0
a : R[X]
inst_2 : Nontrivial R
⊢ Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) (a ^ n) : R[X]) (0 : R[X]) ↔
    Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) (0 : R[X])

Tactic:
simp +contextual [derivative_pow, chn]

Premises used: Polynomial.derivative_pow
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
f : R[X]
h : X ∣ f
g : R[X]
hfg : f = X * g
rw : (X * g).coeff 0 = 0
rw₁ rw₂ : Eq.{u + 1} (α := R) 0 0
⊢ f.coeff 0 = 0

Tactic:
rw [hfg, coeff_X_mul_zero]

Premises used: Polynomial.coeff_X_mul_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
f : R[X]
hf : f.coeff 0 = 0
rw : f = X * f.divX + 0
rw₁ : f = X * f.divX + (C : (a : R) → R[X]) 0
rw₂ : f = HAdd.hAdd (β := R[X]) (X * f.divX) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
rw₃ rw₄ : f = f
⊢ f = X * f.divX

Tactic:
rw [← add_zero (X * f.divX), ← C_0, ← hf, X_mul_divX_add]

Premises used: HMul.hMul, Polynomial.C_0, Polynomial.X_mul_divX_add, Polynomial.divX, add_zero, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
h : HPow.hPow (α := R[X]) X n ∣ f
d : ℕ
hd : d < n
g : R[X]
hgf : f = HPow.hPow (α := R[X]) X n * g
⊢ f.coeff d = 0

Tactic:
simp only [hgf, coeff_X_pow_mul', ite_eq_right_iff, not_le_of_gt hd, IsEmpty.forall_iff]

Premises used: Polynomial.coeff_X_pow_mul', ite_eq_right_iff, not_le_of_gt, IsEmpty.forall_iff
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
f : R[X]
hd : ∀ d < 0, f.coeff d = 0
⊢ HPow.hPow (α := R[X]) (β := ℕ) X 0 ∣ f

Tactic:
simp [pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : ∀ (hd : ∀ d < n, f.coeff d = 0), HPow.hPow (α := R[X]) X n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
succ : ∀ (g : R[X]) (hgf : f = HPow.hPow (α := R[X]) X n * g), HPow.hPow (α := R[X]) X (n + 1) ∣ f
⊢ HPow.hPow (α := R[X]) X (n + 1) ∣ f

Tactic:
obtain ⟨g, hgf⟩ := hn fun d : ℕ => fun H : d < n => hd _ (Nat.lt_succ_of_lt H)

Premises used: Nat.lt_succ_of_lt
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : ∀ (hd : ∀ d < n, f.coeff d = 0), HPow.hPow (α := R[X]) X n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = HPow.hPow (α := R[X]) X n * g
⊢ (HPow.hPow (α := R[X]) X n * g).coeff (0 + n) = g.coeff 0

Tactic:
have := coeff_X_pow_mul g n 0
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : ∀ (hd : ∀ d < n, f.coeff d = 0), HPow.hPow (α := R[X]) X n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = HPow.hPow (α := R[X]) X n * g
this : (HPow.hPow (α := R[X]) X n * g).coeff (0 + n) = g.coeff 0
⊢ 0 = g.coeff 0

Tactic:
rw [zero_add, ← hgf, hd n (Nat.lt_succ_self n)] at this

Premises used: Nat.lt_succ_self, zero_add
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : ∀ (hd : ∀ d < n, f.coeff d = 0), HPow.hPow (α := R[X]) X n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = HPow.hPow (α := R[X]) X n * g
this : 0 = g.coeff 0
succ : ∀ (k : R[X]) (hgk : g = X * k), HPow.hPow (α := R[X]) X (n + 1) ∣ f
⊢ HPow.hPow (α := R[X]) X (n + 1) ∣ f

Tactic:
obtain ⟨k, hgk⟩ := Polynomial.X_dvd_iff.mpr this.symm

Premises used: Iff.mpr, Polynomial.X_dvd_iff, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : ∀ (hd : ∀ d < n, f.coeff d = 0), HPow.hPow (α := R[X]) X n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = HPow.hPow (α := R[X]) X n * g
this : 0 = g.coeff 0
k : R[X]
hgk : g = X * k
h : f = HPow.hPow (α := R[X]) X (n + 1) * k
⊢ HPow.hPow (α := R[X]) X (n + 1) ∣ f

Tactic:
use k
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hn : ∀ (hd : ∀ d < n, f.coeff d = 0), HPow.hPow (α := R[X]) X n ∣ f
hd : ∀ d < n + 1, f.coeff d = 0
g : R[X]
hgf : f = HPow.hPow (α := R[X]) X n * g
this : 0 = g.coeff 0
k : R[X]
hgk : g = X * k
h : f = HPow.hPow (α := R[X]) X n * X * k
h₁ : f = HPow.hPow (α := R[X]) X n * (X * k)
h₂ h₃ h₄ h₅ : f = HPow.hPow (α := R[X]) X n * g
⊢ f = HPow.hPow (α := R[X]) X (n + 1) * k

Tactic:
rwa [pow_succ, mul_assoc, ← hgk]

Premises used: pow_succ, mul_assoc
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
f : R[X]
n : ℕ
hd : ∀ d < n, f.coeff d = 0
zero : ∀ (hd : ∀ d < 0, f.coeff d = 0), HPow.hPow (α := R[X]) (β := ℕ) X 0 ∣ f
succ :
  ∀ (n : ℕ) (hn : ∀ (hd : ∀ d < n, f.coeff d = 0), HPow.hPow (α := R[X]) X n ∣ f) (hd : ∀ d < n + 1, f.coeff d = 0),
    HPow.hPow (α := R[X]) X (n + 1) ∣ f
⊢ HPow.hPow (α := R[X]) X n ∣ f

Tactic:
induction n with
    | zero => simp [pow_zero]
    | succ n hn =>
      obtain ⟨g, hgf⟩ := hn fun d : ℕ => fun H : d < n => hd _ (Nat.lt_succ_of_lt H)
      have := coeff_X_pow_mul g n 0
      rw [zero_add, ← hgf, hd n (Nat.lt_succ_self n)] at this
      obtain ⟨k, hgk⟩ := Polynomial.X_dvd_iff.mpr this.symm
      use k
      rwa [pow_succ, mul_assoc, ← hgk]

Premises used: pow_succ, mul_assoc, zero_add, pow_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p = 0
⊢ False

Tactic:
simp [hp0] at hp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
⊢ p ≠ 0

Tactic:
have hp0 : p ≠ 0 := fun hp0 => by simp [hp0] at hp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r = 0
⊢ q = p ^ (q.natDegree + 1) * 0

Tactic:
subst hr0
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
hp0 : p ≠ 0
hr : q = p ^ (q.natDegree + 1) * 0
⊢ False

Tactic:
simp [hq] at hr
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
⊢ r ≠ 0

Tactic:
have hr0 : r ≠ 0 := fun hr0 => by subst hr0; simp [hq] at hr
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
⊢ p.leadingCoeff ^ (q.natDegree + 1) = 1

Tactic:
have hpn1 : leadingCoeff p ^ (natDegree q + 1) = 1 := by simp [show _ = _ from hmp]
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
⊢ p.leadingCoeff ^ (q.natDegree + 1) ≠ 0

Tactic:
have hpn0' : leadingCoeff p ^ (natDegree q + 1) ≠ 0 := hpn1.symm ▸ zn0.symm
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
⊢ (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0

Tactic:
simp only [leadingCoeff_pow' hpn0', leadingCoeff_eq_zero, hpn1, one_mul, Ne,
          hr0, not_false_eq_true]

Premises used: Ne, Polynomial.leadingCoeff_pow', not_false_eq_true, Polynomial.leadingCoeff_eq_zero, one_mul
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
⊢ (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0

Tactic:
have hpnr0 : leadingCoeff (p ^ (natDegree q + 1)) * leadingCoeff r ≠ 0 := by
      simp only [leadingCoeff_pow' hpn0', leadingCoeff_eq_zero, hpn1, one_mul, Ne,
          hr0, not_false_eq_true]
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
rw : (↑0 : WithBot ℕ) < p.degree
⊢ LT.lt (α := WithBot ℕ) (↑0 : WithBot ℕ) (↑p.natDegree : WithBot ℕ)

Tactic:
rw [← degree_eq_natDegree hp0]

Premises used: Polynomial.degree_eq_natDegree
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
⊢ (↑0 : WithBot ℕ) < p.degree

Tactic:
hp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
⊢ (↑0 : WithBot ℕ) < p.degree

Tactic:
exact hp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
⊢ 0 < p.natDegree

Tactic:
have hnp : 0 < natDegree p := Nat.cast_lt.1 <| by
      rw [← degree_eq_natDegree hp0]; exact hp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
hnp : 0 < p.natDegree
⊢ q.natDegree = (p ^ (q.natDegree + 1) * r).natDegree

Tactic:
have := congr_arg natDegree hr
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
hnp : 0 < p.natDegree
this : q.natDegree = (p ^ (q.natDegree + 1) * r).natDegree
⊢ q.natDegree = q.natDegree * p.natDegree + (1 * p.natDegree + r.natDegree)

Tactic:
rw [natDegree_mul' hpnr0, natDegree_pow' hpn0', add_mul, add_assoc] at this

Premises used: add_mul, add_assoc, Polynomial.natDegree_mul', Polynomial.natDegree_pow'
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
hnp : 0 < p.natDegree
this : q.natDegree = q.natDegree * p.natDegree + (1 * p.natDegree + r.natDegree)
rwa rwa₁ rwa₂ rwa₃ : 0 < p.natDegree
⊢ 0 < 1 * p.natDegree

Tactic:
rwa [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : Ne.{u + 1} (α := R) 0 1
h : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
hpnr0 : (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0
hnp : 0 < p.natDegree
this : q.natDegree = q.natDegree * p.natDegree + (1 * p.natDegree + r.natDegree)
⊢ False

Tactic:
exact
      ne_of_lt
        (lt_add_of_le_of_pos (le_mul_of_one_le_right (Nat.zero_le _) hnp)
          (add_pos_of_pos_of_nonneg (by rwa [one_mul]) (Nat.zero_le _)))
        this

Premises used: Nat.zero_le, le_mul_of_one_le_right, lt_add_of_le_of_pos, ne_of_lt, add_pos_of_pos_of_nonneg
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
obtain :
  ∀ (r : R[X]) (hdeg : (p * r).natDegree ≤ p.natDegree),
    p * r = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (p * r).leadingCoeff : R[X])
⊢ q = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) q.leadingCoeff : R[X])

Tactic:
obtain ⟨r, rfl⟩ := hdvd

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
inl :
  ∀ (hdeg : (p * 0).natDegree ≤ p.natDegree),
    p * 0 = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (p * 0).leadingCoeff : R[X])
inr : ∀ (hr : r ≠ 0), p * r = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (p * r).leadingCoeff : R[X])
⊢ p * r = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (p * r).leadingCoeff : R[X])

Tactic:
obtain rfl | hr := eq_or_ne r 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
hdeg : (p * 0).natDegree ≤ p.natDegree
⊢ p * 0 = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (p * 0).leadingCoeff : R[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : r ≠ 0
⊢ r.natDegree = 0

Tactic:
simpa [hp.natDegree_mul' hr] using hdeg

Premises used: Polynomial.Monic.natDegree_mul'
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : r ≠ 0
⊢ r.natDegree = 0

Tactic:
have : r.natDegree = 0 := by simpa [hp.natDegree_mul' hr] using hdeg
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : r ≠ 0
this : r.natDegree = 0
inr :
  HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (r.coeff 0) : R[X]) =
    HMul.hMul (β := R[X]) p
      ((C : (a : R) → R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (r.coeff 0) : R[X])).leadingCoeff : R[X])
⊢ p * r = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (p * r).leadingCoeff : R[X])

Tactic:
rw [eq_C_of_natDegree_eq_zero this]

Premises used: Polynomial.eq_C_of_natDegree_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
hdeg : (p * r).natDegree ≤ p.natDegree
hr : r ≠ 0
this : r.natDegree = 0
⊢ HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (r.coeff 0) : R[X]) =
    HMul.hMul (β := R[X]) p
      ((C : (a : R) → R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (r.coeff 0) : R[X])).leadingCoeff : R[X])

Tactic:
simp [leadingCoeff_monic_mul hp]

Premises used: Polynomial.leadingCoeff_monic_mul
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
rw : HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) q.leadingCoeff : R[X]) = p
⊢ q = p

Tactic:
rw [eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le hp hdvd hdeg]

Premises used: Polynomial.eq_mul_leadingCoeff_of_monic_of_dvd_of_natDegree_le
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
hdvd : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) q.leadingCoeff : R[X]) = p

Tactic:
simp [hq]
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
rw : q.degree ≤ p.degree
⊢ LE.le (α := WithBot ℕ) (↑q.natDegree : WithBot ℕ) (↑p.natDegree : WithBot ℕ)

Tactic:
rw [← degree_eq_natDegree h.2, ← degree_eq_natDegree hq0]

Premises used: Polynomial.degree_eq_natDegree, And.right
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
⊢ q.degree ≤ p.degree

Tactic:
h.1

Premises used: And.left