awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
a_1 b_1 : R[X]
hp0 : a_1 ≠ 0
hq0 : b_1 ≠ 0
hp0₁ : ¬a_1.leadingCoeff = 0
⊢ ¬b_1.leadingCoeff = 0

Tactic:
rw [Ne, ← leadingCoeff_eq_zero] at *

Premises used: Ne, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
a_1 b_1 : R[X]
hp0 : ¬a_1.leadingCoeff = 0
hq0 : ¬b_1.leadingCoeff = 0
rw :
  (C : (a : R) → R[X]) (↑(normUnit (a_1.leadingCoeff * b_1.leadingCoeff)) : R) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit a_1.leadingCoeff) : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit b_1.leadingCoeff) : R) : R[X])
rw₁ :
  (C : (a : R) → R[X]) (↑(HMul.hMul (α := Rˣ) (normUnit a_1.leadingCoeff) (normUnit b_1.leadingCoeff)) : R) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit a_1.leadingCoeff) : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit b_1.leadingCoeff) : R) : R[X])
rw₂ :
  (C : (a : R) → R[X]) ((↑(normUnit a_1.leadingCoeff) : R) * (↑(normUnit b_1.leadingCoeff) : R)) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit a_1.leadingCoeff) : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit b_1.leadingCoeff) : R) : R[X])
rw₃ rw₄ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit a_1.leadingCoeff) : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit b_1.leadingCoeff) : R) : R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit a_1.leadingCoeff) : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit b_1.leadingCoeff) : R) : R[X])
⊢ (C : (a : R) → R[X]) (↑(normUnit (a_1 * b_1).leadingCoeff) : R) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit a_1.leadingCoeff) : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit b_1.leadingCoeff) : R) : R[X])

Tactic:
rw [leadingCoeff_mul, normUnit_mul hp0 hq0, Units.val_mul, C_mul]

Premises used: Polynomial.leadingCoeff_mul, Polynomial.C_mul, NormalizationMonoid.normUnit_mul, Units.val_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
u : R[X]ˣ
rw :
  HMul.hMul (β := R[X]) (↑u : R[X]) ((C : (a : R) → R[X]) (↑(normUnit (↑u : R[X]).leadingCoeff) : R) : R[X]) =
    (↑1 : R[X])
⊢ (C : (a : R) → R[X]) (↑(normUnit (↑u : R[X]).leadingCoeff) : R) = (↑u⁻¹ : R[X])

Tactic:
rw [← mul_one u⁻¹, Units.val_mul, Units.eq_inv_mul_iff_mul_eq]

Premises used: Inv.inv, mul_one, Units.eq_inv_mul_iff_mul_eq, Units.val_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
u : R[X]ˣ
rcases :
  ∀ (w : Rˣ) (h2 : (C : (a : R) → R[X]) (↑w : R) = (↑u : R[X])),
    HMul.hMul (β := R[X]) (↑u : R[X]) ((C : (a : R) → R[X]) (↑(normUnit (↑u : R[X]).leadingCoeff) : R) : R[X]) =
      (↑1 : R[X])
⊢ HMul.hMul (β := R[X]) (↑u : R[X]) ((C : (a : R) → R[X]) (↑(normUnit (↑u : R[X]).leadingCoeff) : R) : R[X]) =
    (↑1 : R[X])

Tactic:
rcases Polynomial.isUnit_iff.1 ⟨u, rfl⟩ with ⟨_, ⟨w, rfl⟩, h2⟩

Premises used: Polynomial.isUnit_iff, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
u : R[X]ˣ
w : Rˣ
h2 : (C : (a : R) → R[X]) (↑w : R) = (↑u : R[X])
rw : Eq.{u + 1} (α := R[X]) 1 (↑1 : R[X])
⊢ HMul.hMul (β := R[X]) (↑u : R[X]) ((C : (a : R) → R[X]) (↑(normUnit (↑u : R[X]).leadingCoeff) : R) : R[X]) =
    (↑1 : R[X])

Tactic:
rw [← h2, leadingCoeff_C, normUnit_coe_units, ← C_mul, Units.mul_inv, C_1]

Premises used: Polynomial.C_1, NormalizationMonoid.normUnit_coe_units, Units.mul_inv, Polynomial.C_mul, Polynomial.leadingCoeff_C
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
u : R[X]ˣ
w : Rˣ
h2 : (C : (a : R) → R[X]) (↑w : R) = (↑u : R[X])
⊢ Eq.{u + 1} (α := R[X]) 1 (↑1 : R[X])

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
p : R[X]
⊢ (↑(normUnit p) : R[X]) = (C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff) : R)

Tactic:
simp [normUnit]

