awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
this : ¬(HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree
rw : (p.divModByMonicAux (q := HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) ⋯).2 = p
⊢ p % q = p

Tactic:
rw [mod_def, modByMonic, dif_pos (monic_mul_leadingCoeff_inv hq0)]

Premises used: dif_pos, Polynomial.monic_mul_leadingCoeff_inv, Polynomial.modByMonic, Polynomial.mod_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
this : ¬(HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree
unfold :
  (if h : (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree ∧ p ≠ 0 then
        have z :=
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X
              (p.natDegree - (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).natDegree));
        have _wf := ⋯;
        have dm :=
          (p - HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) * z).divModByMonicAux (q :=
            HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) ⋯;
        (z + dm.1, dm.2)
      else (0, p)).2 =
    p
⊢ (p.divModByMonicAux (q := HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) ⋯).2 = p

Tactic:
unfold divModByMonicAux

Premises used: Polynomial.divModByMonicAux
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
this : ¬(HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree
⊢ (if (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree ∧ ¬p = 0 then
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X
                (p.natDegree - (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).natDegree)) +
            ((p -
                    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
                      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                        (HPow.hPow (α := R[X]) X
                          (p.natDegree -
                            (HMul.hMul (β := R[X]) q
                                ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).natDegree))).divModByMonicAux
                (q := HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) ⋯).1,
          ((p -
                  HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
                    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                      (HPow.hPow (α := R[X]) X
                        (p.natDegree -
                          (HMul.hMul (β := R[X]) q
                              ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).natDegree))).divModByMonicAux
              (q := HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) ⋯).2)
      else (0, p)).2 =
    p

Tactic:
simp only [this, false_and, if_false]

Premises used: if_false, false_and
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
⊢ q * (p / q) + p % q = p

Tactic:
have := EuclideanDomain.div_add_mod p q
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
this : q * (p / q) + p % q = p
rwa : ∀ (this : q * 0 + p % q = p), p.degree < q.degree
rwa₁ : ∀ (this : 0 + p % q = p), p.degree < q.degree
rwa₂ : ∀ (this : p % q = p), p.degree < q.degree
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : p.degree < q.degree), p.degree < q.degree
⊢ p.degree < q.degree

Tactic:
rwa [h, mul_zero, zero_add, mod_eq_self_iff hq0] at this

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

Tactic:
have hlt : degree p < degree (q * C (leadingCoeff q)⁻¹) := by
      rwa [degree_mul_leadingCoeff_inv q hq0]
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
hlt : p.degree < (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree
⊢ (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).Monic

Tactic:
have hm : Monic (q * C (leadingCoeff q)⁻¹) := monic_mul_leadingCoeff_inv hq0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
hlt : p.degree < (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree
hm : (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).Monic
rw :
  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])) =
    0
rw₁ : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) (0 : R[X]) = 0
rw₂ rw₃ : Eq.{u + 1} (α := R[X]) 0 0
⊢ p / q = 0

Tactic:
rw [div_def, (divByMonic_eq_zero_iff hm).2 hlt, mul_zero]

Premises used: Iff.mpr, Polynomial.div_def, Polynomial.divByMonic_eq_zero_iff, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
hpq : q.degree ≤ p.degree
⊢ (p % q).degree < (q * (p / q)).degree

Tactic:
have : degree (p % q) < degree (q * (p / q)) :=
    calc
      degree (p % q) < degree q := EuclideanDomain.mod_lt _ hq0
      _ ≤ _ := degree_le_mul_left _ (mt (Polynomial.div_eq_zero_iff hq0).1 (not_lt_of_ge hpq))
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
hpq : q.degree ≤ p.degree
this : (p % q).degree < (q * (p / q)).degree
rw : q.degree + (p / q).degree
| p.degree

Tactic:
rw [← EuclideanDomain.div_add_mod p q, degree_add_eq_left_of_degree_lt this, degree_mul]

Premises used: EuclideanDomain.div_add_mod, Polynomial.degree_add_eq_left_of_degree_lt, Polynomial.degree_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
hpq : q.degree ≤ p.degree
this : (p % q).degree < (q * (p / q)).degree
conv_rhs : q.degree + (p / q).degree = p.degree
conv_rhs₁ : q.degree + (p / q).degree = q.degree + (p / q).degree
⊢ q.degree + (p / q).degree = p.degree

