awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : ∀ m ≤ n, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)
zero :
  ∀ (hnzd : ∀ m ≤ 0, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)),
    Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑0! : R)
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R)
have succ : ∀ (n : ℕ)
  (ih :
    ∀ (hnzd : ∀ m ≤ n, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)),
      Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑n ! : R))
  (hnzd : ∀ m ≤ n + 1, m ≠ 0 → Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R)),
  Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(n + 1)! : R)
Tactic: induction n with
  | zero =>
    simp only [Nat.factorial_zero, Nat.cast_one]
    exact Submonoid.one_mem _
  | succ n ih =>
    rw [Nat.factorial_succ, Nat.cast_mul, mul_mem_nonZeroDivisors]
    exact ⟨hnzd _ le_rfl n.succ_ne_zero, ih fun m h ↦ hnzd m (h.trans n.le_succ)⟩
Cleared hypotheses: n, hnzd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑1! : R)
have rw : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) 1
Tactic: rw [Nat.factorial_one, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ 1 < rootMultiplicity t p ↔ p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t
have rw : (∀ m ≤ 1, ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t) ↔
  p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t
Tactic: rw [one_lt_rootMultiplicity_iff_isRoot_iterate_derivative h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
⊢ (∀ m ≤ 1, ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t) ↔
    p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t
have refine : p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t →
  ∀ (m : ℕ) (hm : m ≤ 1) (h0 : p.IsRoot t) (h1 : IsRoot ((derivative : (a : R[X]) → R[X]) p) t),
    ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t
Tactic: refine ⟨fun h ↦ ⟨h 0 (by simp), h 1 (by simp)⟩, fun ⟨h0, h1⟩ m hm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
h_1 : p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t
m : ℕ
hm : m ≤ 1
h0 : p.IsRoot t
h1 : IsRoot ((derivative : (a : R[X]) → R[X]) p) t
⊢ ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t
have zero : ∀ (hm : LE.le (α := ℕ) 0 1), ((⇑derivative : (a : R[X]) → R[X])^[0] p).IsRoot t
Tactic: obtain (_ | _ | m) := m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
h_1 : p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t
m : ℕ
hm : m ≤ 1
h0 : p.IsRoot t
h1 : IsRoot ((derivative : (a : R[X]) → R[X]) p) t
zero : ∀ (hm : LE.le (α := ℕ) 0 1), ((⇑derivative : (a : R[X]) → R[X])^[0] p).IsRoot t
⊢ ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t
have succ : ∀ (hm : HAdd.hAdd (α := ℕ) 0 1 ≤ 1), ((⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] p).IsRoot t
Tactic: obtain (_ | _ | m) := m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
h : p ≠ 0
h_1 : p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t
m : ℕ
hm : m ≤ 1
h0 : p.IsRoot t
h1 : IsRoot ((derivative : (a : R[X]) → R[X]) p) t
zero : ∀ (hm : LE.le (α := ℕ) 0 1), ((⇑derivative : (a : R[X]) → R[X])^[0] p).IsRoot t
succ : ∀ (hm : HAdd.hAdd (α := ℕ) 0 1 ≤ 1), ((⇑derivative : (a : R[X]) → R[X])^[HAdd.hAdd (α := ℕ) 0 1] p).IsRoot t
⊢ ((⇑derivative : (a : R[X]) → R[X])^[m] p).IsRoot t
have succ₁ : ∀ (m : ℕ) (hm : m + 1 + 1 ≤ 1), ((⇑derivative : (a : R[X]) → R[X])^[m + 1 + 1] p).IsRoot t
Tactic: obtain (_ | _ | m) := m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : GCDMonoid R[X]
p : R[X]
t : R
h : p ≠ 0
⊢ 1 < rootMultiplicity t p ↔
    (@gcd _ CommSemiring.toCommMonoidWithZero _ p ((derivative : (a : R[X]) → R[X]) p)).IsRoot t
have simp_rw : p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t ↔
  (@gcd _ CommSemiring.toCommMonoidWithZero _ p ((derivative : (a : R[X]) → R[X]) p)).IsRoot t
Tactic: simp_rw [one_lt_rootMultiplicity_iff_isRoot h, ← dvd_iff_isRoot, dvd_gcd_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : GCDMonoid R[X]
p : R[X]
t : R
h : p ≠ 0
simp_rw :
  p.IsRoot t ∧ IsRoot ((derivative : (a : R[X]) → R[X]) p) t ↔
    (@gcd _ CommSemiring.toCommMonoidWithZero _ p ((derivative : (a : R[X]) → R[X]) p)).IsRoot t
⊢ 1 < rootMultiplicity t p ↔
    (@gcd _ CommSemiring.toCommMonoidWithZero _ p ((derivative : (a : R[X]) → R[X]) p)).IsRoot t
have simp_rw₁ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ p ∧
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ (derivative : (a : R[X]) → R[X]) p ↔
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣
    @gcd _ CommSemiring.toCommMonoidWithZero _ p ((derivative : (a : R[X]) → R[X]) p)
Tactic: simp_rw [one_lt_rootMultiplicity_iff_isRoot h, ← dvd_iff_isRoot, dvd_gcd_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
have pos : ∀ (h : p = 0), rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
pos : ∀ (h : p = 0), rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
have neg : ∀ (h : ¬p = 0), rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
Tactic: by_cases h : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
h : p = 0
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
have pos : rootMultiplicity t ((derivative : (a : R[X]) → R[X]) 0) = rootMultiplicity t 0 - 1
Tactic: rw [h, map_zero, rootMultiplicity_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
h : p = 0
pos : rootMultiplicity t ((derivative : (a : R[X]) → R[X]) 0) = rootMultiplicity t 0 - 1
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
have pos₁ : rootMultiplicity t 0 = rootMultiplicity t 0 - 1
Tactic: rw [h, map_zero, rootMultiplicity_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
h : p = 0
pos : rootMultiplicity t ((derivative : (a : R[X]) → R[X]) 0) = rootMultiplicity t 0 - 1
pos₁ : rootMultiplicity t 0 = rootMultiplicity t 0 - 1
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
have pos₂ : 0 = HSub.hSub (α := ℕ) 0 1
Tactic: rw [h, map_zero, rootMultiplicity_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
p : R[X]
t : R
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p)
have pos : ∀ (h : p.IsRoot t), rootMultiplicity t p - 1 ≤ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p)
Tactic: by_cases h : p.IsRoot t
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
p : R[X]
t : R
pos : ∀ (h : p.IsRoot t), rootMultiplicity t p - 1 ≤ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p)
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p)
have neg : ∀ (h : ¬p.IsRoot t), rootMultiplicity t p - 1 ≤ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p)
Tactic: by_cases h : p.IsRoot t
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
hfd : f ∣ HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g
a : R
haf : f.IsRoot a
⊢ g.IsRoot a
have rcases : ∀ (r : R[X]) (hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r), g.IsRoot a
Tactic: rcases hfd with ⟨r, hr⟩
Cleared hypotheses: hfd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
⊢ Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
have contrapose : ∀ (haf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])), ¬f.IsRoot a
Tactic: contrapose haf
Cleared hypotheses: haf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
haf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
⊢ ¬f.IsRoot a
have rw : ∀ (hf0 : Ne (α := R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X]) (0 : R[X])) {a : R} (r : R[X])
  (hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r)
  (haf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])),
  ¬IsRoot ((C : (a : R) → R[X]) (f.coeff 0)) a
