awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : a ≠ 0
h : p ∣ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q
r : R[X]
hr : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q = p * r
rw : q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p * r)
rw₁ :
  q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q)
rw₂ : q = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) ((C : (a : R) → R[X]) a : R[X]) * q
rw₃ : q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a⁻¹ * a) : R[X]) q
rw₄ : q = (C : (a : R) → R[X]) 1 * q
rw₅ : q = 1 * q
rw₆ rw₇ : q = q
⊢ q = p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) r

Tactic:
rw [mul_left_comm p, ← hr, ← mul_assoc, ← C.map_mul, inv_mul_cancel₀ ha, C.map_one,
        one_mul]

Premises used: Polynomial.C, mul_assoc, RingHom.map_one, mul_left_comm, RingHom.map_mul, inv_mul_cancel₀, one_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
inst_1 : DecidableEq R
hp : p ≠ 0
⊢ p.leadingCoeff ≠ 0

Tactic:
have : p.leadingCoeff ≠ 0 := mt leadingCoeff_eq_zero.mp hp
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
inst_1 : DecidableEq R
hp : p ≠ 0
this : p.leadingCoeff ≠ 0
⊢ (↑(normUnit p) : R[X]) = (C : (a : R) → R[X]) p.leadingCoeff⁻¹

Tactic:
simp [CommGroupWithZero.coe_normUnit _ this]

Premises used: CommGroupWithZero.coe_normUnit
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
pos : ∀ (H : x = 0), map f x ∣ map f y ↔ x ∣ y
neg : ∀ (H : ¬x = 0), map f x ∣ map f y ↔ x ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
by_cases H : x = 0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : x = 0
pos : map f 0 ∣ map f y ↔ 0 ∣ y
pos₁ : 0 ∣ map f y ↔ 0 ∣ y
pos₂ : map f y = 0 ↔ 0 ∣ y
pos₃ : map f y = 0 ↔ y = 0
pos₄ pos₅ : y = 0 ↔ y = 0
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
rw [H, Polynomial.map_zero, zero_dvd_iff, zero_dvd_iff, Polynomial.map_eq_zero]

Premises used: zero_dvd_iff, Polynomial.map_zero, Polynomial.map_eq_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
neg : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ x ∣ y
neg₁ : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₂ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₃ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ x * (↑(normUnit x) : R[X]) ∣ y
neg₄ :
  map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₅ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) (map f x).leadingCoeff⁻¹ : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₆ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) ((f : (a : R) → k) x.leadingCoeff)⁻¹ : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₇ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) ((f : (a : R) → k) x.leadingCoeff⁻¹) : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₈ :
  map f x * map f ((C : (a : R) → R[X]) x.leadingCoeff⁻¹) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₉ :
  map f (HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X])) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₁₀ neg₁₁ :
  HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]

Premises used: Polynomial.coe_normUnit_of_ne_zero, normalize_dvd_iff, Polynomial.map_mul, mt, map_inv₀, normalize_apply, RingHom.injective, Polynomial.monic_mul_leadingCoeff_inv, Iff.mp, Polynomial.map_dvd_map, Polynomial.leadingCoeff_map, Polynomial.map_eq_zero, Polynomial.map_C
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
neg : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ x ∣ y
neg₁ : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₂ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₃ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ x * (↑(normUnit x) : R[X]) ∣ y
neg₄ :
  map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₅ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) (map f x).leadingCoeff⁻¹ : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₆ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) ((f : (a : R) → k) x.leadingCoeff)⁻¹ : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₇ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) ((f : (a : R) → k) x.leadingCoeff⁻¹) : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₈ :
  map f x * map f ((C : (a : R) → R[X]) x.leadingCoeff⁻¹) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₉ :
  map f (HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X])) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₁₀ neg₁₁ :
  HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y

Tactic:
classical
    rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]

Premises used: normalize_dvd_iff, Polynomial.map_mul, map_inv₀, normalize_apply, RingHom.injective, Polynomial.monic_mul_leadingCoeff_inv, Polynomial.map_dvd_map, Polynomial.leadingCoeff_map, Polynomial.map_C
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
inst_1 : DecidableEq R
⊢ degree.{u} (R := R) ((normalize : (a : R[X]) → R[X]) p) = p.degree

