awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw : q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (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]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) q)
Tactic: rw [mul_left_comm p, ← hr, ← mul_assoc, ← C.map_mul, inv_mul_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
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
rw : q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p * 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]) q)
⊢ q = 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]) * q
Tactic: rw [mul_left_comm p, ← hr, ← mul_assoc, ← C.map_mul, inv_mul_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
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
rw : q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p * 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]) q)
rw₂ : q = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) ((C : (a : R) → R[X]) a : R[X]) * q
⊢ 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⁻¹ * a) : R[X]) q
Tactic: rw [mul_left_comm p, ← hr, ← mul_assoc, ← C.map_mul, inv_mul_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
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
rw : q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p * 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]) q)
rw₂ : q = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) ((C : (a : R) → R[X]) a : R[X]) * q
rw₃ : q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a⁻¹ * a) : R[X]) q
⊢ q = p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) r
have rw₄ : q = (C : (a : R) → R[X]) 1 * q
Tactic: rw [mul_left_comm p, ← hr, ← mul_assoc, ← C.map_mul, inv_mul_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
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
rw : q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p * 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]) q)
rw₂ : q = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) ((C : (a : R) → R[X]) a : R[X]) * q
rw₃ : q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a⁻¹ * a) : R[X]) q
rw₄ : q = (C : (a : R) → R[X]) 1 * q
⊢ q = p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) r
have rw₅ : q = 1 * q
Tactic: rw [mul_left_comm p, ← hr, ← mul_assoc, ← C.map_mul, inv_mul_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
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
rw : q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) (p * 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]) q)
rw₂ : q = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) ((C : (a : R) → R[X]) a : R[X]) * q
rw₃ : q = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a⁻¹ * a) : R[X]) q
rw₄ : q = (C : (a : R) → R[X]) 1 * q
rw₅ : q = 1 * q
⊢ q = p * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) r
have rw₆ : q = q
Tactic: rw [mul_left_comm p, ← hr, ← mul_assoc, ← C.map_mul, inv_mul_cancel₀ ha, C.map_one,
        one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : Field R
p : R[X]
inst_1 : DecidableEq R
hp : p ≠ 0
⊢ (↑(normUnit p) : R[X]) = (C : (a : R) → R[X]) p.leadingCoeff⁻¹
have this : p.leadingCoeff ≠ 0
Tactic: have : p.leadingCoeff ≠ 0 := mt leadingCoeff_eq_zero.mp hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
⊢ map f x ∣ map f y ↔ x ∣ y
have pos : ∀ (H : x = 0), map f x ∣ map f y ↔ x ∣ y
Tactic: by_cases H : x = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
pos : ∀ (H : x = 0), map f x ∣ map f y ↔ x ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y
have neg : ∀ (H : ¬x = 0), map f x ∣ map f y ↔ x ∣ y
Tactic: by_cases H : x = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : x = 0
⊢ map f x ∣ map f y ↔ x ∣ y
have pos : map f 0 ∣ map f y ↔ 0 ∣ y
Tactic: rw [H, Polynomial.map_zero, zero_dvd_iff, zero_dvd_iff, Polynomial.map_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : x = 0
pos : map f 0 ∣ map f y ↔ 0 ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y
have pos₁ : 0 ∣ map f y ↔ 0 ∣ y
Tactic: rw [H, Polynomial.map_zero, zero_dvd_iff, zero_dvd_iff, Polynomial.map_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : x = 0
pos : map f 0 ∣ map f y ↔ 0 ∣ y
pos₁ : 0 ∣ map f y ↔ 0 ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y
have pos₂ : map f y = 0 ↔ 0 ∣ y
Tactic: rw [H, Polynomial.map_zero, zero_dvd_iff, zero_dvd_iff, Polynomial.map_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : x = 0
pos : map f 0 ∣ map f y ↔ 0 ∣ y
pos₁ : 0 ∣ map f y ↔ 0 ∣ y
pos₂ : map f y = 0 ↔ 0 ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y
have pos₃ : map f y = 0 ↔ y = 0
Tactic: rw [H, Polynomial.map_zero, zero_dvd_iff, zero_dvd_iff, Polynomial.map_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : x = 0
pos : map f 0 ∣ map f y ↔ 0 ∣ y
pos₁ : 0 ∣ map f y ↔ 0 ∣ y
pos₂ : map f y = 0 ↔ 0 ∣ y
pos₃ : map f y = 0 ↔ y = 0
⊢ map f x ∣ map f y ↔ x ∣ y
have pos₄ : y = 0 ↔ y = 0
Tactic: rw [H, Polynomial.map_zero, zero_dvd_iff, zero_dvd_iff, Polynomial.map_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
⊢ map f x ∣ map f y ↔ x ∣ y
have neg : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ x ∣ y
Tactic: rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
neg : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ x ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y
have neg₁ : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
Tactic: rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
neg : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ x ∣ y
neg₁ : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y
have neg₂ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
Tactic: rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
neg : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ x ∣ y
neg₁ : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₂ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y
have neg₃ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ x * (↑(normUnit x) : R[X]) ∣ y
Tactic: rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
neg : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ x ∣ y
neg₁ : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₂ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₃ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ x * (↑(normUnit x) : R[X]) ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y
have neg₄ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔
  HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
Tactic: rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
neg : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ x ∣ y
neg₁ : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₂ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₃ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ x * (↑(normUnit x) : R[X]) ∣ y
neg₄ :
  map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y
have neg₅ : HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) (map f x).leadingCoeff⁻¹ : k[X]) ∣ map f y ↔
  HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
Tactic: rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
neg : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ x ∣ y
neg₁ : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₂ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₃ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ x * (↑(normUnit x) : R[X]) ∣ y
neg₄ :
  map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₅ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) (map f x).leadingCoeff⁻¹ : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y
have neg₆ : HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) ((f : (a : R) → k) x.leadingCoeff)⁻¹ : k[X]) ∣ map f y ↔
  HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
Tactic: rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
neg : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ x ∣ y
neg₁ : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₂ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₃ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ x * (↑(normUnit x) : R[X]) ∣ y
neg₄ :
  map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₅ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) (map f x).leadingCoeff⁻¹ : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₆ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) ((f : (a : R) → k) x.leadingCoeff)⁻¹ : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y
