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
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]))
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]))
⊢ 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₀]
-- 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
⊢ map f (p / q) = map f p / map f q
have if : ∀ (hq0 : q = 0), map f (p / q) = map f p / map f q
Tactic: if hq0 : q = 0 then simp [hq0]
  else
    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
if : ∀ (hq0 : q = 0), map f (p / q) = map f p / map f q
⊢ map f (p / q) = map f p / map f q
have if₁ : ∀ (hq0 : ¬q = 0), map f (p / q) = map f p / map f q
Tactic: if hq0 : q = 0 then simp [hq0]
  else
    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
⊢ map f (p % q) = map f p % map f q
have pos : ∀ (hq0 : q = 0), map f (p % q) = map f p % map f q
Tactic: by_cases hq0 : q = 0
-- 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
pos : ∀ (hq0 : q = 0), map f (p % q) = map f p % map f q
⊢ map f (p % q) = map f p % map f q
have neg : ∀ (hq0 : ¬q = 0), map f (p % q) = map f p % map f q
Tactic: by_cases hq0 : q = 0
-- 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 neg : map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) = map f p % map f q
Tactic: rw [mod_def, mod_def, leadingCoeff_map f, ← map_inv₀ f, ← map_C f, ← Polynomial.map_mul f,
      map_modByMonic f (monic_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 q : R[X]
inst_1 : Field k
f : R →+* k
hq0 : ¬q = 0
neg : map f (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 neg₁ : map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
  map f p %ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
Tactic: rw [mod_def, mod_def, leadingCoeff_map f, ← map_inv₀ f, ← map_C f, ← Polynomial.map_mul f,
      map_modByMonic f (monic_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 q : R[X]
inst_1 : Field k
f : R →+* k
hq0 : ¬q = 0
neg : map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) = map f p % map f q
neg₁ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[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 neg₂ : map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[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 [mod_def, mod_def, leadingCoeff_map f, ← map_inv₀ f, ← map_C f, ← Polynomial.map_mul f,
      map_modByMonic f (monic_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 q : R[X]
inst_1 : Field k
f : R →+* k
hq0 : ¬q = 0
neg : map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) = map f p % map f q
neg₁ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
neg₂ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff)⁻¹ : k[X])
⊢ map f (p % q) = map f p % map f q
have neg₃ : map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[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 [mod_def, mod_def, leadingCoeff_map f, ← map_inv₀ f, ← map_C f, ← Polynomial.map_mul f,
      map_modByMonic f (monic_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 q : R[X]
inst_1 : Field k
f : R →+* k
hq0 : ¬q = 0
neg : map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) = map f p % map f q
neg₁ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
neg₂ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff)⁻¹ : k[X])
neg₃ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff⁻¹) : k[X])
⊢ map f (p % q) = map f p % map f q
have neg₄ : map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
  map f p %ₘ (map f q * map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹))
Tactic: rw [mod_def, mod_def, leadingCoeff_map f, ← map_inv₀ f, ← map_C f, ← Polynomial.map_mul f,
      map_modByMonic f (monic_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 q : R[X]
inst_1 : Field k
f : R →+* k
hq0 : ¬q = 0
neg : map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) = map f p % map f q
neg₁ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
neg₂ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff)⁻¹ : k[X])
neg₃ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff⁻¹) : k[X])
neg₄ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ (map f q * map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹))
⊢ map f (p % q) = map f p % map f q
have neg₅ : map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
  map f p %ₘ map f (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
Tactic: rw [mod_def, mod_def, leadingCoeff_map f, ← map_inv₀ f, ← map_C f, ← Polynomial.map_mul f,
      map_modByMonic f (monic_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 q : R[X]
inst_1 : Field k
f : R →+* k
hq0 : ¬q = 0
neg : map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) = map f p % map f q
neg₁ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) (map f q).leadingCoeff⁻¹ : k[X])
neg₂ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff)⁻¹ : k[X])
neg₃ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ HMul.hMul (β := k[X]) (map f q) ((C : (a : k) → k[X]) ((f : (a : R) → k) q.leadingCoeff⁻¹) : k[X])
neg₄ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ (map f q * map f ((C : (a : R) → R[X]) q.leadingCoeff⁻¹))
neg₅ :
  map f (p %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
    map f p %ₘ map f (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
⊢ map f (p % q) = map f p % map f q
have neg₆ : map f p %ₘ map f (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) =
  map f p %ₘ map f (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]))
