awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ p.natDegree
h : j < p.natDegree
⊢ (↑(den A r) : A) ∣ (p.scaleRoots (↑(den A r) : A)).coeff j * num A r ^ j
have pos : (↑(den A r) : A) ∣ p.coeff j * (↑(den A r) : A) ^ (p.natDegree - j) * num A r ^ j
Tactic: rw [coeff_scaleRoots]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ p.natDegree
h : j < p.natDegree
⊢ (↑(den A r) : A) ∣ p.coeff j * (↑(den A r) : A) ^ (p.natDegree - j) * num A r ^ j
have pos : (↑(den A r) : A) ∣ (↑(den A r) : A) ^ (p.natDegree - j)
Tactic: refine (dvd_mul_of_dvd_right ?_ _).mul_right _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ p.natDegree
h : j < p.natDegree
⊢ (↑(den A r) : A) ∣ (↑(den A r) : A) ^ (p.natDegree - j)
have h₁ : (↑(den A r) : A) = (↑(den A r) : A) ^ Nat.succ 0
Tactic: convert! pow_dvd_pow (den A r : A) (Nat.succ_le_iff.mpr (lt_tsub_iff_left.mpr _))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ p.natDegree
h : j < p.natDegree
h₁ : (↑(den A r) : A) = (↑(den A r) : A) ^ Nat.succ 0
pos : ℕ
⊢ (↑(den A r) : A) ∣ (↑(den A r) : A) ^ (p.natDegree - j)
have pos₁ : j + 0 < p.natDegree
Tactic: convert! pow_dvd_pow (den A r : A) (Nat.succ_le_iff.mpr (lt_tsub_iff_left.mpr _))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (hypothesis)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ p.natDegree
h : p.natDegree ≤ j
⊢ (↑(den A r) : A) ∣ (p.scaleRoots (↑(den A r) : A)).coeff j * num A r ^ j
have hj₁ : j ≠ (p.scaleRoots (↑(den A r) : A)).natDegree
Tactic: rw [← natDegree_scaleRoots p (den A r)] at *
Cleared hypotheses: hj, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (hypothesis)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ p.natDegree
h : p.natDegree ≤ j
hj₁ : j ≠ (p.scaleRoots (↑(den A r) : A)).natDegree
⊢ (↑(den A r) : A) ∣ (p.scaleRoots (↑(den A r) : A)).coeff j * num A r ^ j
have h₁ : (p.scaleRoots (↑(den A r) : A)).natDegree ≤ j
Tactic: rw [← natDegree_scaleRoots p (den A r)] at *
Cleared hypotheses: hj, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
j : ℕ
hj : j ≠ (p.scaleRoots (↑(den A r) : A)).natDegree
h : (p.scaleRoots (↑(den A r) : A)).natDegree ≤ j
⊢ (↑(den A r) : A) ∣ (p.scaleRoots (↑(den A r) : A)).coeff j * num A r ^ j
have neg : (↑(den A r) : A) ∣ 0
Tactic: rw [coeff_eq_zero_of_natDegree_lt (lt_of_le_of_ne h hj.symm),
    zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
⊢ ∃ (r' : A), r = (algebraMap A K : (a : A) → K) r' ∧ r' ∣ p.coeff 0
have obtain : ∀ (inv : A) (h_inv : 1 = (↑(den A r) : A) * inv), ∃ (r' : A), r = (algebraMap A K : (a : A) → K) r' ∧ r' ∣ p.coeff 0
Tactic: obtain ⟨inv, h_inv⟩ := hp ▸ den_dvd_of_is_root hr
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
⊢ ∃ (r' : A), r = (algebraMap A K : (a : A) → K) r' ∧ r' ∣ p.coeff 0
have right : num A r * inv ∣ p.coeff 0
Tactic: use num A r * inv, ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
right : num A r * inv ∣ p.coeff 0
⊢ ∃ (r' : A), r = (algebraMap A K : (a : A) → K) r' ∧ r' ∣ p.coeff 0
have left : r = (algebraMap A K : (a : A) → K) (num A r * inv)
Tactic: use num A r * inv, ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (hypothesis)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
⊢ num A r * inv ∣ p.coeff 0
have h : inv ∣ 1
Tactic: have h : inv ∣ 1 := ⟨den A r, by simpa [mul_comm] using h_inv⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (hypothesis)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
⊢ r = (algebraMap A K : (a : A) → K) (num A r * inv)
have d_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) (0 : K)
Tactic: have d_ne_zero : algebraMap A K (den A r) ≠ 0 :=
      IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors (den A r).prop
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
d_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) (0 : K)
⊢ r = (algebraMap A K : (a : A) → K) (num A r * inv)
have left : HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
    ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) =
  (algebraMap A K : (a : A) → K) (num A r * inv)
Tactic: nth_rw 1 [← mk'_num_den' A r]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
d_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) (0 : K)
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) =
    (algebraMap A K : (a : A) → K) (num A r * inv)