have neg₇ : HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) ((f : (a : R) → k) x.leadingCoeff⁻¹) : k[X]) ∣ map f y ↔
  HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
Tactic: rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
neg : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ x ∣ y
neg₁ : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₂ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₃ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ x * (↑(normUnit x) : R[X]) ∣ y
neg₄ :
  map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₅ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) (map f x).leadingCoeff⁻¹ : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₆ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) ((f : (a : R) → k) x.leadingCoeff)⁻¹ : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₇ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) ((f : (a : R) → k) x.leadingCoeff⁻¹) : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y
have neg₈ : map f x * map f ((C : (a : R) → R[X]) x.leadingCoeff⁻¹) ∣ map f y ↔
  HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
Tactic: rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
neg : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ x ∣ y
neg₁ : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₂ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₃ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ x * (↑(normUnit x) : R[X]) ∣ y
neg₄ :
  map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₅ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) (map f x).leadingCoeff⁻¹ : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₆ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) ((f : (a : R) → k) x.leadingCoeff)⁻¹ : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₇ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) ((f : (a : R) → k) x.leadingCoeff⁻¹) : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₈ :
  map f x * map f ((C : (a : R) → R[X]) x.leadingCoeff⁻¹) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y
have neg₉ : map f (HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X])) ∣ map f y ↔
  HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
Tactic: rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
neg : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ x ∣ y
neg₁ : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₂ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
neg₃ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ x * (↑(normUnit x) : R[X]) ∣ y
neg₄ :
  map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₅ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) (map f x).leadingCoeff⁻¹ : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₆ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) ((f : (a : R) → k) x.leadingCoeff)⁻¹ : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₇ :
  HMul.hMul (β := k[X]) (map f x) ((C : (a : k) → k[X]) ((f : (a : R) → k) x.leadingCoeff⁻¹) : k[X]) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₈ :
  map f x * map f ((C : (a : R) → R[X]) x.leadingCoeff⁻¹) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
neg₉ :
  map f (HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X])) ∣ map f y ↔
    HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y
have neg₁₀ : HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y ↔
  HMul.hMul (β := R[X]) x ((C : (a : R) → R[X]) x.leadingCoeff⁻¹ : R[X]) ∣ y
Tactic: rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
⊢ map f x ∣ map f y ↔ x ∣ y
have neg : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ x ∣ y
Tactic: classical
    rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
neg : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ x ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y
have neg₁ : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
Tactic: classical
    rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
k : Type y
inst : Field R
inst_1 : Field k
f : R →+* k
x y : R[X]
H : ¬x = 0
neg : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ x ∣ y
neg₁ : (normalize : (a : k[X]) → k[X]) (map f x) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
⊢ map f x ∣ map f y ↔ x ∣ y
have neg₂ : map f x * (↑(normUnit (map f x)) : k[X]) ∣ map f y ↔ (normalize : (a : R[X]) → R[X]) x ∣ y
Tactic: classical
    rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X], normalize_apply, normalize_apply,
      coe_normUnit_of_ne_zero H, coe_normUnit_of_ne_zero (mt (Polynomial.map_eq_zero f).1 H),
      leadingCoeff_map, ← map_inv₀ f, ← map_C, ← Polynomial.map_mul,
      map_dvd_map _ f.injective (monic_mul_leadingCoeff_inv H)]