Premises used: NormalizationMonoid.normUnit
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
p : R[X]
⊢ Eq (α := R) (leadingCoeff ((normalize : (a : R[X]) → R[X]) p) : R) ((normalize : (a : R) → R) p.leadingCoeff : R)

Tactic:
simp [normalize_apply]

Premises used: normalize_apply
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
p : R[X]
hp : p.Monic
⊢ (normalize : (a : R[X]) → R[X]) p = p

Tactic:
simp only [Polynomial.coe_normUnit, normalize_apply, hp.leadingCoeff, normUnit_one,
    Units.val_one, Polynomial.C.map_one, mul_one]

Premises used: Polynomial.C, RingHom.map_one, normalize_apply, Polynomial.coe_normUnit, Units.val_one, normUnit_one, Polynomial.Monic.leadingCoeff, mul_one
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NormalizationMonoid R
p : R[X]
rw : (p * (↑(normUnit p) : R[X])).roots = p.roots
rw₁ : ((↑(normUnit p) : R[X]) * p).roots = p.roots
rw₂ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff) : R) : R[X]) p).roots = p.roots
rw₃ rw₄ : p.roots = p.roots
⊢ roots ((normalize : (a : R[X]) → R[X]) p) = p.roots

Tactic:
rw [normalize_apply, mul_comm, coe_normUnit, roots_C_mul _ (normUnit (leadingCoeff p)).ne_zero]

Premises used: Polynomial.roots_C_mul, Units.ne_zero, Polynomial.leadingCoeff, normalize_apply, Polynomial.coe_normUnit, mul_comm, NormalizationMonoid.normUnit
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
⊢ Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑(normUnit (leadingCoeff X)) : R))

Tactic:
have := coe_normUnit (R := R) (p := X)
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑(normUnit (leadingCoeff X)) : R))
rwa :
  ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑(normUnit 1) : R))),
    Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
rwa₁ :
  ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑1 : R))),
    Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
rwa₂ :
  ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) 1)),
    Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
rwa₃ : ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) 1), Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (this : Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1), Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
⊢ Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1

Tactic:
rwa [leadingCoeff_X, normUnit_one, Units.val_one, map_one, Units.val_eq_one] at this

Premises used: Polynomial.leadingCoeff_X, map_one, Units.val_one, normUnit_one, Units.val_eq_one
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
⊢ Eq.{u + 1} (α := R[X]) X ((normalize : (a : R[X]) → R[X]) X)

Tactic:
simp only [normalize_apply, normUnit_X, Units.val_one, mul_one]

Premises used: normalize_apply, Units.val_one, mul_one, Polynomial.normUnit_X
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : DivisionRing R
p : R[X]
hp0 : p ≠ 0
hp : ¬IsUnit p
h : p.degree ≤ 0
⊢ Ne (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])

Tactic:
rw [eq_C_of_degree_le_zero h] at hp0 hp

Premises used: Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : DivisionRing R
p : R[X]
hp0 : p ≠ 0
hp : ¬IsUnit p
h : p.degree ≤ 0
hp0₁ : Ne (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])
⊢ ¬IsUnit (M := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])

Tactic:
rw [eq_C_of_degree_le_zero h] at hp0 hp

Premises used: Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : DivisionRing R
p : R[X]
hp0 : p ≠ 0
hp : ¬IsUnit p
h : p.degree ≤ 0
hp0₁ : Ne (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])
hp₁ : ¬IsUnit (M := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
⊢ p.degree ≤ 0

Tactic:
rw [eq_C_of_degree_le_zero h] at hp0 hp

Premises used: Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : DivisionRing R
p : R[X]
hp0 : Ne (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])
hp : ¬IsUnit (M := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
h : p.degree ≤ 0
⊢ ¬Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) ((C : (a : R) → R[X]) 0 : R[X])

