awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
inr :
  ∀
    (this :
      ∀ (n : ℕ) (h : p.natDegree ≤ n),
        (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
          ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i)
    (h : ¬p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
wlog :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
    ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

Tactic:
wlog h : p.natDegree ≤ n generalizing n

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
    ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

Tactic:
Nat.decreasingInduction' (fun n hn _ ih ↦ ?_) (le_of_not_ge h) ?_

Premises used: Nat.decreasingInduction', le_of_not_ge
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n
inr :
  ∀ (n_1 : ℕ) (hn : n_1 < p.natDegree),
    n ≤ n_1 →
      ∀
        (ih :
          (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n_1 + 1) =
            ∑ i ∈ Icc (n_1 + 1 + 1) p.natDegree, a ^ (i - (n_1 + 1 + 1)) * p.coeff i),
        (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n_1 =
          ∑ i ∈ Icc (n_1 + 1) p.natDegree, a ^ (i - (n_1 + 1)) * p.coeff i
inr₁ :
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff p.natDegree =
    ∑ i ∈ Icc (p.natDegree + 1) p.natDegree, a ^ (i - (p.natDegree + 1)) * p.coeff i
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
    ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

Tactic:
refine Nat.decreasingInduction' (fun n hn _ ih ↦ ?_) (le_of_not_ge h) ?_
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n_1 : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n_1
n : ℕ
hn : n < p.natDegree
h_1 : n_1 ≤ n
ih :
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1) =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
inr :
  p.coeff n.succ + ∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x =
    p.coeff (n + 1) + ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a * (a ^ (i - (n + 1 + 1)) * p.coeff i)
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
    ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

Tactic:
rw [coeff_divByMonic_X_sub_C_rec, ih, eq_comm, Icc_eq_cons_Ioc (Nat.succ_le_iff.mpr hn),
          sum_cons, Nat.sub_self, pow_zero, one_mul, mul_sum]

Premises used: Iff.mpr, Finset.mul_sum, Finset.sum_cons, Polynomial.coeff_divByMonic_X_sub_C_rec, Finset.Icc_eq_cons_Ioc, eq_comm, pow_zero, Nat.sub_self, Nat.succ_le_iff, one_mul
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n_1 : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n_1
n : ℕ
hn : n < p.natDegree
h_1 : n_1 ≤ n
ih :
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1) =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
inr :
  Eq.{u + 1} (α := R) (∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x)
    (∑ i ∈ Icc (n + 1 + 1) p.natDegree, a * (a ^ (i - (n + 1 + 1)) * p.coeff i))
⊢ p.coeff n.succ + ∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x =
    p.coeff (n + 1) + ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a * (a ^ (i - (n + 1 + 1)) * p.coeff i)

Tactic:
congr 1
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n_1 : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n_1
n : ℕ
hn : n < p.natDegree
h_1 : n_1 ≤ n
ih :
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1) =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
⊢ Eq.{u + 1} (α := R) (∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x)
    (∑ i ∈ Icc (n + 1 + 1) p.natDegree, a * (a ^ (i - (n + 1 + 1)) * p.coeff i))

Tactic:
sum_congr ?_ fun i hi ↦ ?_

Premises used: Finset.sum_congr
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n_1 : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n_1
n : ℕ
hn : n < p.natDegree
h_1 : n_1 ≤ n
ih :
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1) =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
inr : Ioc n.succ p.natDegree = Icc (n + 1 + 1) p.natDegree
inr₁ :
  ∀ (i : ℕ) (hi : i ∈ Icc (n + 1 + 1) p.natDegree),
    a ^ (i - (n + 1)) * p.coeff i = a * (a ^ (i - (n + 1 + 1)) * p.coeff i)
⊢ Eq.{u + 1} (α := R) (∑ x ∈ Ioc n.succ p.natDegree, a ^ (x - (n + 1)) * p.coeff x)
    (∑ i ∈ Icc (n + 1 + 1) p.natDegree, a * (a ^ (i - (n + 1 + 1)) * p.coeff i))

Tactic:
refine sum_congr ?_ fun i hi ↦ ?_

Premises used: Finset.sum_congr
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n_1 : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n_1
n : ℕ
hn : n < p.natDegree
h_1 : n_1 ≤ n
ih :
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1) =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
inr : ∀ (a : ℕ), a ∈ Ioc n.succ p.natDegree ↔ a ∈ Icc (n + 1 + 1) p.natDegree
⊢ Ioc n.succ p.natDegree = Icc (n + 1 + 1) p.natDegree

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n_1 : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n_1
n : ℕ
hn : n < p.natDegree
h_1 : n_1 ≤ n
ih :
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1) =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
a_1 : ℕ
⊢ a_1 ∈ Ioc n.succ p.natDegree ↔ a_1 ∈ Icc (n + 1 + 1) p.natDegree

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n_1 : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n_1
n : ℕ
hn : n < p.natDegree
h_1 : n_1 ≤ n
ih :
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1) =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
inr : 1 ≤ i - (n + 1)
⊢ a ^ (i - (n + 1)) * p.coeff i = a * (a ^ (i - (n + 1 + 1)) * p.coeff i)

