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 : R[X]
h : p.degree = 1
⊢ p.roots = {-((p.coeff 1)⁻¹ * p.coeff 0)}
have rw : (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).roots =
  {-(((HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
                ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
            1)⁻¹ *
        (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
              ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
          0)}
Tactic: rw [eq_X_add_C_of_degree_le_one (show degree p ≤ 1 by rw [h])]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 1
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
        ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).roots =
    {-(((HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
                  ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
              1)⁻¹ *
          (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
                ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
            0)}
have this : p.coeff 1 ≠ 0
Tactic: have : p.coeff 1 ≠ 0 := coeff_ne_zero_of_eq_degree h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 1
⊢ p.IsRoot (-((p.coeff 1)⁻¹ * p.coeff 0))
have rw : -((p.coeff 1)⁻¹ * p.coeff 0) ∈ p.roots
Tactic: rw [← mem_roots (by simp [← zero_le_degree_iff, h])]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
u : R[X]ˣ
n : ℕ
⊢ ((↑u : R[X]).coeff n)⁻¹ = (↑u⁻¹ : R[X]).coeff n
have rw : (1 / if n = 0 then (↑u : R[X]).coeff 0 else 0) = if n = 0 then (↑u⁻¹ : R[X]).coeff 0 else 0
Tactic: rw [eq_C_of_degree_eq_zero (degree_coe_units u), eq_C_of_degree_eq_zero (degree_coe_units u⁻¹),
    coeff_C, coeff_C, inv_eq_one_div]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
u : R[X]ˣ
n : ℕ
⊢ (1 / if n = 0 then (↑u : R[X]).coeff 0 else 0) = if n = 0 then (↑u⁻¹ : R[X]).coeff 0 else 0
have pos : n = 0 → 1 / (↑u : R[X]).coeff 0 = (↑u⁻¹ : R[X]).coeff 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
u : R[X]ˣ
n : ℕ
pos : n = 0 → 1 / (↑u : R[X]).coeff 0 = (↑u⁻¹ : R[X]).coeff 0
⊢ (1 / if n = 0 then (↑u : R[X]).coeff 0 else 0) = if n = 0 then (↑u⁻¹ : R[X]).coeff 0 else 0
have neg : ¬n = 0 → 1 / 0 = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
u : R[X]ˣ
n : ℕ
h : n = 0
⊢ 1 / (↑u : R[X]).coeff 0 = (↑u⁻¹ : R[X]).coeff 0
have pos : Eq.{u + 1} (α := R) (eval 0 (↑1 : R[X])) 1
Tactic: rw [div_eq_iff_mul_eq (coeff_coe_units_zero_ne_zero u), coeff_zero_eq_eval_zero,
        coeff_zero_eq_eval_zero, ← eval_mul, ← Units.val_mul, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : Field R
p : R[X]
inst_1 : DecidableEq R
hp0 : p ≠ 0
⊢ Monic.{u} (R := R) ((normalize : (a : R[X]) → R[X]) p)
have hp0₁ : IsUnit p.leadingCoeff
Tactic: rw [Ne, ← leadingCoeff_eq_zero, ← Ne, ← isUnit_iff_ne_zero] at hp0
Cleared hypotheses: hp0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff
have pos : ∀ (hq : q = 0), (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff
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]
hpq : q.degree ≤ p.degree
pos : ∀ (hq : q = 0), (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff
have neg : ∀ (hq : ¬q = 0), (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff
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]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff
have rw : (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree
Tactic: rw [div_def, leadingCoeff_mul, leadingCoeff_C,
    leadingCoeff_divByMonic_of_monic (monic_mul_leadingCoeff_inv hq) _, mul_comm,
    div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
⊢ p / HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p / q)
have pos : ∀ (ha : a = 0),
  p / HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p / q)
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
pos :
  ∀ (ha : a = 0),
    p / HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p / q)
⊢ p / HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p / q)
have neg : ∀ (ha : ¬a = 0),
  p / HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p / q)
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : ¬a = 0
⊢ p / HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p / q)
have neg : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
      (p /ₘ
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
          (q *
            HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
              ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])))) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
      (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])))
Tactic: simp only [div_def, leadingCoeff_mul, mul_inv, leadingCoeff_C, C.map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : ¬a = 0
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
        (p /ₘ
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
            (q *
              HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
                ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])))) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
      (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])))
have neg : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
    (q *
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
  HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
Tactic: congr 3
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : ¬a = 0
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (q *
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
          ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
have neg : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
      (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: rw [mul_left_comm q, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : ¬a = 0
neg :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (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])
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (q *
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
          ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
have neg₁ : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) *
    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: rw [mul_left_comm q, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : ¬a = 0
neg :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (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])
neg₁ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) *
      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])
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (q *
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
          ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
have neg₂ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a⁻¹) : R[X])
    (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: rw [mul_left_comm q, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : ¬a = 0
neg :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (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])
neg₁ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) *
      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])
neg₂ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a⁻¹) : R[X])
      (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])
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (q *
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
          ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
have neg₃ : (C : (a : R) → R[X]) 1 * 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: rw [mul_left_comm q, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : ¬a = 0
neg :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (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])
neg₁ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) *
      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])
