awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
a_1 b_1 : R[X]
hp0 : ¬a_1.leadingCoeff = 0
hq0 : ¬b_1.leadingCoeff = 0
rw :
  (C : (a : R) → R[X]) (↑(normUnit (a_1.leadingCoeff * b_1.leadingCoeff)) : R) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit a_1.leadingCoeff) : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit b_1.leadingCoeff) : R) : R[X])
rw₁ :
  (C : (a : R) → R[X]) (↑(HMul.hMul (α := Rˣ) (normUnit a_1.leadingCoeff) (normUnit b_1.leadingCoeff)) : R) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit a_1.leadingCoeff) : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit b_1.leadingCoeff) : R) : R[X])
rw₂ :
  (C : (a : R) → R[X]) ((↑(normUnit a_1.leadingCoeff) : R) * (↑(normUnit b_1.leadingCoeff) : R)) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit a_1.leadingCoeff) : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit b_1.leadingCoeff) : R) : R[X])
⊢ (C : (a : R) → R[X]) (↑(normUnit (a_1 * b_1).leadingCoeff) : R) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit a_1.leadingCoeff) : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit b_1.leadingCoeff) : R) : R[X])
have rw₃ : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit a_1.leadingCoeff) : R) : R[X])
    ((C : (a : R) → R[X]) (↑(normUnit b_1.leadingCoeff) : R) : R[X]) =
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit a_1.leadingCoeff) : R) : R[X])
    ((C : (a : R) → R[X]) (↑(normUnit b_1.leadingCoeff) : R) : R[X])
Tactic: rw [leadingCoeff_mul, normUnit_mul hp0 hq0, Units.val_mul, C_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
u : R[X]ˣ
⊢ (C : (a : R) → R[X]) (↑(normUnit (↑u : R[X]).leadingCoeff) : R) = (↑u⁻¹ : R[X])
have rw : HMul.hMul (β := R[X]) (↑u : R[X]) ((C : (a : R) → R[X]) (↑(normUnit (↑u : R[X]).leadingCoeff) : R) : R[X]) = (↑1 : R[X])
Tactic: rw [← mul_one u⁻¹, Units.val_mul, Units.eq_inv_mul_iff_mul_eq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
u : R[X]ˣ
⊢ HMul.hMul (β := R[X]) (↑u : R[X]) ((C : (a : R) → R[X]) (↑(normUnit (↑u : R[X]).leadingCoeff) : R) : R[X]) =
    (↑1 : R[X])
have rcases : ∀ (w : Rˣ) (h2 : (C : (a : R) → R[X]) (↑w : R) = (↑u : R[X])),
  HMul.hMul (β := R[X]) (↑u : R[X]) ((C : (a : R) → R[X]) (↑(normUnit (↑u : R[X]).leadingCoeff) : R) : R[X]) =
    (↑1 : R[X])
Tactic: rcases Polynomial.isUnit_iff.1 ⟨u, rfl⟩ with ⟨_, ⟨w, rfl⟩, h2⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
u : R[X]ˣ
w : Rˣ
h2 : (C : (a : R) → R[X]) (↑w : R) = (↑u : R[X])
⊢ HMul.hMul (β := R[X]) (↑u : R[X]) ((C : (a : R) → R[X]) (↑(normUnit (↑u : R[X]).leadingCoeff) : R) : R[X]) =
    (↑1 : R[X])
have rw : Eq.{u + 1} (α := R[X]) 1 (↑1 : R[X])
Tactic: rw [← h2, leadingCoeff_C, normUnit_coe_units, ← C_mul, Units.mul_inv, C_1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NormalizationMonoid R
p : R[X]
⊢ roots ((normalize : (a : R[X]) → R[X]) p) = p.roots
have rw : (p * (↑(normUnit p) : R[X])).roots = p.roots
Tactic: rw [normalize_apply, mul_comm, coe_normUnit, roots_C_mul _ (normUnit (leadingCoeff p)).ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NormalizationMonoid R
p : R[X]
rw : (p * (↑(normUnit p) : R[X])).roots = p.roots
⊢ roots ((normalize : (a : R[X]) → R[X]) p) = p.roots
have rw₁ : ((↑(normUnit p) : R[X]) * p).roots = p.roots
Tactic: rw [normalize_apply, mul_comm, coe_normUnit, roots_C_mul _ (normUnit (leadingCoeff p)).ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NormalizationMonoid R
p : R[X]
rw : (p * (↑(normUnit p) : R[X])).roots = p.roots
rw₁ : ((↑(normUnit p) : R[X]) * p).roots = p.roots
⊢ roots ((normalize : (a : R[X]) → R[X]) p) = p.roots
have rw₂ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff) : R) : R[X]) p).roots = p.roots
Tactic: rw [normalize_apply, mul_comm, coe_normUnit, roots_C_mul _ (normUnit (leadingCoeff p)).ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : NormalizationMonoid R
p : R[X]
rw : (p * (↑(normUnit p) : R[X])).roots = p.roots
rw₁ : ((↑(normUnit p) : R[X]) * p).roots = p.roots
rw₂ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff) : R) : R[X]) p).roots = p.roots
⊢ roots ((normalize : (a : R[X]) → R[X]) p) = p.roots
have rw₃ : p.roots = p.roots
Tactic: rw [normalize_apply, mul_comm, coe_normUnit, roots_C_mul _ (normUnit (leadingCoeff p)).ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
⊢ Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
have this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑(normUnit (leadingCoeff X)) : R))
Tactic: have := coe_normUnit (R := R) (p := X)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑(normUnit (leadingCoeff X)) : R))
⊢ Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
have rwa : ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑(normUnit 1) : R))),
  Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