have left : (algebraMap A K : (a : A) → K) (num A r) =
  HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r * inv) : K)
    ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
Tactic: rw [div_eq_iff d_ne_zero, map_mul, mul_assoc, mul_comm ((algebraMap A K) inv),
      ← map_mul, ← h_inv, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
d_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) (0 : K)
left :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r * inv) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) =
    (algebraMap A K : (a : A) → K) (num A r * inv)
have left₁ : (algebraMap A K : (a : A) → K) (num A r) =
  HMul.hMul (β := K)
    (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      ((algebraMap A K : (a : A) → K) inv : K))
    ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
Tactic: rw [div_eq_iff d_ne_zero, map_mul, mul_assoc, mul_comm ((algebraMap A K) inv),
      ← map_mul, ← h_inv, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
d_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) (0 : K)
left :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r * inv) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
left₁ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
        ((algebraMap A K : (a : A) → K) inv : K))
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) =
    (algebraMap A K : (a : A) → K) (num A r * inv)
have left₂ : (algebraMap A K : (a : A) → K) (num A r) =
  HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
    (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) inv : K)
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K))
Tactic: rw [div_eq_iff d_ne_zero, map_mul, mul_assoc, mul_comm ((algebraMap A K) inv),
      ← map_mul, ← h_inv, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
d_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) (0 : K)
left :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r * inv) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
left₁ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
        ((algebraMap A K : (a : A) → K) inv : K))
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
left₂ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) inv : K)
        ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K))
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) =
    (algebraMap A K : (a : A) → K) (num A r * inv)
have left₃ : (algebraMap A K : (a : A) → K) (num A r) =
  HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
    (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
      ((algebraMap A K : (a : A) → K) inv : K))
Tactic: rw [div_eq_iff d_ne_zero, map_mul, mul_assoc, mul_comm ((algebraMap A K) inv),
      ← map_mul, ← h_inv, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
d_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) (0 : K)
left :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r * inv) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
left₁ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
        ((algebraMap A K : (a : A) → K) inv : K))
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
left₂ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) inv : K)
        ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K))
left₃ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
        ((algebraMap A K : (a : A) → K) inv : K))
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) =
    (algebraMap A K : (a : A) → K) (num A r * inv)
have left₄ : (algebraMap A K : (a : A) → K) (num A r) =
  HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
    ((algebraMap A K : (a : A) → K) ((↑(den A r) : A) * inv) : K)
Tactic: rw [div_eq_iff d_ne_zero, map_mul, mul_assoc, mul_comm ((algebraMap A K) inv),
      ← map_mul, ← h_inv, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
d_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) (0 : K)
left :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r * inv) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
left₁ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
        ((algebraMap A K : (a : A) → K) inv : K))
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
left₂ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) inv : K)
        ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K))
left₃ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
        ((algebraMap A K : (a : A) → K) inv : K))
left₄ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      ((algebraMap A K : (a : A) → K) ((↑(den A r) : A) * inv) : K)
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) =
    (algebraMap A K : (a : A) → K) (num A r * inv)
have left₅ : (algebraMap A K : (a : A) → K) (num A r) =
  HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K) ((algebraMap A K : (a : A) → K) 1 : K)
Tactic: rw [div_eq_iff d_ne_zero, map_mul, mul_assoc, mul_comm ((algebraMap A K) inv),
      ← map_mul, ← h_inv, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
d_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) (0 : K)
left :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r * inv) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
left₁ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
        ((algebraMap A K : (a : A) → K) inv : K))
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
left₂ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) inv : K)
        ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K))
