awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
mul_eq :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m *
      (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) =
    p
inr :
  let g := p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m;
  ∀ (mul_eq : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g = p),
    eval t g = (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff
⊢ eval t (p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m) =
    (p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).trailingCoeff

Tactic:
set g := p /ₘ (X - C t) ^ m

Premises used: Polynomial.C, HSub.hSub, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m
mul_eq : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g = p
rw : eval 0 (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))) = eval t g
rw₁ : eval (eval 0 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))) g = eval t g
rw₂ : eval (HAdd.hAdd (α := R) (eval 0 X) (eval 0 ((C : (a : R) → R[X]) t))) g = eval t g
rw₃ : eval (HAdd.hAdd (α := R) 0 (eval 0 ((C : (a : R) → R[X]) t))) g = eval t g
rw₄ : eval (0 + t) g = eval t g
rw₅ rw₆ : eval t g = eval t g
⊢ (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).coeff 0 = eval t g

Tactic:
rw [coeff_zero_eq_eval_zero, eval_comp, eval_add, eval_X, eval_C, zero_add]

Premises used: Polynomial.coeff_zero_eq_eval_zero, Polynomial.eval_C, Polynomial.eval_X, zero_add, Polynomial.eval_comp, Polynomial.eval_add
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m
mul_eq : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g = p
⊢ (g.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))).coeff 0 = eval t g