neg₂ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a⁻¹) : R[X])
      (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])
neg₃ :
  (C : (a : R) → R[X]) 1 * 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])
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (q *
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
          ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
have neg₄ : 1 * 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: rw [mul_left_comm q, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : ¬a = 0
neg :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (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])
neg₁ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) *
      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])
neg₂ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a⁻¹) : R[X])
      (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])
neg₃ :
  (C : (a : R) → R[X]) 1 * 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])
neg₄ :
  1 * 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])
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (q *
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
          ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])
have neg₅ : 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: rw [mul_left_comm q, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a b : R
inst : Field R
⊢ (C : (a : R) → R[X]) (a / b) =
    HDiv.hDiv (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) b : R[X])
have rw : (C : (a : R) → R[X]) (a / b) =
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) b⁻¹ : R[X])
Tactic: rw [div_C, ← C_mul, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a b : R
inst : Field R
rw :
  (C : (a : R) → R[X]) (a / b) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) b⁻¹ : R[X])
⊢ (C : (a : R) → R[X]) (a / b) =
    HDiv.hDiv (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) b : R[X])
have rw₁ : Eq (α := R[X]) ((C : (a : R) → R[X]) (a / b) : R[X]) ((C : (a : R) → R[X]) (a * b⁻¹) : R[X])
Tactic: rw [div_C, ← C_mul, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a b : R
inst : Field R
rw :
  (C : (a : R) → R[X]) (a / b) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) b⁻¹ : R[X])
rw₁ : Eq (α := R[X]) ((C : (a : R) → R[X]) (a / b) : R[X]) ((C : (a : R) → R[X]) (a * b⁻¹) : R[X])
⊢ (C : (a : R) → R[X]) (a / b) =
    HDiv.hDiv (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) b : R[X])
have rw₂ : Eq (α := R[X]) ((C : (a : R) → R[X]) (a * b⁻¹) : R[X]) ((C : (a : R) → R[X]) (a * b⁻¹) : R[X])
Tactic: rw [div_C, ← C_mul, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : a ≠ 0
h : p ∣ q
r : R[X]
hr : q = p * r
⊢ q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) r
have rw : q =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) r)
Tactic: rw [mul_assoc, mul_left_comm p, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one,
        one_mul, hr]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : a ≠ 0
h : p ∣ q
r : R[X]
hr : q = p * r
rw :
  q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) r)
⊢ q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) r
have 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]) (p * r))
Tactic: rw [mul_assoc, mul_left_comm p, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one,
        one_mul, hr]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : a ≠ 0
h : p ∣ q
r : R[X]
hr : q = p * r
rw :
  q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) 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]) (p * r))
⊢ q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) r
have rw₂ : q = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) * (p * r)
Tactic: rw [mul_assoc, mul_left_comm p, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one,
        one_mul, hr]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : a ≠ 0
h : p ∣ q
r : R[X]
hr : q = p * r
rw :
  q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) 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]) (p * r))
rw₂ : q = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) * (p * r)
⊢ q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) r
have rw₃ : q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a⁻¹) : R[X]) (p * r)
Tactic: rw [mul_assoc, mul_left_comm p, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one,
        one_mul, hr]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : a ≠ 0
h : p ∣ q
r : R[X]
hr : q = p * r
rw :
  q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) 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]) (p * r))
rw₂ : q = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) * (p * r)
rw₃ : q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a⁻¹) : R[X]) (p * r)
⊢ q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) r
have rw₄ : q = (C : (a : R) → R[X]) 1 * (p * r)
Tactic: rw [mul_assoc, mul_left_comm p, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one,
        one_mul, hr]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : a ≠ 0
h : p ∣ q
r : R[X]
hr : q = p * r
rw :
  q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) 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]) (p * r))
rw₂ : q = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) * (p * r)
rw₃ : q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a⁻¹) : R[X]) (p * r)
rw₄ : q = (C : (a : R) → R[X]) 1 * (p * r)
⊢ q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) r
have rw₅ : q = 1 * (p * r)
Tactic: rw [mul_assoc, mul_left_comm p, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one,
        one_mul, hr]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
a : R
inst : Field R
p q : R[X]
ha : a ≠ 0
h : p ∣ q
r : R[X]
hr : q = p * r
rw :
  q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
      (p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) 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]) (p * r))
rw₂ : q = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) * (p * r)
rw₃ : q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a⁻¹) : R[X]) (p * r)
rw₄ : q = (C : (a : R) → R[X]) 1 * (p * r)
rw₅ : q = 1 * (p * r)
rw₆ : q = p * r
⊢ q =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) r
have rw₇ : p * r = p * r
Tactic: rw [mul_assoc, mul_left_comm p, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one,
        one_mul, hr]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ q = p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) r
have rw : q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p * r)
Tactic: rw [mul_left_comm p, ← hr, ← mul_assoc, ← C.map_mul, inv_mul_cancel₀ ha, C.map_one,
        one_mul]