Tactic:
conv_rhs =>
    rw [← EuclideanDomain.div_add_mod p q, degree_add_eq_left_of_degree_lt this, degree_mul]

Premises used: EuclideanDomain.div_add_mod, Polynomial.degree_add_eq_left_of_degree_lt, Polynomial.degree_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
pos : ∀ (hq : q = 0), (p / q).degree ≤ p.degree
neg : ∀ (hq : ¬q = 0), (p / q).degree ≤ p.degree
⊢ (p / q).degree ≤ p.degree

Tactic:
by_cases hq : q = 0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hq : q = 0
⊢ (p / q).degree ≤ p.degree

Tactic:
simp [hq]
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hq : ¬q = 0
neg : (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree
⊢ (p / q).degree ≤ p.degree

Tactic:
rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq]

Premises used: Polynomial.div_def, Polynomial.degree_mul_leadingCoeff_inv, mul_comm
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hq : ¬q = 0
⊢ (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree

Tactic:
degree_divByMonic_le _ _

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

Tactic:
exact degree_divByMonic_le _ _

Premises used: Polynomial.degree_divByMonic_le
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q = 0
⊢ False

Tactic:
simp [hq0] at hq
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
⊢ q ≠ 0

Tactic:
have hq0 : q ≠ 0 := fun hq0 => by simp [hq0] at hq
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q ≠ 0
rw : (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree < p.degree
⊢ (p / q).degree < p.degree

Tactic:
rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq0]

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

Tactic:
rw [degree_mul_leadingCoeff_inv _ hq0]

Premises used: Polynomial.degree_mul_leadingCoeff_inv
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q ≠ 0
⊢ 0 < q.degree

Tactic:
hq
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q ≠ 0
⊢ 0 < q.degree

Tactic:
exact hq
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q ≠ 0
⊢ (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree < p.degree

Tactic:
exact degree_divByMonic_lt _ (q * C q.leadingCoeff⁻¹) hp
    (by rw [degree_mul_leadingCoeff_inv _ hq0]; exact hq)

Premises used: Polynomial.C, HMul.hMul, Polynomial.leadingCoeff, Inv.inv, Polynomial.degree_divByMonic_lt, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
p : R[X]
inst_1 : Field k
f : R →+* k
simp_rw : (map f p).degree = 0 ↔ p.degree = 0
⊢ IsUnit (map f p) ↔ IsUnit p

Tactic:
simp_rw [isUnit_iff_degree_eq_zero, degree_map]

Premises used: Polynomial.isUnit_iff_degree_eq_zero, Polynomial.degree_map
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
hq0 : q = 0
⊢ map f (p / q) = map f p / map f q

Tactic:
simp [hq0]
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
if : ∀ (hq0 : q = 0), map f (p / q) = map f p / map f q
if₁ : ∀ (hq0 : ¬q = 0), map f (p / q) = map f p / map f q
if₂ : ∀ (hq0 : q = 0), map f (p / q) = map f p / map f q
if₃ if₄ : ∀ (hq0 : ¬q = 0), map f (p / q) = map f p / map f q
⊢ map f (p / q) = map f p / map f q

Tactic:
if hq0 : q = 0 then simp [hq0]
  else
    rw [div_def, div_def, Polynomial.map_mul, map_divByMonic f (monic_mul_leadingCoeff_inv hq0),
      Polynomial.map_mul, map_C, leadingCoeff_map, map_inv₀]

Premises used: Polynomial.div_def, Polynomial.map_mul, map_inv₀, Polynomial.leadingCoeff_map, Polynomial.map_C
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
pos : ∀ (hq0 : q = 0), map f (p % q) = map f p % map f q
neg : ∀ (hq0 : ¬q = 0), map f (p % q) = map f p % map f q
⊢ map f (p % q) = map f p % map f q

Tactic:
by_cases hq0 : q = 0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
hq0 : q = 0
⊢ map f (p % q) = map f p % map f q

Tactic:
simp [hq0]
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
hq0 : ¬q = 0
neg : map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) = map f p % map f q
neg₁ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
neg₂ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff)⁻¹ : k[X])
neg₃ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff⁻¹) : k[X])
neg₄ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ (map f q * map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹))
neg₅ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ map f (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
neg₆ neg₇ :
  map f p %ₘ map f (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ map f (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
⊢ map f (p % q) = map f p % map f q

Tactic:
rw [mod_def, mod_def, leadingCoeff_map f, ← map_inv₀ f, ← map_C f, ← Polynomial.map_mul f,
      map_modByMonic f (monic_mul_leadingCoeff_inv hq0)]

Premises used: Polynomial.map_mul, Polynomial.map_modByMonic, map_inv₀, Polynomial.monic_mul_leadingCoeff_inv, Polynomial.leadingCoeff_map, Polynomial.map_C, Polynomial.mod_def
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
rw : q ≠ 0
⊢ q.leadingCoeff ≠ 0

Tactic:
rw [leadingCoeff_ne_zero]

Premises used: Polynomial.leadingCoeff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
contrapose : ∀ (hq : q = 0), q.natDegree = 0
⊢ q ≠ 0

Tactic:
contrapose hq
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q = 0
⊢ q.natDegree = 0

Tactic:
simp [hq]
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
⊢ q.leadingCoeff ≠ 0

Tactic:
have hq' : q.leadingCoeff ≠ 0 := by
    rw [leadingCoeff_ne_zero]
    contrapose hq
    simp [hq]
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (p %ₘ HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).natDegree < q.natDegree

Tactic:
(natDegree_modByMonic_lt p ?_ ?_).trans_le ?_

Premises used: Polynomial.natDegree_modByMonic_lt, LT.lt.trans_le
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
refine_1 : (HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).Monic
refine_2 : HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X]) ≠ 1
refine_3 : (HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).natDegree ≤ q.natDegree
⊢ (p %ₘ HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).natDegree < q.natDegree

Tactic:
refine (natDegree_modByMonic_lt p ?_ ?_).trans_le ?_

Premises used: Polynomial.natDegree_modByMonic_lt, LT.lt.trans_le
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).Monic