Tactic: rwa [leadingCoeff_X, normUnit_one, Units.val_one, map_one, Units.val_eq_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑(normUnit (leadingCoeff X)) : R))
rwa :
  ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑(normUnit 1) : R))),
    Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
⊢ Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
have rwa₁ : ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑1 : R))),
  Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
Tactic: rwa [leadingCoeff_X, normUnit_one, Units.val_one, map_one, Units.val_eq_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑(normUnit (leadingCoeff X)) : R))
rwa :
  ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑(normUnit 1) : R))),
    Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
rwa₁ :
  ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑1 : R))),
    Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
⊢ Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
have rwa₂ : ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) 1)),
  Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
Tactic: rwa [leadingCoeff_X, normUnit_one, Units.val_one, map_one, Units.val_eq_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑(normUnit (leadingCoeff X)) : R))
rwa :
  ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑(normUnit 1) : R))),
    Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
rwa₁ :
  ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑1 : R))),
    Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
rwa₂ :
  ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) 1)),
    Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
⊢ Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
have rwa₃ : ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) 1), Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
Tactic: rwa [leadingCoeff_X, normUnit_one, Units.val_one, map_one, Units.val_eq_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : NormalizationMonoid R
this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑(normUnit (leadingCoeff X)) : R))
rwa :
  ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑(normUnit 1) : R))),
    Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
rwa₁ :
  ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) (↑1 : R))),
    Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
rwa₂ :
  ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) ((C : (a : R) → R[X]) 1)),
    Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
rwa₃ : ∀ (this : Eq.{u + 1} (α := R[X]) (↑(normUnit X) : R[X]) 1), Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
⊢ Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
have rwa₄ : ∀ (this : Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1), Eq.{u + 1} (α := R[X]ˣ) (normUnit X) 1
Tactic: rwa [leadingCoeff_X, normUnit_one, Units.val_one, map_one, Units.val_eq_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : DivisionRing R
p : R[X]
hp0 : p ≠ 0
hp : ¬IsUnit p
h : p.degree ≤ 0
⊢ False
have hp0₁ : Ne (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])
Tactic: rw [eq_C_of_degree_le_zero h] at hp0 hp
Cleared hypotheses: hp0, hp, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : DivisionRing R
p : R[X]
hp0 : p ≠ 0
hp : ¬IsUnit p
h : p.degree ≤ 0
hp0₁ : Ne (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])
⊢ False
have hp₁ : ¬IsUnit (M := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
Tactic: rw [eq_C_of_degree_le_zero h] at hp0 hp
Cleared hypotheses: hp0, hp, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 = 0
⊢ False
have h₁ : degree.{u} (R := R) ((C : (a : R) → R[X]) 0) = 0
Tactic: rw [eq_C_of_degree_le_zero this, hc] at h
Cleared hypotheses: h, this, hc
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : Field R
p : R[X]
h : degree.{u} (R := R) ((C : (a : R) → R[X]) 0) = 0
this : p.degree ≤ 0
hc : p.coeff 0 = 0
⊢ False
have h₁ : degree.{u} (R := R) 0 = 0
Tactic: simp only [map_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 ≠ 0
| p
have rw : ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
Tactic: rw [eq_C_of_degree_le_zero this]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 ≠ 0
⊢ 1 = HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (p.coeff 0)⁻¹ : R[X])
have conv : 1 =
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
    ((C : (a : R) → R[X]) (p.coeff 0)⁻¹ : R[X])
Tactic: conv in p => rw [eq_C_of_degree_le_zero this]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 ≠ 0
⊢ 1 =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
      ((C : (a : R) → R[X]) (p.coeff 0)⁻¹ : R[X])
have rw : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (p.coeff 0 * (p.coeff 0)⁻¹) : R[X])
Tactic: rw [← C_mul, mul_inv_cancel₀ hc, C_1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 ≠ 0
rw : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (p.coeff 0 * (p.coeff 0)⁻¹) : R[X])
⊢ 1 =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
      ((C : (a : R) → R[X]) (p.coeff 0)⁻¹ : R[X])