Tactic: rw [eq_C_of_derivative_eq_zero haf] at hf0 ⊢
Cleared hypotheses: hf0, a, r, hr, haf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
⊢ g.IsRoot a
have hdf0 : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
Tactic: have hdf0 : derivative f ≠ 0 := by
    contrapose haf
    rw [eq_C_of_derivative_eq_zero haf] at hf0 ⊢
    exact not_isRoot_C _ _ <| C_ne_zero.mp hf0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
hdf0 : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
⊢ g.IsRoot a
have by_contra : ∀ (hg : ¬g.IsRoot a), False
Tactic: by_contra hg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
hdf0 : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hg : ¬g.IsRoot a
⊢ False
have hdfg0 : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g ≠ 0
Tactic: have hdfg0 : f.derivative * g ≠ 0 := mul_ne_zero hdf0 (by rintro rfl; simp at hg)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
hdf0 : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hg : ¬g.IsRoot a
hdfg0 : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g ≠ 0
⊢ False
have hr' : rootMultiplicity a (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g) = rootMultiplicity a (f * r)
Tactic: have hr' := congr_arg (rootMultiplicity a) hr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
hdf0 : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hg : ¬g.IsRoot a
hdfg0 : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g ≠ 0
hr' :
  rootMultiplicity a (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g) = rootMultiplicity a (f * r)
⊢ False
have this : IsDomain R
Tactic: have : IsDomain R := {}
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : NoZeroDivisors R
inst_2 : CharZero R
f g : R[X]
hf0 : f ≠ 0
a : R
haf : f.IsRoot a
r : R[X]
hr : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g = f * r
hdf0 : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hg : ¬g.IsRoot a
hdfg0 : HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g ≠ 0
hr' :
  rootMultiplicity a (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g) = rootMultiplicity a (f * r)