Tactic:
monic_mul_C_of_leadingCoeff_mul_eq_one ?_

Premises used: Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
refine_1 : q.leadingCoeff * q.leadingCoeff⁻¹ = 1
⊢ (HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).Monic

Tactic:
refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_

Premises used: Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
refine_1 refine_1₁ : q.leadingCoeff = q.leadingCoeff
⊢ q.leadingCoeff * q.leadingCoeff⁻¹ = 1

Tactic:
rw [mul_inv_eq_one₀ hq']

Premises used: mul_inv_eq_one₀
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
refine_2 : ∀ (hq : HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X]) = 1), q.natDegree = 0
⊢ HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X]) ≠ 1

Tactic:
contrapose hq
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
k : Type y
inst : Field k
p q : k[X]
hq' : q.leadingCoeff ≠ 0
hq : HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X]) = 1
refine_2 : (HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).natDegree = 0
⊢ q.natDegree = 0

Tactic:
rw [← natDegree_mul_C_eq_of_mul_eq_one ((inv_mul_eq_one₀ hq').mpr rfl)]

Premises used: Iff.mpr, Polynomial.natDegree_mul_C_eq_of_mul_eq_one, inv_mul_eq_one₀, rfl
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
k : Type y
inst : Field k
p q : k[X]
hq' : q.leadingCoeff ≠ 0
hq : HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X]) = 1
⊢ (HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).natDegree = 0

Tactic:
simp [hq]
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).natDegree ≤ q.natDegree

Tactic:
natDegree_mul_C_le q q.leadingCoeff⁻¹

Premises used: Polynomial.leadingCoeff, Inv.inv, Polynomial.natDegree_mul_C_le
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).natDegree ≤ q.natDegree

Tactic:
exact natDegree_mul_C_le q q.leadingCoeff⁻¹

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

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hq : q ≠ 0
refine : (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).Monic
⊢ (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree < q.degree

Tactic:
refine (Polynomial.degree_modByMonic_lt p ?_).trans_eq (by simp)

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

Tactic:
simp [Polynomial.Monic.def, hq]

Premises used: Polynomial.Monic.def
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p₁ p₂ q : R[X]
⊢ (p₁ + p₂) % q = p₁ % q + p₂ % q

Tactic:
simp [Polynomial.mod_def, Polynomial.add_modByMonic]

Premises used: Polynomial.add_modByMonic, Polynomial.mod_def
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p₁ p₂ q : R[X]
⊢ (p₁ - p₂) % q = p₁ % q - p₂ % q

Tactic:
simp [Polynomial.mod_def, Polynomial.sub_modByMonic]

Premises used: Polynomial.sub_modByMonic, Polynomial.mod_def
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p₁ p₂ q : R[X]
⊢ p₁ * 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])