left₃ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
        ((algebraMap A K : (a : A) → K) inv : K))
left₄ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      ((algebraMap A K : (a : A) → K) ((↑(den A r) : A) * inv) : K)
left₅ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K) ((algebraMap A K : (a : A) → K) 1 : K)
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) =
    (algebraMap A K : (a : A) → K) (num A r * inv)
have left₆ : (algebraMap A K : (a : A) → K) (num A r) =
  HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K) (1 : K)
Tactic: rw [div_eq_iff d_ne_zero, map_mul, mul_assoc, mul_comm ((algebraMap A K) inv),
      ← map_mul, ← h_inv, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.RationalRoot (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
inst_1 : IsDomain A
inst_2 : UniqueFactorizationMonoid A
inst_3 : Field K
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
p : A[X]
hp : p.Monic
r : K
hr : Eq.{u_2 + 1} (α := K) ((aeval r : (a : A[X]) → K) p : K) (0 : K)
inv : A
h_inv : 1 = (↑(den A r) : A) * inv
d_ne_zero : Ne.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) (0 : K)
left :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r * inv) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
left₁ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
        ((algebraMap A K : (a : A) → K) inv : K))
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
left₂ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) inv : K)
        ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K))
left₃ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      (HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K)
        ((algebraMap A K : (a : A) → K) inv : K))
left₄ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      ((algebraMap A K : (a : A) → K) ((↑(den A r) : A) * inv) : K)
left₅ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K) ((algebraMap A K : (a : A) → K) 1 : K)
left₆ :
  (algebraMap A K : (a : A) → K) (num A r) =
    HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K) (1 : K)
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) (num A r) : K)
      ((algebraMap A K : (a : A) → K) (↑(den A r) : A) : K) =
    (algebraMap A K : (a : A) → K) (num A r * inv)
have left₇ : Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) (num A r) : K) ((algebraMap A K : (a : A) → K) (num A r) : K)
Tactic: rw [div_eq_iff d_ne_zero, map_mul, mul_assoc, mul_comm ((algebraMap A K) inv),
      ← map_mul, ← h_inv, map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
f g : R[X]
m : ℕ
i j_1 : Fin (0 + m)
j : Fin m
⊢ f.sylvester g 0 m i (Fin.natAdd 0 j) = Matrix.diagonal (fun (x : Fin (0 + m)) ↦ f.coeff 0) i (Fin.natAdd 0 j)
have rw : (if (↑i : ℕ) ∈ Icc (↑j : ℕ) ((↑j : ℕ) + 0) then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
  if i = Fin.natAdd 0 j then f.coeff 0 else 0
Tactic: rw [sylvester, Matrix.of_apply, Fin.addCases_right, Matrix.diagonal_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
f g : R[X]
m : ℕ
i j_1 : Fin (0 + m)
j : Fin m
⊢ (if (↑i : ℕ) ∈ Icc (↑j : ℕ) ((↑j : ℕ) + 0) then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if i = Fin.natAdd 0 j then f.coeff 0 else 0
have pos : (↑i : ℕ) ∈ Icc (↑j : ℕ) ((↑j : ℕ) + 0) → i = Fin.natAdd 0 j → f.coeff ((↑i : ℕ) - (↑j : ℕ)) = f.coeff 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Resultant.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
f g : R[X]
m : ℕ
i j_1 : Fin (0 + m)
j : Fin m
pos : (↑i : ℕ) ∈ Icc (↑j : ℕ) ((↑j : ℕ) + 0) → i = Fin.natAdd 0 j → f.coeff ((↑i : ℕ) - (↑j : ℕ)) = f.coeff 0
⊢ (if (↑i : ℕ) ∈ Icc (↑j : ℕ) ((↑j : ℕ) + 0) then f.coeff ((↑i : ℕ) - (↑j : ℕ)) else 0) =
    if i = Fin.natAdd 0 j then f.coeff 0 else 0
have neg : (↑i : ℕ) ∈ Icc (↑j : ℕ) ((↑j : ℕ) + 0) → ¬i = Fin.natAdd 0 j → f.coeff ((↑i : ℕ) - (↑j : ℕ)) = 0
Tactic: split_ifs