Tactic:
have : (g.comp (X + C t)).coeff 0 = g.eval t := by
    rw [coeff_zero_eq_eval_zero, eval_comp, eval_add, eval_X, eval_C, zero_add]
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
simp_rw :
  (∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
⊢ n ≤ rootMultiplicity a p ↔ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p

Tactic:
simp_rw [rootMultiplicity, dif_neg p0, Nat.le_find_iff, not_not]

Premises used: Classical.not_not, Nat.le_find_iff, dif_neg, Polynomial.rootMultiplicity
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ (∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p

Tactic:
⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩

Premises used: Polynomial.C, pow_dvd_pow, HSub.hSub, Iff.intro, Polynomial.X, DFunLike.coe, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
refine :
  ∀ (h : ∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p),
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
⊢ (∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p

Tactic:
refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p
zero :
  ∀ (h : ∀ m < 0, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p),
    HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) 0 ∣ p
succ :
  ∀ (n : ℕ) (h : ∀ m < n + 1, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p),
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p

Tactic:
rcases n with - | n
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
h : ∀ m < 0, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p
⊢ 1 ∣ p

Tactic:
apply one_dvd

Premises used: one_dvd
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ m < n + 1, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p

Tactic:
h n n.lt_succ_self

Premises used: Nat.lt_succ_self
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
h : ∀ m < n + 1, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p

Tactic:
exact h n n.lt_succ_self

Premises used: Nat.lt_succ_self
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
simp_rw :
  (n ≤
      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)
          ⋯) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₁ :
  n ≤
      Nat.find (p := fun (n : ℕ) ↦ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p)
        ⋯ ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₂ :
  (∀ m < n, ¬¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₃ :
  (∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p) ↔
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
simp_rw₄ :
  ∀ (h : ∀ m < n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p),
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p
zero :
  ∀ (h : ∀ m < 0, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p),
    HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) 0 ∣ p
succ succ₁ :
  ∀ (n : ℕ) (h : ∀ m < n + 1, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (m + 1) ∣ p),
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p
⊢ n ≤ rootMultiplicity a p ↔ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ n ∣ p

Tactic:
classical
  simp_rw [rootMultiplicity, dif_neg p0, Nat.le_find_iff, not_not]
  refine ⟨fun h => ?_, fun h m hm => (pow_dvd_pow _ hm).trans h⟩
  rcases n with - | n
  · rw [pow_zero]
    apply one_dvd
  · exact h n n.lt_succ_self

Premises used: Classical.not_not, Nat.le_find_iff, dif_neg, pow_zero, one_dvd, Polynomial.rootMultiplicity
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
rw : rootMultiplicity a p ≤ n ↔ ¬n + 1 ≤ rootMultiplicity a p
rw₁ : rootMultiplicity a p ≤ n ↔ rootMultiplicity a p < n + 1
rw₂ rw₃ : rootMultiplicity a p ≤ n ↔ rootMultiplicity a p ≤ n
⊢ rootMultiplicity a p ≤ n ↔ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (n + 1) ∣ p

Tactic:
rw [← (le_rootMultiplicity_iff p0).not, not_le, Nat.lt_add_one_iff]

Premises used: not_le, Nat.lt_add_one_iff, Iff.not, Polynomial.le_rootMultiplicity_iff
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
rw :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
      min (rootMultiplicity a p) (rootMultiplicity a q) ∣
    p + q
⊢ min (rootMultiplicity a p) (rootMultiplicity a q) ≤ rootMultiplicity a (p + q)

Tactic:
rw [le_rootMultiplicity_iff hzero]

Premises used: Polynomial.le_rootMultiplicity_iff
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
      min (rootMultiplicity a p) (rootMultiplicity a q) ∣
    p + q

Tactic:
min_pow_dvd_add (pow_rootMultiplicity_dvd p a) (pow_rootMultiplicity_dvd q a)

Premises used: Polynomial.pow_rootMultiplicity_dvd, min_pow_dvd_add
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
a : R
hzero : p + q ≠ 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^
      min (rootMultiplicity a p) (rootMultiplicity a q) ∣
    p + q

Tactic:
exact min_pow_dvd_add (pow_rootMultiplicity_dvd p a) (pow_rootMultiplicity_dvd q a)

Premises used: Polynomial.pow_rootMultiplicity_dvd, min_pow_dvd_add
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
rw :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x p *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x q ∣
    p * q
⊢ rootMultiplicity x p + rootMultiplicity x q ≤ rootMultiplicity x (p * q)

Tactic:
rw [le_rootMultiplicity_iff hpq, pow_add]

Premises used: pow_add, Polynomial.le_rootMultiplicity_iff
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
a : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x p ∣ p
a₁ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x q ∣ q
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x p *
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x q ∣
    p * q

Tactic:
gcongr
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x p ∣ p

Tactic:
apply pow_rootMultiplicity_dvd

Premises used: Polynomial.pow_rootMultiplicity_dvd
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ^ rootMultiplicity x q ∣ q

Tactic:
apply pow_rootMultiplicity_dvd

Premises used: Polynomial.pow_rootMultiplicity_dvd
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hq : q ≠ 0
hpq : p ∣ q
x : R
obtain : ∀ (w : R[X]) (hq : p * w ≠ 0), rootMultiplicity x p ≤ rootMultiplicity x (p * w)
⊢ rootMultiplicity x p ≤ rootMultiplicity x q

Tactic:
obtain ⟨_, rfl⟩ := hpq

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
w : R[X]
hq : p * w ≠ 0
⊢ rootMultiplicity x p ≤ rootMultiplicity x (p * w)

Tactic:
Nat.le_of_add_right_le <| le_rootMultiplicity_mul x hq

Premises used: Nat.le_of_add_right_le, Polynomial.le_rootMultiplicity_mul
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
x : R
w : R[X]
hq : p * w ≠ 0
⊢ rootMultiplicity x p ≤ rootMultiplicity x (p * w)

Tactic:
exact Nat.le_of_add_right_le <| le_rootMultiplicity_mul x hq

Premises used: Nat.le_of_add_right_le, Polynomial.le_rootMultiplicity_mul
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
rw rw₁ : rootMultiplicity a p ≤ rootMultiplicity a p
⊢ ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ^ (rootMultiplicity a p + 1) ∣ p

Tactic:
rw [← rootMultiplicity_le_iff p0]

Premises used: Polynomial.rootMultiplicity_le_iff
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
pos : ∀ (h : p = 0), rootMultiplicity 0 p = p.natTrailingDegree
neg : ∀ (h : ¬p = 0), rootMultiplicity 0 p = p.natTrailingDegree
⊢ rootMultiplicity 0 p = p.natTrailingDegree

Tactic:
by_cases h : p = 0
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
h : p = 0
⊢ rootMultiplicity 0 p = p.natTrailingDegree

Tactic:
simp only [h, rootMultiplicity_zero, natTrailingDegree_zero]

Premises used: Polynomial.natTrailingDegree_zero, Polynomial.rootMultiplicity_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
h : ¬p = 0
⊢ rootMultiplicity 0 p = p.natTrailingDegree

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
h : ¬p = 0
neg : rootMultiplicity 0 p ≤ p.natTrailingDegree
neg₁ : p.natTrailingDegree ≤ rootMultiplicity 0 p
⊢ rootMultiplicity 0 p = p.natTrailingDegree

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
h : ¬p = 0
neg : ∃ (x : ℕ), ¬(x < p.natTrailingDegree + 1 → p.coeff x = 0)
⊢ rootMultiplicity 0 p ≤ p.natTrailingDegree

Tactic:
rw [rootMultiplicity_le_iff h, map_zero, sub_zero, X_pow_dvd_iff, not_forall]

Premises used: sub_zero, map_zero, Polynomial.X_pow_dvd_iff, Polynomial.rootMultiplicity_le_iff, Classical.not_forall
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
h : ¬p = 0
⊢ ∃ (x : ℕ), ¬(x < p.natTrailingDegree + 1 → p.coeff x = 0)

Tactic:
⟨p.natTrailingDegree,
      fun h' ↦ trailingCoeff_nonzero_iff_nonzero.2 h <| h' <| Nat.lt_add_one _⟩

Premises used: Iff.mpr, Nat.lt_add_one, Polynomial.trailingCoeff_nonzero_iff_nonzero, Exists.intro, Polynomial.natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
h : ¬p = 0
⊢ ∃ (x : ℕ), ¬(x < p.natTrailingDegree + 1 → p.coeff x = 0)

Tactic:
exact ⟨p.natTrailingDegree,
      fun h' ↦ trailingCoeff_nonzero_iff_nonzero.2 h <| h' <| Nat.lt_add_one _⟩
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
h : ¬p = 0
neg : ∀ d < p.natTrailingDegree, p.coeff d = 0
⊢ p.natTrailingDegree ≤ rootMultiplicity 0 p

Tactic:
rw [le_rootMultiplicity_iff h, map_zero, sub_zero, X_pow_dvd_iff]

Premises used: sub_zero, map_zero, Polynomial.le_rootMultiplicity_iff, Polynomial.X_pow_dvd_iff
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
h : ¬p = 0
⊢ ∀ d < p.natTrailingDegree, p.coeff d = 0

Tactic:
fun _ ↦ coeff_eq_zero_of_lt_natTrailingDegree

Premises used: Polynomial.coeff_eq_zero_of_lt_natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
h : ¬p = 0
⊢ ∀ d < p.natTrailingDegree, p.coeff d = 0

Tactic:
exact fun _ ↦ coeff_eq_zero_of_lt_natTrailingDegree

Premises used: Polynomial.coeff_eq_zero_of_lt_natTrailingDegree
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
⊢ Nontrivial R

Tactic:
nontriviality
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
h : Nontrivial R
⊢ q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0

Tactic:
simpa [divByMonic_eq_zero_iff hmonic, hmonic.leadingCoeff,
      Nat.WithBot.one_le_iff_zero_lt] using hdegree

Premises used: Polynomial.divByMonic_eq_zero_iff, Nat.WithBot.one_le_iff_zero_lt, Polynomial.Monic.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
h : Nontrivial R
⊢ q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0

Tactic:
have h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0 := by
    simpa [divByMonic_eq_zero_iff hmonic, hmonic.leadingCoeff,
      Nat.WithBot.one_le_iff_zero_lt] using hdegree
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
h_1 : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
nth_rw : (p /ₘ q).leadingCoeff = (p %ₘ q + q * (p /ₘ q)).leadingCoeff
⊢ (p /ₘ q).leadingCoeff = p.leadingCoeff

Tactic:
nth_rw 2 [← modByMonic_add_div p q]

Premises used: Polynomial.modByMonic_add_div
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
h_1 : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
rw : (p %ₘ q).degree < (q * (p /ₘ q)).degree
⊢ (p /ₘ q).leadingCoeff = (p %ₘ q + q * (p /ₘ q)).leadingCoeff

Tactic:
rw [leadingCoeff_add_of_degree_lt, leadingCoeff_monic_mul hmonic]

Premises used: Polynomial.leadingCoeff_monic_mul, Polynomial.leadingCoeff_add_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
h_1 : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
rw : (p %ₘ q).degree < p.degree
⊢ (p %ₘ q).degree < (q * (p /ₘ q)).degree

Tactic:
rw [degree_mul' h, degree_add_divByMonic hmonic hdegree]

Premises used: Polynomial.degree_mul', Polynomial.degree_add_divByMonic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
h_1 : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p %ₘ q).degree < p.degree

Tactic:
(degree_modByMonic_lt p hmonic).trans_le hdegree

Premises used: LT.lt.trans_le, Polynomial.degree_modByMonic_lt
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
h_1 : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p %ₘ q).degree < p.degree

