awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ map f x ∣ map f y ↔ x ∣ y
have neg₃ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ x * (↑(normUnit x) : R[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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ map f x ∣ map f y ↔ x ∣ y
have 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
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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ map f x ∣ map f y ↔ x ∣ y
have 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
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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ map f x ∣ map f y ↔ x ∣ y
have 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
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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ map f x ∣ map f y ↔ x ∣ y
have 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
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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ map f x ∣ map f y ↔ x ∣ y
have 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
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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ map f x ∣ map f y ↔ x ∣ y
have 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
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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ map f x ∣ map f y ↔ x ∣ y
have 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
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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : Field R
p : R[X]
hp1 : p.degree = 1
⊢ Prime p
have this : 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]))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p : R[X]
hp1 : p.degree = 1
⊢ Prime p
have have : ∀ (this : Prime (M := R[X]) ((normalize : (a : R[X]) → R[X]) p : R[X])), 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
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
x : R
⊢ ¬Irreducible (M := R[X]) ((C : (a : R) → R[X]) x : R[X])
have pos : ∀ (H : x = 0), ¬Irreducible (M := R[X]) ((C : (a : R) → R[X]) x : R[X])
Tactic: by_cases H : x = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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])
⊢ ¬Irreducible (M := R[X]) ((C : (a : R) → R[X]) x : R[X])
have neg : ∀ (H : ¬x = 0), ¬Irreducible (M := R[X]) ((C : (a : R) → R[X]) x : R[X])
Tactic: by_cases H : x = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
x : R
H : x = 0
⊢ ¬Irreducible (M := R[X]) ((C : (a : R) → R[X]) x : R[X])
have pos : ¬Irreducible.{u} (M := R[X]) 0
Tactic: rw [H, C_0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
K : Type u_1
inst : Ring K
f : K[X]
a : K
⊢ 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])
have 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
Tactic: rw [eq_sub_iff_add_eq, ← eq_sub_iff_add_eq', modByMonic_eq_sub_mul_div]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ 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])
have 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]))
Tactic: rw [eq_sub_iff_add_eq, ← eq_sub_iff_add_eq', modByMonic_eq_sub_mul_div]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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]))
⊢ 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])
have 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]))
Tactic: rw [eq_sub_iff_add_eq, ← eq_sub_iff_add_eq', modByMonic_eq_sub_mul_div]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
K : Type u_1
inst : CommRing K
f : K[X]
a : K
⊢ 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 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])
Tactic: have key := by apply congrArg derivative <| X_sub_C_mul_divByMonic_eq_sub_modByMonic f a
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
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])
⊢ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣ (derivative : (a : K[X]) → K[X]) f
have 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
Tactic: have key := divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative f a
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣ (derivative : (a : K[X]) → K[X]) f
have 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
Tactic: have ⟨u,hu⟩ := hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) ∣ (derivative : (a : K[X]) → K[X]) f
have 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])
Tactic: rw [← key, hu, ← mul_add (X - C a) u _]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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]
⊢ 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])
have 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])
Tactic: use (u + derivative ((X - C a) * u))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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]))
have 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])
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))) ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
K : Type u_1
inst : Field K
f : K[X]
a : K
hf' : 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])
have 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
Tactic: contrapose hf' with h
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
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])
⊢ eval a ((derivative : (a : K[X]) → K[X]) f) = 0
have this : 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