Tactic: rw [mod_def, mod_def, leadingCoeff_map f, ← map_inv₀ f, ← map_C f, ← Polynomial.map_mul f,
      map_modByMonic f (monic_mul_leadingCoeff_inv hq0)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
⊢ q.leadingCoeff ≠ 0
have rw : q ≠ 0
Tactic: rw [leadingCoeff_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
⊢ q ≠ 0
have contrapose : ∀ (hq : q = 0), q.natDegree = 0
Tactic: contrapose hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
⊢ (p % q).natDegree < q.natDegree
have hq' : q.leadingCoeff ≠ 0
Tactic: have hq' : q.leadingCoeff ≠ 0 := by
    rw [leadingCoeff_ne_zero]
    contrapose hq
    simp [hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (p %ₘ HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).natDegree < q.natDegree
have refine_1 : (HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).Monic
Tactic: refine (natDegree_modByMonic_lt p ?_ ?_).trans_le ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
refine_1 : (HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).Monic
⊢ (p %ₘ HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).natDegree < q.natDegree
have refine_2 : HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X]) ≠ 1
Tactic: refine (natDegree_modByMonic_lt p ?_ ?_).trans_le ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
refine_1 : (HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).Monic
refine_2 : HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X]) ≠ 1
⊢ (p %ₘ HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).natDegree < q.natDegree
have refine_3 : (HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).natDegree ≤ q.natDegree
Tactic: refine (natDegree_modByMonic_lt p ?_ ?_).trans_le ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ (HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).Monic
have refine_1 : q.leadingCoeff * q.leadingCoeff⁻¹ = 1
Tactic: refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ q.leadingCoeff * q.leadingCoeff⁻¹ = 1
have refine_1 : q.leadingCoeff = q.leadingCoeff
Tactic: rw [mul_inv_eq_one₀ hq']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
k : Type y
inst : Field k
p q : k[X]
hq : q.natDegree ≠ 0
hq' : q.leadingCoeff ≠ 0
⊢ HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X]) ≠ 1
have refine_2 : ∀ (hq : HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X]) = 1), q.natDegree = 0
Tactic: contrapose hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
k : Type y
inst : Field k
p q : k[X]
hq' : q.leadingCoeff ≠ 0
hq : HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X]) = 1
⊢ q.natDegree = 0
have refine_2 : (HMul.hMul (β := k[X]) q ((C : (a : k) → k[X]) q.leadingCoeff⁻¹ : k[X])).natDegree = 0
Tactic: rw [← natDegree_mul_C_eq_of_mul_eq_one ((inv_mul_eq_one₀ hq').mpr rfl)]
-- 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 %ₘ HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree < q.degree
have refine : (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).Monic
Tactic: refine (Polynomial.degree_modByMonic_lt p ?_).trans_eq (by simp)
-- 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
inst_2 : DecidableEq R
inst_3 : DecidableEq k
f : R →+* k
x : R[X]
⊢ EuclideanDomain.gcd (map f 0) (map f x) = map f (EuclideanDomain.gcd 0 x)
have simp_rw : EuclideanDomain.gcd 0 (map f x) = map f (EuclideanDomain.gcd 0 x)
Tactic: simp_rw [Polynomial.map_zero, EuclideanDomain.gcd_zero_left]
-- 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
inst_2 : DecidableEq R
inst_3 : DecidableEq k
f : R →+* k
x y : R[X]
h : x ≠ 0
ih : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd (y % x) x)
⊢ EuclideanDomain.gcd (map f x) (map f y) = map f (EuclideanDomain.gcd x y)
have rw : EuclideanDomain.gcd (map f y % map f x) (map f x) = map f (EuclideanDomain.gcd x y)
Tactic: rw [gcd_val, ← map_mod, ih, ← gcd_val]
-- 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
inst_2 : DecidableEq R
inst_3 : DecidableEq k
f : R →+* k
x y : R[X]
h : x ≠ 0
ih : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd (y % x) x)
rw : EuclideanDomain.gcd (map f y % map f x) (map f x) = map f (EuclideanDomain.gcd x y)
⊢ EuclideanDomain.gcd (map f x) (map f y) = map f (EuclideanDomain.gcd x y)
have rw₁ : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd x y)
Tactic: rw [gcd_val, ← map_mod, ih, ← gcd_val]
-- 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
inst_2 : DecidableEq R
inst_3 : DecidableEq k
f : R →+* k
x y : R[X]
h : x ≠ 0
ih : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd (y % x) x)
rw : EuclideanDomain.gcd (map f y % map f x) (map f x) = map f (EuclideanDomain.gcd x y)
rw₁ : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd x y)
⊢ EuclideanDomain.gcd (map f x) (map f y) = map f (EuclideanDomain.gcd x y)
have rw₂ : map f (EuclideanDomain.gcd (y % x) x) = map f (EuclideanDomain.gcd x y)
Tactic: rw [gcd_val, ← map_mod, ih, ← gcd_val]
-- 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
inst_2 : DecidableEq R
inst_3 : DecidableEq k
f : R →+* k
x y : R[X]
h : x ≠ 0
ih : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd (y % x) x)
rw : EuclideanDomain.gcd (map f y % map f x) (map f x) = map f (EuclideanDomain.gcd x y)
rw₁ : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd x y)
rw₂ : map f (EuclideanDomain.gcd (y % x) x) = map f (EuclideanDomain.gcd x y)
⊢ EuclideanDomain.gcd (map f x) (map f y) = map f (EuclideanDomain.gcd x y)
have rw₃ : map f (EuclideanDomain.gcd x y) = map f (EuclideanDomain.gcd x y)
Tactic: rw [gcd_val, ← map_mod, ih, ← gcd_val]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hf : eval₂ ϕ α f = 0
hg : eval₂ ϕ α g = 0
⊢ eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
have rw : eval₂ ϕ α (f * EuclideanDomain.gcdA f g + g * EuclideanDomain.gcdB f g) = 0
Tactic: rw [EuclideanDomain.gcd_eq_gcd_ab f g, Polynomial.eval₂_add, Polynomial.eval₂_mul,
    Polynomial.eval₂_mul, hf, hg, zero_mul, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hf : eval₂ ϕ α f = 0
hg : eval₂ ϕ α g = 0
rw : eval₂ ϕ α (f * EuclideanDomain.gcdA f g + g * EuclideanDomain.gcdB f g) = 0
⊢ eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
have rw₁ : eval₂ ϕ α (f * EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
Tactic: rw [EuclideanDomain.gcd_eq_gcd_ab f g, Polynomial.eval₂_add, Polynomial.eval₂_mul,
    Polynomial.eval₂_mul, hf, hg, zero_mul, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hf : eval₂ ϕ α f = 0
hg : eval₂ ϕ α g = 0
rw : eval₂ ϕ α (f * EuclideanDomain.gcdA f g + g * EuclideanDomain.gcdB f g) = 0
rw₁ : eval₂ ϕ α (f * EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
⊢ eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
have rw₂ : eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
Tactic: rw [EuclideanDomain.gcd_eq_gcd_ab f g, Polynomial.eval₂_add, Polynomial.eval₂_mul,
    Polynomial.eval₂_mul, hf, hg, zero_mul, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hf : eval₂ ϕ α f = 0
hg : eval₂ ϕ α g = 0
rw : eval₂ ϕ α (f * EuclideanDomain.gcdA f g + g * EuclideanDomain.gcdB f g) = 0
rw₁ : eval₂ ϕ α (f * EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
rw₂ : eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
⊢ eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
have rw₃ : eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α g * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
Tactic: rw [EuclideanDomain.gcd_eq_gcd_ab f g, Polynomial.eval₂_add, Polynomial.eval₂_mul,
    Polynomial.eval₂_mul, hf, hg, zero_mul, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hf : eval₂ ϕ α f = 0
hg : eval₂ ϕ α g = 0
rw : eval₂ ϕ α (f * EuclideanDomain.gcdA f g + g * EuclideanDomain.gcdB f g) = 0
rw₁ : eval₂ ϕ α (f * EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
rw₂ : eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
rw₃ : eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α g * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
⊢ eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
have rw₄ : 0 * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α g * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
Tactic: rw [EuclideanDomain.gcd_eq_gcd_ab f g, Polynomial.eval₂_add, Polynomial.eval₂_mul,
    Polynomial.eval₂_mul, hf, hg, zero_mul, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : CommSemiring k
inst_2 : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hf : eval₂ ϕ α f = 0
hg : eval₂ ϕ α g = 0
rw : eval₂ ϕ α (f * EuclideanDomain.gcdA f g + g * EuclideanDomain.gcdB f g) = 0
rw₁ : eval₂ ϕ α (f * EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
rw₂ : eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α (g * EuclideanDomain.gcdB f g) = 0
rw₃ : eval₂ ϕ α f * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α g * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
rw₄ : 0 * eval₂ ϕ α (EuclideanDomain.gcdA f g) + eval₂ ϕ α g * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
⊢ eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
have rw₅ : 0 * eval₂ ϕ α (EuclideanDomain.gcdA f g) + 0 * eval₂ ϕ α (EuclideanDomain.gcdB f g) = 0
Tactic: rw [EuclideanDomain.gcd_eq_gcd_ab f g, Polynomial.eval₂_add, Polynomial.eval₂_mul,
    Polynomial.eval₂_mul, hf, hg, zero_mul, zero_mul, zero_add]