this : IsDomain R
⊢ False
have hr'₁ : rootMultiplicity a f = rootMultiplicity a r + rootMultiplicity a f + Nat.succ 0
Tactic: rw [rootMultiplicity_mul hdfg0, derivative_rootMultiplicity_of_root haf,
    rootMultiplicity_eq_zero hg, add_zero, rootMultiplicity_mul (hr ▸ hdfg0), add_comm,
    Nat.sub_eq_iff_eq_add (Nat.succ_le_iff.2 ((rootMultiplicity_pos hf0).2 haf))] at hr'
Cleared hypotheses: hr', this
-- 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
p : R[X]
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff) : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff)⁻¹ : R) : R[X]) =
    1
have rw : Eq (α := R[X]) ((C : (a : R) → R[X]) ((↑(normUnit p.leadingCoeff) : R) * (↑(normUnit p.leadingCoeff)⁻¹ : R)) : R[X])
  (1 : R[X])
Tactic: rw [← map_mul, Units.mul_inv, C_1]
-- 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
p : R[X]
rw :
  Eq (α := R[X]) ((C : (a : R) → R[X]) ((↑(normUnit p.leadingCoeff) : R) * (↑(normUnit p.leadingCoeff)⁻¹ : R)) : R[X])
    (1 : R[X])
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff) : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff)⁻¹ : R) : R[X]) =
    1
have rw₁ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1
Tactic: rw [← map_mul, Units.mul_inv, C_1]
-- 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
p : R[X]
rw :
  Eq (α := R[X]) ((C : (a : R) → R[X]) ((↑(normUnit p.leadingCoeff) : R) * (↑(normUnit p.leadingCoeff)⁻¹ : R)) : R[X])
    (1 : R[X])
rw₁ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff) : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff)⁻¹ : R) : R[X]) =
    1
have rw₂ : Eq.{u + 1} (α := R[X]) 1 1
Tactic: rw [← map_mul, Units.mul_inv, C_1]
-- 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
p : R[X]
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff)⁻¹ : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff) : R) : R[X]) =
    1
have rw : Eq (α := R[X]) ((C : (a : R) → R[X]) ((↑(normUnit p.leadingCoeff)⁻¹ : R) * (↑(normUnit p.leadingCoeff) : R)) : R[X])
  (1 : R[X])
Tactic: rw [← map_mul, Units.inv_mul, C_1]
-- 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
p : R[X]
rw :
  Eq (α := R[X]) ((C : (a : R) → R[X]) ((↑(normUnit p.leadingCoeff)⁻¹ : R) * (↑(normUnit p.leadingCoeff) : R)) : R[X])
    (1 : R[X])
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff)⁻¹ : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff) : R) : R[X]) =
    1
have rw₁ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1
Tactic: rw [← map_mul, Units.inv_mul, C_1]
-- 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
p : R[X]
rw :
  Eq (α := R[X]) ((C : (a : R) → R[X]) ((↑(normUnit p.leadingCoeff)⁻¹ : R) * (↑(normUnit p.leadingCoeff) : R)) : R[X])
    (1 : R[X])
rw₁ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff)⁻¹ : R) : R[X])
      ((C : (a : R) → R[X]) (↑(normUnit p.leadingCoeff) : R) : R[X]) =
    1
have rw₂ : Eq.{u + 1} (α := R[X]) 1 1
Tactic: rw [← map_mul, Units.inv_mul, C_1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
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 ≠ 0
hq0 : b_1 ≠ 0
⊢ (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 hp0₁ : ¬a_1.leadingCoeff = 0
Tactic: rw [Ne, ← leadingCoeff_eq_zero] at *
Cleared hypotheses: hp0, hq0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (hypothesis)
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 ≠ 0
hq0 : b_1 ≠ 0
hp0₁ : ¬a_1.leadingCoeff = 0
⊢ (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 hq0₁ : ¬b_1.leadingCoeff = 0
Tactic: rw [Ne, ← leadingCoeff_eq_zero] at *
Cleared hypotheses: hp0, hq0
-- 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
⊢ (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 : (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])
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
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])
⊢ (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₁ : (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])
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
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])
⊢ (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₂ : (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])
Tactic: rw [leadingCoeff_mul, normUnit_mul hp0 hq0, Units.val_mul, C_mul]