awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ (p.divModByMonicAux (q := HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) ⋯).2 = p
have 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 := sorry;
      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])) sorry;
      (z + dm.1, dm.2)
    else (0, p)).2 =
  p
Tactic: unfold divModByMonicAux
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
⊢ p % q = p
have have : ∀ (this : ¬(HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree), p % q = p
Tactic: classical
    have : ¬degree (q * C (leadingCoeff q)⁻¹) ≤ degree p :=
      not_le_of_gt <| by rwa [degree_mul_leadingCoeff_inv q hq0]
    rw [mod_def, modByMonic, dif_pos (monic_mul_leadingCoeff_inv hq0)]
    unfold divModByMonicAux
    dsimp
    simp only [this, false_and, if_false]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
have have₁ have₂ :
  ∀ (this : ¬(HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree), p % q = p
⊢ p % q = p
have have₃ : ∀ (this : ¬(HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree),
  (p.divModByMonicAux (q := HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) sorry).2 = p
Tactic: classical
    have : ¬degree (q * C (leadingCoeff q)⁻¹) ≤ degree p :=
      not_le_of_gt <| by rwa [degree_mul_leadingCoeff_inv q hq0]
    rw [mod_def, modByMonic, dif_pos (monic_mul_leadingCoeff_inv hq0)]
    unfold divModByMonicAux
    dsimp
    simp only [this, false_and, if_false]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
have have₁ have₂ :
  ∀ (this : ¬(HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree), p % q = p
have₃ :
  ∀ (this : ¬(HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree),
    (p.divModByMonicAux (q := HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) ⋯).2 = p
⊢ p % q = p
have have₄ : ∀ (this : ¬(HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree),
  (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 := sorry;
        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])) sorry;
        (z + dm.1, dm.2)
      else (0, p)).2 =
    p
Tactic: classical
    have : ¬degree (q * C (leadingCoeff q)⁻¹) ≤ degree p :=
      not_le_of_gt <| by rwa [degree_mul_leadingCoeff_inv q hq0]
    rw [mod_def, modByMonic, dif_pos (monic_mul_leadingCoeff_inv hq0)]
    unfold divModByMonicAux
    dsimp
    simp only [this, false_and, if_false]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
⊢ p.degree < q.degree
have this : q * (p / q) + p % q = p
Tactic: have := EuclideanDomain.div_add_mod p q
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ p.degree < q.degree
have rwa : ∀ (this : q * 0 + p % q = p), p.degree < q.degree
Tactic: rwa [h, mul_zero, zero_add, mod_eq_self_iff hq0] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ p.degree < q.degree
have rwa₁ : ∀ (this : 0 + p % q = p), p.degree < q.degree
Tactic: rwa [h, mul_zero, zero_add, mod_eq_self_iff hq0] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ p.degree < q.degree
have rwa₂ : ∀ (this : p % q = p), p.degree < q.degree
Tactic: rwa [h, mul_zero, zero_add, mod_eq_self_iff hq0] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ p.degree < q.degree
have rwa₃ : ∀ (this : p.degree < q.degree), p.degree < q.degree
Tactic: rwa [h, mul_zero, zero_add, mod_eq_self_iff hq0] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
⊢ p / q = 0
have hlt : 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
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
⊢ p / q = 0
have hm : (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
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ p / q = 0
have 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
Tactic: rw [div_def, (divByMonic_eq_zero_iff hm).2 hlt, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ p / q = 0
have rw₁ : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) (0 : R[X]) = 0
Tactic: rw [div_def, (divByMonic_eq_zero_iff hm).2 hlt, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ p / q = 0
have rw₂ : Eq.{u + 1} (α := R[X]) 0 0
Tactic: rw [div_def, (divByMonic_eq_zero_iff hm).2 hlt, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
hpq : q.degree ≤ p.degree
⊢ q.degree + (p / q).degree = p.degree
have this : (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))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
| p.degree
have rw : q.degree + (p / q).degree
Tactic: rw [← EuclideanDomain.div_add_mod p q, degree_add_eq_left_of_degree_lt this, degree_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ q.degree + (p / q).degree = p.degree
have conv_rhs : 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ q.degree + (p / q).degree = p.degree
have conv_rhs₁ : q.degree + (p / q).degree = q.degree + (p / q).degree
Tactic: conv_rhs =>
    rw [← EuclideanDomain.div_add_mod p q, degree_add_eq_left_of_degree_lt this, degree_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
⊢ (p / q).degree ≤ p.degree
have pos : ∀ (hq : q = 0), (p / q).degree ≤ p.degree
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
pos : ∀ (hq : q = 0), (p / q).degree ≤ p.degree
⊢ (p / q).degree ≤ p.degree
have neg : ∀ (hq : ¬q = 0), (p / q).degree ≤ p.degree
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
hq : ¬q = 0
⊢ (p / q).degree ≤ p.degree
have neg : (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree
Tactic: rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
⊢ (p / q).degree < p.degree
have hq0 : q ≠ 0
Tactic: have hq0 : q ≠ 0 := fun hq0 => by simp [hq0] at hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
hp : p ≠ 0
hq : 0 < q.degree
hq0 : q ≠ 0
⊢ (p / q).degree < p.degree
have rw : (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree < p.degree
Tactic: rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p : R[X]
inst_1 : Field k
f : R →+* k
⊢ IsUnit (map f p) ↔ IsUnit p
have simp_rw : (map f p).degree = 0 ↔ p.degree = 0
Tactic: simp_rw [isUnit_iff_degree_eq_zero, degree_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
have rw : map f
    (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]))) =
  map f p / map f q
Tactic: 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₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
hq0 : ¬q = 0
rw :
  map f
      (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]))) =
    map f p / map f q
⊢ map f (p / q) = map f p / map f q
have rw₁ : map f
    (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]))) =
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
    (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
Tactic: 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₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
hq0 : ¬q = 0
rw :
  map f
      (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]))) =
    map f p / map f q