Tactic:
simp [normalize_apply]

Premises used: normalize_apply
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
hp1 : p.degree = 1
hp0 : p = 0
⊢ ¬p.degree = 1

Tactic:
simp [hp0]
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
hp1 : p.degree = 1
⊢ Prime (M := R[X]) ((normalize : (a : R[X]) → R[X]) p : R[X])

Tactic:
have : Prime (normalize p) :=
    Monic.prime_of_degree_eq_one (hp1 ▸ degree_normalize)
      (monic_normalize fun hp0 ↦ absurd hp1 (by simp [hp0]))
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
hp1 : p.degree = 1
this : Prime (M := R[X]) ((normalize : (a : R[X]) → R[X]) p : R[X])
⊢ Prime p

Tactic:
(normalize_associated _).prime this

Premises used: Associated.prime, normalize_associated
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
hp1 : p.degree = 1
this : Prime (M := R[X]) ((normalize : (a : R[X]) → R[X]) p : R[X])
⊢ Prime p

Tactic:
exact (normalize_associated _).prime this

Premises used: Associated.prime, normalize_associated
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
hp1 : p.degree = 1
have have₁ have₂ : ∀ (this : Prime (M := R[X]) ((normalize : (a : R[X]) → R[X]) p : R[X])), Prime p
⊢ Prime p

Tactic:
classical
  have : Prime (normalize p) :=
    Monic.prime_of_degree_eq_one (hp1 ▸ degree_normalize)
      (monic_normalize fun hp0 ↦ absurd hp1 (by simp [hp0]))
  exact (normalize_associated _).prime this
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
hp1 : p.degree = 1
⊢ Irreducible p

Tactic:
(prime_of_degree_eq_one hp1).irreducible

Premises used: Prime.irreducible, Polynomial.prime_of_degree_eq_one
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
x : R
pos : ∀ (H : x = 0), ¬Irreducible (M := R[X]) ((C : (a : R) → R[X]) x : R[X])
neg : ∀ (H : ¬x = 0), ¬Irreducible (M := R[X]) ((C : (a : R) → R[X]) x : R[X])
⊢ ¬Irreducible (M := R[X]) ((C : (a : R) → R[X]) x : R[X])

Tactic:
by_cases H : x = 0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
x : R
H : x = 0
pos : ¬Irreducible.{u} (M := R[X]) 0
⊢ ¬Irreducible (M := R[X]) ((C : (a : R) → R[X]) x : R[X])

Tactic:
rw [H, C_0]

Premises used: Polynomial.C_0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
x : R
H : x = 0
⊢ ¬Irreducible.{u} (M := R[X]) 0

Tactic:
not_irreducible_zero

Premises used: not_irreducible_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
x : R
H : x = 0
⊢ ¬Irreducible.{u} (M := R[X]) 0

Tactic:
exact not_irreducible_zero

Premises used: not_irreducible_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
x : R
H : ¬x = 0
⊢ ¬Irreducible (M := R[X]) ((C : (a : R) → R[X]) x : R[X])

Tactic:
fun hx => hx.not_isUnit <| isUnit_C.2 <| isUnit_iff_ne_zero.2 H

Premises used: Iff.mpr, Irreducible.not_isUnit, Polynomial.isUnit_C, isUnit_iff_ne_zero, Not
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
x : R
H : ¬x = 0
⊢ ¬Irreducible (M := R[X]) ((C : (a : R) → R[X]) x : R[X])

Tactic:
exact fun hx => hx.not_isUnit <| isUnit_C.2 <| isUnit_iff_ne_zero.2 H
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p : R[X]
hp : Irreducible p
⊢ 0 < p.degree

Tactic:
lt_of_not_ge fun hp0 =>
    have := eq_C_of_degree_le_zero hp0
    not_irreducible_C (p.coeff 0) <| this ▸ hp

Premises used: lt_of_not_ge, Eq.rec, Polynomial.coeff, Polynomial.eq_C_of_degree_le_zero, Polynomial.not_irreducible_C, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
K : Type u_1
inst : Ring K
f : K[X]
a : K
rw :
  HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) *
        (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) +
      f %ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) =
    f