have rw₁ : Eq.{u + 1} (α := R[X]) 1 ((C : (a : R) → R[X]) 1)
Tactic: rw [← C_mul, mul_inv_cancel₀ hc, C_1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p : R[X]
h : p.degree = 0
this : p.degree ≤ 0
hc : p.coeff 0 ≠ 0
rw : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (p.coeff 0 * (p.coeff 0)⁻¹) : R[X])
rw₁ : Eq.{u + 1} (α := R[X]) 1 ((C : (a : R) → R[X]) 1)
⊢ 1 =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
      ((C : (a : R) → R[X]) (p.coeff 0)⁻¹ : R[X])
have rw₂ : Eq.{u + 1} (α := R[X]) 1 1
Tactic: rw [← C_mul, mul_inv_cancel₀ hc, C_1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
⊢ q * p.div q + p.mod q = p
have pos : ∀ (h : q = 0), q * p.div q + p.mod q = p
Tactic: by_cases h : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
pos : ∀ (h : q = 0), q * p.div q + p.mod q = p
⊢ q * p.div q + p.mod q = p
have neg : ∀ (h : ¬q = 0), q * p.div q + p.mod q = p
Tactic: by_cases h : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
h : ¬q = 0
| q * p.div q + p.mod q = p
have rhs : p
Tactic: rhs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
h : ¬q = 0
| p
have rw : p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
  HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
    (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
Tactic: rw [← modByMonic_add_div p (q * C q.leadingCoeff⁻¹)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
h : ¬q = 0
| q * p.div q + p.mod q = p
have rw : p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
  HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
    (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
Tactic: rhs
      rw [← modByMonic_add_div p (q * C q.leadingCoeff⁻¹)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
h : ¬q = 0
⊢ q * p.div q + p.mod q = p
have neg : q * p.div q + p.mod q =
  p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
      (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
Tactic: conv =>
      rhs
      rw [← modByMonic_add_div p (q * C q.leadingCoeff⁻¹)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
h : ¬q = 0
⊢ q * p.div q + p.mod q =
    p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
have neg : q *
      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])) +
    p.mod q =
  p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
      (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
Tactic: rw [div, mod, add_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
h : ¬q = 0
neg :
  q *
        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])) +
      p.mod q =
    p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
⊢ q * p.div q + p.mod q =
    p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
have neg₁ : q *
      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])) +
    p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) =
  p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
      (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
Tactic: rw [div, mod, add_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
h : ¬q = 0
neg :
  q *
        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])) +
      p.mod q =
    p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
neg₁ :
  q *
        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])) +
      p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) =
    p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
⊢ q * p.div q + p.mod q =
    p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
have neg₂ : p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
    q *
      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])) =
  p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
      (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
Tactic: rw [div, mod, add_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
p q : R[X]
h : ¬q = 0
neg :
  q *
        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])) +
      p.mod q =
    p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
neg₁ :
  q *
        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])) +
      p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) =
    p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
neg₂ :
  p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      q *
        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])) =
    p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
⊢ q * p.div q + p.mod q =
    p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
      HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
        (p /ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
have neg₃ : p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
    q *
      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])) =
  p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) +
    q *
      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: rw [div, mod, add_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : Field R
q p : R[X]
hq : q ≠ 0
⊢ (p.mod q).degree < q.degree
have rw : (p.mod q).degree < (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree
Tactic: rw [← degree_mul_leadingCoeff_inv q hq]
-- 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 = p
have this : ¬(HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree
Tactic: have : ¬degree (q * C (leadingCoeff q)⁻¹) ≤ degree p :=
      not_le_of_gt <| by rwa [degree_mul_leadingCoeff_inv q 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
this : ¬(HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree
⊢ p % q = p
have rw : (p.divModByMonicAux (q := HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) sorry).2 = p
Tactic: rw [mod_def, modByMonic, dif_pos (monic_mul_leadingCoeff_inv hq0)]