Tactic:
simpa using hp0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : DivisionRing R
p : R[X]
hp0 : Ne (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])
hp : ¬IsUnit (M := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
h : p.degree ≤ 0
⊢ False

Tactic:
exact hp (IsUnit.map C (IsUnit.mk0 (coeff p 0) (mt C_inj.2 (by simpa using hp0))))

Premises used: Iff.mpr, Polynomial.C, Polynomial.C_inj, mt, Polynomial.coeff, IsUnit.mk0, IsUnit.map, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : IsSimpleRing R
inst_2 : Semiring S
inst_3 : Nontrivial S
p : R[X]
f : R →+* S
⊢ map f p = 0 ↔ p = 0

Tactic:
Polynomial.map_eq_zero_iff f.injective

Premises used: RingHom.injective, Polynomial.map_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : IsSimpleRing R
inst_2 : Semiring S
inst_3 : Nontrivial S
p : R[X]
f : R →+* S
hp : p ≠ 0
⊢ map f p ≠ 0

Tactic:
mt (Polynomial.map_eq_zero f).1 hp

Premises used: mt, Iff.mp, Polynomial.map_eq_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : IsSimpleRing R
inst_2 : Semiring S
inst_3 : Nontrivial S
p : R[X]
f : R →+* S
⊢ (map f p).degree = p.degree

Tactic:
degree_map_eq_of_injective f.injective _

Premises used: RingHom.injective, Polynomial.degree_map_eq_of_injective
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : IsSimpleRing R
inst_2 : Semiring S
inst_3 : Nontrivial S
p : R[X]
f : R →+* S
⊢ (map f p).natDegree = p.natDegree

Tactic:
natDegree_map_eq_of_injective f.injective _

Premises used: RingHom.injective, Polynomial.natDegree_map_eq_of_injective
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : IsSimpleRing R
inst_2 : Semiring S
inst_3 : Nontrivial S
p : R[X]
f : R →+* S
⊢ (map f p).leadingCoeff = (f : (a : R) → S) p.leadingCoeff

Tactic:
leadingCoeff_map_of_injective f.injective _

Premises used: RingHom.injective, Polynomial.leadingCoeff_map_of_injective
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : IsSimpleRing R
inst_2 : Semiring S
inst_3 : Nontrivial S
p : R[X]
f : R →+* S
⊢ (map f p).nextCoeff = (f : (a : R) → S) p.nextCoeff

Tactic:
nextCoeff_map f.injective _

Premises used: Polynomial.nextCoeff_map, RingHom.injective
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : IsSimpleRing R
inst_2 : Semiring S
inst_3 : Nontrivial S
f : R →+* S
p : R[X]
⊢ (map f p).Monic ↔ p.Monic

Tactic:
Function.Injective.monic_map_iff f.injective |>.symm

Premises used: Function.Injective.monic_map_iff, RingHom.injective, Iff.symm
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 0
⊢ p.degree ≤ 0

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 = 0
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) 0) = 0

Tactic:
rw [eq_C_of_degree_le_zero this, hc] at h

Premises used: Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 = 0
h₁ : degree.{u} (R := R) ((C : (a : R) → R[X]) 0) = 0
⊢ p.degree ≤ 0

Tactic:
rw [eq_C_of_degree_le_zero this, hc] at h

Premises used: Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 = 0
h₁ : degree.{u} (R := R) ((C : (a : R) → R[X]) 0) = 0
this₁ : p.degree ≤ 0
⊢ p.coeff 0 = 0

Tactic:
rw [eq_C_of_degree_le_zero this, hc] at h

Premises used: Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
h : degree.{u} (R := R) ((C : (a : R) → R[X]) 0) = 0
this : p.degree ≤ 0
hc : p.coeff 0 = 0
⊢ degree.{u} (R := R) 0 = 0

Tactic:
simp only [map_zero] at h

Premises used: map_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
this : p.degree ≤ 0
hc : p.coeff 0 = 0
h : degree.{u} (R := R) 0 = 0
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 ≠ 0
rw : ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
| p

Tactic:
rw [eq_C_of_degree_le_zero this]

Premises used: Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 ≠ 0
conv :
  1 =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
      ((C : (a : R) → R[X]) (p.coeff 0)⁻¹ : R[X])
⊢ 1 = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (p.coeff 0)⁻¹ : R[X])

Tactic:
conv in p => rw [eq_C_of_degree_le_zero this]

Premises used: Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 ≠ 0
rw : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (p.coeff 0 * (p.coeff 0)⁻¹) : R[X])
rw₁ : Eq.{u + 1} (α := R[X]) 1 ((C : (a : R) → R[X]) 1)
rw₂ rw₃ : Eq.{u + 1} (α := R[X]) 1 1
⊢ 1 =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
      ((C : (a : R) → R[X]) (p.coeff 0)⁻¹ : R[X])

Tactic:
rw [← C_mul, mul_inv_cancel₀ hc, C_1]

Premises used: Polynomial.C_1, mul_inv_cancel₀, Polynomial.C_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
pos : ∀ (h : q = 0), q * p.div q + p.mod q = p
neg : ∀ (h : ¬q = 0), q * p.div q + p.mod q = p
⊢ q * p.div q + p.mod q = p

Tactic:
by_cases h : q = 0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
h : q = 0
⊢ q * p.div q + p.mod q = p

Tactic:
simp only [h, zero_mul, mod, modByMonic_zero, zero_add]

Premises used: MulZeroClass.zero_mul, zero_add, Polynomial.modByMonic_zero, Polynomial.mod
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
h : ¬q = 0
rhs : p
| q * p.div q + p.mod q = p