rw₁ :
  f %ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) =
    f -
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) *
        (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
rw₂ rw₃ :
  f -
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) *
        (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) =
    f -
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) *
        (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
⊢ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) *
      (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) =
    f - f %ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])

Tactic:
rw [eq_sub_iff_add_eq, ← eq_sub_iff_add_eq', modByMonic_eq_sub_mul_div]

Premises used: eq_sub_iff_add_eq', eq_sub_iff_add_eq, Polynomial.modByMonic_eq_sub_mul_div
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
K : Type u_1
inst : CommRing K
f : K[X]
a : K
⊢ Eq (α := K[X])
    ((derivative : (a : K[X]) → K[X])
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) *
          (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))) :
      K[X])
    ((derivative : (a : K[X]) → K[X]) (f - f %ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
      K[X])

Tactic:
apply congrArg derivative <| X_sub_C_mul_divByMonic_eq_sub_modByMonic f a

Premises used: Polynomial.derivative, congrArg, Polynomial.X_sub_C_mul_divByMonic_eq_sub_modByMonic, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
K : Type u_1
inst : CommRing K
f : K[X]
a : K
⊢ Eq (α := K[X])
    ((derivative : (a : K[X]) → K[X])
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) *
          (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))) :
      K[X])
    ((derivative : (a : K[X]) → K[X]) (f - f %ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
      K[X])

Tactic:
have key := by apply congrArg derivative <| X_sub_C_mul_divByMonic_eq_sub_modByMonic f a
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
K : Type u_1
inst : CommRing K
f : K[X]
a : K
key :
  Eq (α := K[X])
    ((derivative : (a : K[X]) → K[X])
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) *
          (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))) :
      K[X])
    ((derivative : (a : K[X]) → K[X]) (f - f %ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
      K[X])
⊢ f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) +
      HMul.hMul (β := K[X]) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
        ((derivative : (a : K[X]) → K[X]) (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          K[X]) =
    (derivative : (a : K[X]) → K[X]) f

Tactic:
simpa only [derivative_mul, derivative_sub, derivative_X, derivative_C, sub_zero, one_mul,
    modByMonic_X_sub_C_eq_C_eval] using key

Premises used: Polynomial.derivative_mul, Polynomial.derivative_X, sub_zero, Polynomial.modByMonic_X_sub_C_eq_C_eval, Polynomial.derivative_sub, Polynomial.derivative_C, one_mul
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
hf :
  HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
    f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])
⊢ f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) +
      HMul.hMul (β := K[X]) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
        ((derivative : (a : K[X]) → K[X]) (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          K[X]) =
    (derivative : (a : K[X]) → K[X]) f

Tactic:
have key := divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative f a
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
hf :
  HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
    f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])
key :
  f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) +
      HMul.hMul (β := K[X]) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
        ((derivative : (a : K[X]) → K[X]) (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          K[X]) =
    (derivative : (a : K[X]) → K[X]) f
have :
  ∀ (u : K[X])
    (hu :
      f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) =
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) * u),
    HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣ (derivative : (a : K[X]) → K[X]) f
⊢ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣ (derivative : (a : K[X]) → K[X]) f

Tactic:
have ⟨u,hu⟩ := hf
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
hf :
  HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
    f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])
key :
  f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) +
      HMul.hMul (β := K[X]) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
        ((derivative : (a : K[X]) → K[X]) (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          K[X]) =
    (derivative : (a : K[X]) → K[X]) f
u : K[X]
hu :
  f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) =
    HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) * u
rw :
  HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
    HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) *
      HAdd.hAdd (β := K[X]) u
        ((derivative : (a : K[X]) → K[X]) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) * u) :
          K[X])
⊢ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣ (derivative : (a : K[X]) → K[X]) f

Tactic:
rw [← key, hu, ← mul_add (X - C a) u _]

Premises used: Polynomial.C, HSub.hSub, mul_add, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
hf :
  HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
    f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])