Tactic:
exact (degree_modByMonic_lt p hmonic).trans_le hdegree

Premises used: LT.lt.trans_le, Polynomial.degree_modByMonic_lt
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
inst_1 : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g
this : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∨ IsUnit g
h : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree = 1

Tactic:
have h₁ : degree (X - C x) = 1 := degree_X_sub_C x
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
inst_1 : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g
this : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∨ IsUnit g
h : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree = 1
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree = 0

Tactic:
have h₂ : degree (X - C x) = 0 := degree_eq_zero_of_isUnit h
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
inst_1 : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g
this : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∨ IsUnit g
h : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree = 1
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree = 0
⊢ Eq (α := WithBot ℕ) 1 0

Tactic:
rw [h₁] at h₂
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
inst_1 : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g
this : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∨ IsUnit g
h : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree = 1
h₂ : Eq (α := WithBot ℕ) 1 0
⊢ ¬Eq (α := WithBot ℕ) 1 0

Tactic:
decide
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
inst_1 : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g
this : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∨ IsUnit g
h : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree = 1
h₂ : Eq (α := WithBot ℕ) 1 0
⊢ p.degree = 1

Tactic:
exact absurd h₂ (by decide)

Premises used: absurd
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
inst_1 : IsDomain R
hi : Irreducible p
x : R
hx : p.IsRoot x
g : R[X]
hg : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g
this : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) ∨ IsUnit g
hgu : IsUnit g
rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * g).degree = 1
rw₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).degree + g.degree = 1
rw₂ : 1 + g.degree = 1
rw₃ : HAdd.hAdd (α := WithBot ℕ) 1 0 = 1
rw₄ rw₅ : Eq (α := WithBot ℕ) 1 1
⊢ p.degree = 1