Tactic:
apply Polynomial.mul_modByMonic

Premises used: Polynomial.mul_modByMonic
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
inst_2 : DecidableEq R
inst_3 : DecidableEq k
f : R →+* k
x : R[X]
simp_rw : EuclideanDomain.gcd 0 (map f x) = map f (EuclideanDomain.gcd 0 x)
⊢ EuclideanDomain.gcd (map f 0) (map f x) = map f (EuclideanDomain.gcd 0 x)

Tactic:
simp_rw [Polynomial.map_zero, EuclideanDomain.gcd_zero_left]

Premises used: EuclideanDomain.gcd_zero_left, Polynomial.map_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
inst_2 : DecidableEq R
inst_3 : DecidableEq k
f : R →+* k
x y : R[X]
h : x ≠ 0
ih : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd (y % x) x)
rw : EuclideanDomain.gcd (map f y % map f x) (map f x) = map f (EuclideanDomain.gcd x y)
rw₁ : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd x y)
rw₂ : map f (EuclideanDomain.gcd (y % x) x) = map f (EuclideanDomain.gcd x y)
rw₃ rw₄ : map f (EuclideanDomain.gcd x y) = map f (EuclideanDomain.gcd x y)
⊢ EuclideanDomain.gcd (map f x) (map f y) = map f (EuclideanDomain.gcd x y)

Tactic:
rw [gcd_val, ← map_mod, ih, ← gcd_val]

Premises used: Polynomial.map_mod, EuclideanDomain.gcd_val
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hf : eval₂ ϕ α f = 0
hg : eval₂ ϕ α g = 0
rw : eval₂ ϕ α (f * EuclideanDomain.gcdA f g + g * EuclideanDomain.gcdB f g) = 0
rw₁ : eval₂ ϕ α (f * EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
rw₂ : eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
rw₃ : eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α g * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
rw₄ : 0 * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α g * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
rw₅ : 0 * eval₂ ϕ α (EuclideanDomain.gcdA f g) + 0 * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
rw₆ : 0 + 0 * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
rw₇ : HAdd.hAdd (α := k) 0 0 = 0
rw₈ rw₉ : Eq.{y + 1} (α := k) 0 0
⊢ eval₂ ϕ α (EuclideanDomain.gcd f g) = 0

Tactic:
rw [EuclideanDomain.gcd_eq_gcd_ab f g, Polynomial.eval₂_add, Polynomial.eval₂_mul,
    Polynomial.eval₂_mul, hf, hg, zero_mul, zero_mul, zero_add]

Premises used: MulZeroClass.zero_mul, EuclideanDomain.gcd_eq_gcd_ab, zero_add, Polynomial.eval₂_mul, Polynomial.eval₂_add
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
inst_1 : DecidableEq R
f g : R[X]
α : R
hf : eval α f = 0
hg : eval α g = 0
⊢ eval α (EuclideanDomain.gcd f g) = 0

Tactic:
eval₂_gcd_eq_zero hf hg

Premises used: Polynomial.eval, Polynomial.eval₂_gcd_eq_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
obtain : ∀ (p : R[X]) (hp : f = EuclideanDomain.gcd f g * p), eval₂ ϕ α f = 0
⊢ eval₂ ϕ α f = 0

Tactic:
obtain ⟨p, hp⟩ := EuclideanDomain.gcd_dvd_left f g

Premises used: EuclideanDomain.gcd_dvd_left
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : f = EuclideanDomain.gcd f g * p
rw : eval₂ ϕ α (EuclideanDomain.gcd f g * p) = 0
rw₁ : eval₂ ϕ α (EuclideanDomain.gcd f g) * eval₂ ϕ α p = 0
rw₂ : 0 * eval₂ ϕ α p = 0
rw₃ rw₄ : Eq.{y + 1} (α := k) 0 0
⊢ eval₂ ϕ α f = 0

Tactic:
rw [hp, Polynomial.eval₂_mul, hα, zero_mul]

Premises used: MulZeroClass.zero_mul, Polynomial.eval₂_mul