Tactic:
rhs
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
h : ¬q = 0
rw :
  p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
      (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
| p

Tactic:
rw [← modByMonic_add_div p (q * C q.leadingCoeff⁻¹)]

Premises used: Polynomial.C, HMul.hMul, Polynomial.leadingCoeff, Inv.inv, Polynomial.modByMonic_add_div, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
h : ¬q = 0
rw :
  p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
      (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
| q * p.div q + p.mod q = p

Tactic:
rhs
      rw [← modByMonic_add_div p (q * C q.leadingCoeff⁻¹)]

Premises used: Polynomial.C, HMul.hMul, Polynomial.leadingCoeff, Inv.inv, Polynomial.modByMonic_add_div, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
h : ¬q = 0
neg :
  q * p.div q + p.mod q =
    p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
⊢ q * p.div q + p.mod q = p

Tactic:
conv =>
      rhs
      rw [← modByMonic_add_div p (q * C q.leadingCoeff⁻¹)]

Premises used: Polynomial.C, HMul.hMul, Polynomial.leadingCoeff, Inv.inv, Polynomial.modByMonic_add_div, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
h : ¬q = 0
neg :
  q *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
          (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) +
      p.mod q =
    p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
neg₁ :
  q *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
          (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) +
      p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) =
    p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
neg₂ :
  p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      q *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
          (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
neg₃ neg₄ :
  p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      q *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
          (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      q *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
          (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
⊢ q * p.div q + p.mod q =
    p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))

Tactic:
rw [div, mod, add_comm, mul_assoc]

Premises used: mul_assoc, add_comm, Polynomial.div, Polynomial.mod
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
q p : R[X]
hq : q ≠ 0
rw : (p.mod q).degree < (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree
⊢ (p.mod q).degree < q.degree

Tactic:
rw [← degree_mul_leadingCoeff_inv q hq]

Premises used: Polynomial.degree_mul_leadingCoeff_inv
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
q p : R[X]
hq : q ≠ 0
⊢ (p.mod q).degree < (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree

Tactic:
degree_modByMonic_lt p (monic_mul_leadingCoeff_inv hq)

Premises used: Polynomial.monic_mul_leadingCoeff_inv, Polynomial.degree_modByMonic_lt, Polynomial.mod
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
q p : R[X]
hq : q ≠ 0
⊢ (p.mod q).degree < (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree

Tactic:
exact degree_modByMonic_lt p (monic_mul_leadingCoeff_inv hq)

Premises used: Polynomial.monic_mul_leadingCoeff_inv, Polynomial.degree_modByMonic_lt
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
⊢ p / q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
      (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))

Tactic:
rfl

Premises used: Polynomial.div, rfl
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
⊢ p % q = p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])

Tactic:
rfl

Premises used: dite, Polynomial.modByMonic, Polynomial.mod, rfl
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
q p : R[X]
hq : q.Monic
⊢ p %ₘ q = p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])

Tactic:
simp only [Monic.def.1 hq, inv_one, mul_one, C_1]

Premises used: Polynomial.C_1, inv_one, Iff.mp, Polynomial.Monic.def, mul_one
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
q p : R[X]
hq : q.Monic
⊢ p /ₘ q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
      (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))

Tactic:
simp only [Monic.def.1 hq, inv_one, C_1, one_mul, mul_one]

Premises used: Polynomial.C_1, inv_one, Iff.mp, Polynomial.Monic.def, mul_one, one_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
a : R
⊢ p % HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = (C : (a : R) → R[X]) (eval a p)

Tactic:
modByMonic_eq_mod p (monic_X_sub_C a) ▸ modByMonic_X_sub_C_eq_C_eval _ _

Premises used: Polynomial.monic_X_sub_C, Eq.rec, Polynomial.modByMonic_X_sub_C_eq_C_eval, Polynomial.modByMonic_eq_mod
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
a : R
inst : Field R
p : R[X]
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) *
        (p / HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) =
      p ↔
    p.IsRoot a

Tactic:
divByMonic_eq_div p (monic_X_sub_C a) ▸ mul_divByMonic_eq_iff_isRoot

Premises used: Polynomial.mul_divByMonic_eq_iff_isRoot, Polynomial.monic_X_sub_C, Eq.rec, Polynomial.divByMonic_eq_div
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst : Field R
p q : R[X]
⊢ ∀ (a : R[X]), a / 0 = 0

Tactic:
simp [div_def]

Premises used: Polynomial.div_def
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
rwa rwa₁ rwa₂ rwa₃ : p.degree < q.degree
⊢ p.degree < (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree

Tactic:
rwa [degree_mul_leadingCoeff_inv q hq0]

Premises used: Polynomial.degree_mul_leadingCoeff_inv
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
⊢ ¬(HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree

Tactic:
have : ¬degree (q * C (leadingCoeff q)⁻¹) ≤ degree p :=
      not_le_of_gt <| by rwa [degree_mul_leadingCoeff_inv q hq0]