key :
  f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) +
      HMul.hMul (β := K[X]) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
        ((derivative : (a : K[X]) → K[X]) (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) :
          K[X]) =
    (derivative : (a : K[X]) → K[X]) f
u : K[X]
hu :
  f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) =
    HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) * u
w : K[X]
h :
  HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) *
      HAdd.hAdd (β := K[X]) u
        ((derivative : (a : K[X]) → K[X]) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) * u) :
          K[X]) =
    HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) *
      HAdd.hAdd (β := K[X]) u
        ((derivative : (a : K[X]) → K[X]) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) * u) :
          K[X])
⊢ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
    HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) *
      HAdd.hAdd (β := K[X]) u
        ((derivative : (a : K[X]) → K[X]) (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) * u) :
          K[X])

Tactic:
use (u + derivative ((X - C a) * u))

Premises used: Polynomial.derivative, Polynomial.C, HMul.hMul, HSub.hSub, HAdd.hAdd, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
hf' : eval a ((derivative : (a : K[X]) → K[X]) f) ≠ 0
⊢ IsCoprime (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
    (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))

Tactic:
Or.resolve_left
      (EuclideanDomain.dvd_or_coprime (X - C a) (f /ₘ (X - C a))
        (irreducible_of_degree_eq_one (Polynomial.degree_X_sub_C a))) ?_

Premises used: Polynomial.C, Polynomial.degree_X_sub_C, HSub.hSub, Or.resolve_left, Polynomial.divByMonic, Polynomial.X, DFunLike.coe, EuclideanDomain.dvd_or_coprime, Polynomial.irreducible_of_degree_eq_one
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
hf' : eval a ((derivative : (a : K[X]) → K[X]) f) ≠ 0
refine :
  ¬HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
      f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])
⊢ IsCoprime (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))
    (f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]))

Tactic:
refine Or.resolve_left
      (EuclideanDomain.dvd_or_coprime (X - C a) (f /ₘ (X - C a))
        (irreducible_of_degree_eq_one (Polynomial.degree_X_sub_C a))) ?_

Premises used: Polynomial.C, Polynomial.degree_X_sub_C, HSub.hSub, Or.resolve_left, Polynomial.divByMonic, Polynomial.X, DFunLike.coe, EuclideanDomain.dvd_or_coprime, Polynomial.irreducible_of_degree_eq_one
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
hf' : eval a ((derivative : (a : K[X]) → K[X]) f) ≠ 0
contrapose :
  ∀
    (h :
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
        f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])),
    eval a ((derivative : (a : K[X]) → K[X]) f) = 0
⊢ ¬HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
      f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])

Tactic:
contrapose hf' with h
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
h :
  HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
    f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])
⊢ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣ (derivative : (a : K[X]) → K[X]) f

Tactic:
have : X - C a ∣ derivative f := X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic f h
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
h :
  HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
    f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])
this : HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣ (derivative : (a : K[X]) → K[X]) f
⊢ Eq (α := K[X]) ((C : (a : K) → K[X]) (eval a ((derivative : (a : K[X]) → K[X]) f)) : K[X]) (0 : K[X])

Tactic:
rw [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval] at this

Premises used: Polynomial.monic_X_sub_C, Polynomial.modByMonic_eq_zero_iff_dvd, Polynomial.modByMonic_X_sub_C_eq_C_eval
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
h :
  HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣
    f /ₘ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])
this : Eq (α := K[X]) ((C : (a : K) → K[X]) (eval a ((derivative : (a : K[X]) → K[X]) f)) : K[X]) (0 : K[X])
rwa :
  Eq (α := K[X]) ((C : (a : K) → K[X]) (eval a ((derivative : (a : K[X]) → K[X]) f)) : K[X])
    ((C : (a : K) → K[X]) 0 : K[X])
rwa₁ rwa₂ rwa₃ rwa₄ :
  Eq (α := K[X]) ((C : (a : K) → K[X]) (eval a ((derivative : (a : K[X]) → K[X]) f)) : K[X]) (0 : K[X])
⊢ eval a ((derivative : (a : K[X]) → K[X]) f) = 0

Tactic:
rwa [← C_inj, C_0]

Premises used: Polynomial.C_inj, Polynomial.C_0