Tactic:
rw [← mul_assoc, ← pow_succ', eq_comm, i.sub_succ', Nat.sub_add_cancel]

Premises used: Nat.sub_succ', mul_assoc, eq_comm, Nat.sub_add_cancel, pow_succ'
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n_1 : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n_1
n : ℕ
hn : n < p.natDegree
h_1 : n_1 ≤ n
ih :
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1) =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
inr : 1 + (n + 1) ≤ i
⊢ 1 ≤ i - (n + 1)

Tactic:
apply Nat.le_sub_of_add_le

Premises used: Nat.le_sub_of_add_le
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n_1 : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n_1
n : ℕ
hn : n < p.natDegree
h_1 : n_1 ≤ n
ih :
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1) =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
inr : n + 1 + 1 ≤ i
⊢ 1 + (n + 1) ≤ i

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n_1 : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n_1
n : ℕ
hn : n < p.natDegree
h_1 : n_1 ≤ n
ih :
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1) =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ n + 1 + 1 ≤ i

Tactic:
(mem_Icc.mp hi).1

Premises used: Finset.mem_Icc, And.left, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n_1 : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n_1
n : ℕ
hn : n < p.natDegree
h_1 : n_1 ≤ n
ih :
  (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff (n + 1) =
    ∑ i ∈ Icc (n + 1 + 1) p.natDegree, a ^ (i - (n + 1 + 1)) * p.coeff i
i : ℕ
hi : i ∈ Icc (n + 1 + 1) p.natDegree
⊢ n + 1 + 1 ≤ i

Tactic:
exact (mem_Icc.mp hi).1

Premises used: Finset.mem_Icc, And.left, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff p.natDegree =
    ∑ i ∈ Icc (p.natDegree + 1) p.natDegree, a ^ (i - (p.natDegree + 1)) * p.coeff i

Tactic:
this _ le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
this :
  ∀ (n : ℕ) (h : p.natDegree ≤ n),
    (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
      ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i
h : ¬p.natDegree ≤ n
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff p.natDegree =
    ∑ i ∈ Icc (p.natDegree + 1) p.natDegree, a ^ (i - (p.natDegree + 1)) * p.coeff i

Tactic:
exact this _ le_rfl

Premises used: le_rfl
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
rw : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n = 0
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n =
    ∑ i ∈ Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

Tactic:
rw [Icc_eq_empty (Nat.lt_succ_iff.mpr h).not_ge, sum_empty]

Premises used: Iff.mpr, Nat.lt_succ_iff, Finset.Icc_eq_empty, Finset.sum_empty, LT.lt.not_ge
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
h_1 : Nontrivial R
pos : ∀ (hp : p.natDegree = 0), (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n = 0
neg : ∀ (hp : ¬p.natDegree = 0), (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n = 0
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n = 0

Tactic:
by_cases hp : p.natDegree = 0

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
h_1 : Nontrivial R
hp : p.natDegree = 0
pos : p.degree < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n = 0

Tactic:
rw [(divByMonic_eq_zero_iff <| monic_X_sub_C a).mpr, coeff_zero]

Premises used: Iff.mpr, Polynomial.monic_X_sub_C, Polynomial.divByMonic_eq_zero_iff, Polynomial.coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
h_1 : Nontrivial R
hp : p.natDegree = 0
pos : p.natDegree < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree
⊢ p.degree < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree

Tactic:
apply degree_lt_degree

Premises used: Polynomial.degree_lt_degree
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
h_1 : Nontrivial R
hp : p.natDegree = 0
pos : LT.lt (α := ℕ) 0 1
⊢ p.natDegree < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree

Tactic:
rw [hp, natDegree_X_sub_C]

Premises used: Polynomial.natDegree_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
h_1 : Nontrivial R
hp : p.natDegree = 0
⊢ LT.lt (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
h_1 : Nontrivial R
hp : ¬p.natDegree = 0
neg : (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree < n
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).coeff n = 0

Tactic:
apply coeff_eq_zero_of_natDegree_lt

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
h_1 : Nontrivial R
hp : ¬p.natDegree = 0
neg : p.natDegree - 1 < n
⊢ (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).natDegree < n

Tactic:
rw [natDegree_divByMonic p (monic_X_sub_C a), natDegree_X_sub_C]

Premises used: Polynomial.monic_X_sub_C, Polynomial.natDegree_divByMonic, Polynomial.natDegree_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
h_1 : Nontrivial R
hp : ¬p.natDegree = 0
⊢ p.natDegree - 1 < n

Tactic:
(Nat.pred_lt hp).trans_le h

Premises used: LT.lt.trans_le, Nat.pred_lt, WithBot.recBotCoe, Polynomial.natDegree, Nat.pred, WithBot.unbotD
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
n : ℕ
h : p.natDegree ≤ n
h_1 : Nontrivial R
hp : ¬p.natDegree = 0
⊢ p.natDegree - 1 < n

Tactic:
exact (Nat.pred_lt hp).trans_le h

Premises used: LT.lt.trans_le, Nat.pred_lt
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
h_1 : Nontrivial R
h : IsField.{u} R[X]
this : Field R[X] := h.toField
⊢ False

Tactic:
simpa using congr_arg natDegree (monic_X.eq_one_of_isUnit <| monic_X (R := R).ne_zero.isUnit)

Premises used: Ne.isUnit, congr_arg, Polynomial.natDegree, Polynomial.Monic.eq_one_of_isUnit, Polynomial.monic_X, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
h0 : p ≠ 0
⊢ Nontrivial R

Tactic:
haveI := Nontrivial.of_polynomial_ne h0
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ FiniteMultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p

Tactic:
finiteMultiplicity_of_degree_pos_of_monic ?_ (monic_X_sub_C _) h0

Premises used: Polynomial.monic_X_sub_C, Polynomial.finiteMultiplicity_of_degree_pos_of_monic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
refine : 0 < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree
⊢ FiniteMultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p

Tactic:
refine finiteMultiplicity_of_degree_pos_of_monic ?_ (monic_X_sub_C _) h0

Premises used: Polynomial.monic_X_sub_C, Polynomial.finiteMultiplicity_of_degree_pos_of_monic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
rw : LT.lt (α := WithBot ℕ) 0 1
⊢ 0 < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree

Tactic:
rw [degree_X_sub_C]

Premises used: Polynomial.degree_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
h0 : p ≠ 0
this : Nontrivial R
⊢ LT.lt (α := WithBot ℕ) 0 1

Tactic:
decide
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
p0 : p ≠ 0
a : R
inst_1 : DecidablePred fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p
rw :
  Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) ⋯
⊢ (if h0 : p = 0 then 0
    else
      Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
        ⋯) =
    Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) ⋯

Tactic:
rw [dif_neg p0]

Premises used: dif_neg
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
p0 : p ≠ 0
a : R
inst_1 : DecidablePred fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p
⊢ Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) ⋯

Tactic:
congr
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : DecidableEq R
p : R[X]
a : R
simp :
  Eq (α := ℕ)
    (if h : p = 0 then 0
    else
      Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
        ⋯)
    (if p = 0 then 0
    else
      WithTop.untopD 1
        (if h : FiniteMultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p then
          (↑(Nat.find (p := fun (n : ℕ) ↦
                ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) h) :
            ℕ∞)
        else ⊤))
⊢ rootMultiplicity a p =
    if p = 0 then 0 else multiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p

Tactic:
simp only [rootMultiplicity, multiplicity, emultiplicity]

Premises used: multiplicity, Polynomial.rootMultiplicity, emultiplicity
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : DecidableEq R
p : R[X]
a : R
isTrue : p = 0 → Eq (α := ℕ) 0 0
isFalse :
  ∀ (h : ¬p = 0),
    Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) ⋯ =
      WithTop.untopD 1
        (if h : FiniteMultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p then
          (↑(Nat.find (p := fun (n : ℕ) ↦
                ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) h) :
            ℕ∞)
        else ⊤)
⊢ Eq (α := ℕ)
    (if h : p = 0 then 0
    else
      Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
        ⋯)
    (if p = 0 then 0
    else
      WithTop.untopD 1
        (if h : FiniteMultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p then
          (↑(Nat.find (p := fun (n : ℕ) ↦
                ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) h) :
            ℕ∞)
        else ⊤))

Tactic:
split
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : DecidableEq R
p : R[X]
a : R
h : p = 0
⊢ Eq (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : DecidableEq R
p : R[X]
a : R
h : ¬p = 0
isFalse :
  Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) ⋯ =
    WithTop.untopD 1
      (↑(Nat.find (p := fun (n : ℕ) ↦
            ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) ⋯) :
        ℕ∞)
⊢ Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) ⋯ =
    WithTop.untopD 1
      (if h : FiniteMultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) p then
        (↑(Nat.find (p := fun (n : ℕ) ↦
              ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) h) :
          ℕ∞)
      else ⊤)