Tactic:
rw [hg, degree_mul, degree_X_sub_C, degree_eq_zero_of_isUnit hgu, add_zero]

Premises used: Polynomial.degree_X_sub_C, Polynomial.degree_eq_zero_of_isUnit, add_zero, Polynomial.degree_mul
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
inst_1 : IsDomain R
hi : Irreducible p
hdeg : p.natDegree ≠ 1
x : R
⊢ ¬p.IsRoot x

Tactic:
fun hr ↦ hdeg <| natDegree_eq_of_degree_eq_some <| degree_eq_one_of_irreducible_of_root hi hr

Premises used: Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.degree_eq_one_of_irreducible_of_root, Not
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
inst_1 : IsDomain R
hi : Irreducible p
hdeg : p.natDegree ≠ 1
⊢ p.IsRoot = ⊥

Tactic:
le_bot_iff.mp fun _ ↦ hi.not_isRoot_of_natDegree_ne_one hdeg

Premises used: le_bot_iff, Irreducible.not_isRoot_of_natDegree_ne_one, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
p : R[X]
inst_1 : IsDomain R
inst_2 : IsLeftCancelMulZero R
hi : Irreducible p
⊢ Set.Subsingleton.{u} (α := R) {x : R | p.IsRoot x}

Tactic:
fun _ hx ↦ (subsingleton_isRoot_of_natDegree_eq_one <| natDegree_eq_of_degree_eq_some <|
    degree_eq_one_of_irreducible_of_root hi hx) hx

Premises used: Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.subsingleton_isRoot_of_natDegree_eq_one, Set.Subsingleton, Polynomial.degree_eq_one_of_irreducible_of_root
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hp : p.degree ≠ 0
a : R
⊢ Nontrivial R

Tactic:
nontriviality