rw₁ :
  map f
      (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]))) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
⊢ map f (p / q) = map f p / map f q
have rw₂ : map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹) *
    map f (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
    (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
Tactic: 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₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
hq0 : ¬q = 0
rw :
  map f
      (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]))) =
    map f p / map f q
rw₁ :
  map f
      (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]))) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
rw₂ :
  map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹) *
      map f (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
⊢ map f (p / q) = map f p / map f q
have rw₃ : map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹) *
    (map f p /ₘ map f (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))) =
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
    (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
Tactic: 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₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
hq0 : ¬q = 0
rw :
  map f
      (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]))) =
    map f p / map f q
rw₁ :
  map f
      (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]))) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
rw₂ :
  map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹) *
      map f (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
rw₃ :
  map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹) *
      (map f p /ₘ map f (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
⊢ map f (p / q) = map f p / map f q
have rw₄ : map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹) * (map f p /ₘ (map f q * map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹))) =
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
    (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
Tactic: 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₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
hq0 : ¬q = 0
rw :
  map f
      (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]))) =
    map f p / map f q
rw₁ :
  map f
      (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]))) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
rw₂ :
  map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹) *
      map f (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
rw₃ :
  map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹) *
      (map f p /ₘ map f (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
rw₄ :
  map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹) *
      (map f p /ₘ (map f q * map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹))) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
⊢ map f (p / q) = map f p / map f q
have rw₅ : HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff⁻¹) : k[X])
    (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff⁻¹) : k[X])) =
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
    (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
Tactic: 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₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
p q : R[X]
inst_1 : Field k
f : R →+* k
hq0 : ¬q = 0
rw :
  map f
      (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]))) =
    map f p / map f q
rw₁ :
  map f
      (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]))) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
rw₂ :
  map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹) *
      map f (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
rw₃ :
  map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹) *
      (map f p /ₘ map f (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
rw₄ :
  map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹) *
      (map f p /ₘ (map f q * map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹))) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
rw₅ :
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff⁻¹) : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff⁻¹) : k[X])) =
    HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
      (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X]))
⊢ map f (p / q) = map f p / map f q
have rw₆ : HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff⁻¹) : k[X])
    (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff⁻¹) : k[X])) =
  HMul.hMul (α := k[X]) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff)⁻¹ : k[X])
    (map f p /ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff)⁻¹ : k[X]))
Tactic: 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₀]