Tactic:
simp only [finiteMultiplicity_X_sub_C a h, ↓reduceDIte]

Premises used: reduceDIte, Polynomial.finiteMultiplicity_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : DecidableEq R
p : R[X]
a : R
h : ¬p = 0
⊢ Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) ⋯ =
    Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p) ⋯

Tactic:
congr
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
x : R
⊢ rootMultiplicity x 0 = 0

Tactic:
dif_pos rfl

Premises used: dif_pos, Polynomial.rootMultiplicity, rfl
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
r a : R
inl : Subsingleton R → rootMultiplicity a ((C : (a : R) → R[X]) r) = 0
inr : Nontrivial R → rootMultiplicity a ((C : (a : R) → R[X]) r) = 0
⊢ rootMultiplicity a ((C : (a : R) → R[X]) r) = 0

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
r a : R
h : Subsingleton R
inl : rootMultiplicity a 0 = 0
inl₁ inl₂ : Eq (α := ℕ) 0 0
⊢ rootMultiplicity a ((C : (a : R) → R[X]) r) = 0

Tactic:
rw [Subsingleton.elim (C r) 0, rootMultiplicity_zero]

Premises used: Polynomial.C, Polynomial.rootMultiplicity_zero, Subsingleton.elim, OfNat.ofNat, DFunLike.coe