awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
a b : R
hg :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree =
    1
hf :
  (f.comp
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X]))).Splits
ha : a ≠ 0
rw :
  f =
    f.comp
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) *
          HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
        ((C : (a : R) → R[X]) b : R[X]))
rw₁ :
  f =
    f.comp
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a⁻¹) : R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))
        ((C : (a : R) → R[X]) b : R[X]))
rw₂ :
  f =
    f.comp
      (HAdd.hAdd (β := R[X])
        ((C : (a : R) → R[X]) 1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
        ((C : (a : R) → R[X]) b : R[X]))
⊢ f =
    f.comp
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))))
        ((C : (a : R) → R[X]) b : R[X]))
have rw₃ : f =
  f.comp
    (HAdd.hAdd (β := R[X]) (1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
      ((C : (a : R) → R[X]) b : R[X]))
Tactic: rw [← mul_assoc, ← C_mul, mul_inv_cancel₀ ha, C_1, one_mul, sub_add_cancel, comp_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
a b : R
hg :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree =
    1
hf :
  (f.comp
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X]))).Splits
ha : a ≠ 0
rw :
  f =
    f.comp
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) *
          HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
        ((C : (a : R) → R[X]) b : R[X]))
rw₁ :
  f =
    f.comp
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a⁻¹) : R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))
        ((C : (a : R) → R[X]) b : R[X]))
rw₂ :
  f =
    f.comp
      (HAdd.hAdd (β := R[X])
        ((C : (a : R) → R[X]) 1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
        ((C : (a : R) → R[X]) b : R[X]))
rw₃ :
  f =
    f.comp
      (HAdd.hAdd (β := R[X]) (1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
        ((C : (a : R) → R[X]) b : R[X]))
⊢ f =
    f.comp
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))))
        ((C : (a : R) → R[X]) b : R[X]))
have rw₄ : f =
  f.comp
    (HAdd.hAdd (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
      ((C : (a : R) → R[X]) b : R[X]))
Tactic: rw [← mul_assoc, ← C_mul, mul_inv_cancel₀ ha, C_1, one_mul, sub_add_cancel, comp_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
a b : R
hg :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree =
    1
hf :
  (f.comp
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X]))).Splits
ha : a ≠ 0
rw :
  f =
    f.comp
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) *
          HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
        ((C : (a : R) → R[X]) b : R[X]))
rw₁ :
  f =
    f.comp
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a⁻¹) : R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))
        ((C : (a : R) → R[X]) b : R[X]))
rw₂ :
  f =
    f.comp
      (HAdd.hAdd (β := R[X])
        ((C : (a : R) → R[X]) 1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
        ((C : (a : R) → R[X]) b : R[X]))
rw₃ :
  f =
    f.comp
      (HAdd.hAdd (β := R[X]) (1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
        ((C : (a : R) → R[X]) b : R[X]))
rw₄ :
  f =
    f.comp
      (HAdd.hAdd (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
        ((C : (a : R) → R[X]) b : R[X]))
⊢ f =
    f.comp
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))))
        ((C : (a : R) → R[X]) b : R[X]))
have rw₅ : f = f.comp X
Tactic: rw [← mul_assoc, ← C_mul, mul_inv_cancel₀ ha, C_1, one_mul, sub_add_cancel, comp_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
a b : R
hg :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree =
    1
hf :
  (f.comp
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X]))).Splits
ha : a ≠ 0
rw :
  f =
    f.comp
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X]) *
          HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
        ((C : (a : R) → R[X]) b : R[X]))
rw₁ :
  f =
    f.comp
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a * a⁻¹) : R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))
        ((C : (a : R) → R[X]) b : R[X]))
rw₂ :
  f =
    f.comp
      (HAdd.hAdd (β := R[X])
        ((C : (a : R) → R[X]) 1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
        ((C : (a : R) → R[X]) b : R[X]))
rw₃ :
  f =
    f.comp
      (HAdd.hAdd (β := R[X]) (1 * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
        ((C : (a : R) → R[X]) b : R[X]))
rw₄ :
  f =
    f.comp
      (HAdd.hAdd (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))
        ((C : (a : R) → R[X]) b : R[X]))
rw₅ : f = f.comp X
⊢ f =
    f.comp
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))))
        ((C : (a : R) → R[X]) b : R[X]))
have rw₆ : f = f
Tactic: rw [← mul_assoc, ← C_mul, mul_inv_cancel₀ ha, C_1, one_mul, sub_add_cancel, comp_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
Goal:
R : Type u_1
inst : Field R
f : R[X]
a b : R
hg :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree =
    1
hf :
  (f.comp
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X]))).Splits
ha : a ≠ 0
⊢ f.Splits
have this : f =
  (f.comp
        (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X]))).comp
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))
Tactic: have : f = (f.comp (C a * X + C b)).comp ((C a⁻¹ * (X - C b))) := by
    simp only [comp_assoc, add_comp, mul_comp, C_comp, X_comp]
    rw [← mul_assoc, ← C_mul, mul_inv_cancel₀ ha, C_1, one_mul, sub_add_cancel, comp_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
a b : R
hg :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree =
    1
hf :
  (f.comp
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X]))).Splits
ha : a ≠ 0
this :
  f =
    (f.comp
          (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
            ((C : (a : R) → R[X]) b : R[X]))).comp
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))
⊢ f.Splits
have rw : ((f.comp
        (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X]))).comp
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))).Splits
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
a b : R
hg :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree =
    1
hf :
  (f.comp
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X]))).Splits
ha : a ≠ 0
this :
  f =
    (f.comp
          (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
            ((C : (a : R) → R[X]) b : R[X]))).comp
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))
⊢ ((f.comp
          (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
            ((C : (a : R) → R[X]) b : R[X]))).comp
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))).Splits
have refine : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))).natDegree ≤
  1
Tactic: refine Splits.comp_of_natDegree_le_one hf ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
a b : R
hg :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree =
    1
hf :
  (f.comp
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X]))).Splits
ha : a ≠ 0
this :
  f =
    (f.comp
          (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
            ((C : (a : R) → R[X]) b : R[X]))).comp
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))).natDegree ≤
    1
have rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])).natDegree ≤ 1
Tactic: rw [natDegree_C_mul (mt inv_eq_zero.mp ha), natDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
a b : R
hg :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree =
    1
hf :
  (f.comp
      (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X]))).Splits
ha : a ≠ 0
this :
  f =
    (f.comp
          (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
            ((C : (a : R) → R[X]) b : R[X]))).comp
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))
rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])).natDegree ≤ 1
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a⁻¹ : R[X])
        (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))).natDegree ≤
    1
have rw₁ : LE.le (α := ℕ) 1 1
Tactic: rw [natDegree_C_mul (mt inv_eq_zero.mp ha), natDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
⊢ eval x ((derivative : (a : R[X]) → R[X]) f) =
    eval x f * Multiset.sum (Multiset.map (fun (z : R) ↦ 1 / (x - z)) f.roots)
have simp : Eq (α := R)
  (Multiset.sum
    (Multiset.map
      (fun (i : R) ↦ f.leadingCoeff * Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) (f.roots.erase i)))
      f.roots))
  (Multiset.sum
    (Multiset.map
      (fun (x_1 : R) ↦
        f.leadingCoeff * (Multiset.prod (Multiset.map (fun (x_2 : R) ↦ x - x_2) f.roots) * (1 / (x - x_1))))
      f.roots))
Tactic: simp only [hf.eval_derivative, hf.eval_eq_prod_roots, ← Multiset.sum_map_mul_left, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
⊢ Eq (α := R)
    (Multiset.sum
      (Multiset.map
        (fun (i : R) ↦ f.leadingCoeff * Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) (f.roots.erase i)))
        f.roots))
    (Multiset.sum
      (Multiset.map
        (fun (x_1 : R) ↦
          f.leadingCoeff * (Multiset.prod (Multiset.map (fun (x_2 : R) ↦ x - x_2) f.roots) * (1 / (x - x_1))))
        f.roots))
have refine : ∀ (z : R) (hz : z ∈ f.roots),
  f.leadingCoeff * Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) (f.roots.erase z)) =
    f.leadingCoeff * (Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) f.roots) * (1 / (x - z)))
Tactic: refine congr_arg Multiset.sum (Multiset.map_congr rfl fun z hz ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
z : R
hz : z ∈ f.roots
⊢ f.leadingCoeff * Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) (f.roots.erase z)) =
    f.leadingCoeff * (Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) f.roots) * (1 / (x - z)))
have ha : x - z ≠ 0
Tactic: rw [← Multiset.prod_map_erase hz, mul_one_div, mul_div_cancel_left₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
⊢ eval x ((derivative : (a : R[X]) → R[X]) f) =
    eval x f * Multiset.sum (Multiset.map (fun (z : R) ↦ 1 / (x - z)) f.roots)
have simp : Eq (α := R)
  (Multiset.sum
    (Multiset.map
      (fun (i : R) ↦ f.leadingCoeff * Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) (f.roots.erase i)))
      f.roots))
  (Multiset.sum
    (Multiset.map
      (fun (x_1 : R) ↦
        f.leadingCoeff * (Multiset.prod (Multiset.map (fun (x_2 : R) ↦ x - x_2) f.roots) * (1 / (x - x_1))))
      f.roots))
Tactic: classical
  simp only [hf.eval_derivative, hf.eval_eq_prod_roots, ← Multiset.sum_map_mul_left, mul_assoc]
  refine congr_arg Multiset.sum (Multiset.map_congr rfl fun z hz ↦ ?_)
  rw [← Multiset.prod_map_erase hz, mul_one_div, mul_div_cancel_left₀]
  aesop (add simp sub_eq_zero)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
simp :
  Eq (α := R)
    (Multiset.sum
      (Multiset.map
        (fun (i : R) ↦ f.leadingCoeff * Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) (f.roots.erase i)))
        f.roots))
    (Multiset.sum
      (Multiset.map
        (fun (x_1 : R) ↦
          f.leadingCoeff * (Multiset.prod (Multiset.map (fun (x_2 : R) ↦ x - x_2) f.roots) * (1 / (x - x_1))))
        f.roots))
⊢ eval x ((derivative : (a : R[X]) → R[X]) f) =
    eval x f * Multiset.sum (Multiset.map (fun (z : R) ↦ 1 / (x - z)) f.roots)
have simp₁ : ∀ (z : R) (hz : z ∈ f.roots),
  f.leadingCoeff * Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) (f.roots.erase z)) =
    f.leadingCoeff * (Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) f.roots) * (1 / (x - z)))
Tactic: classical
  simp only [hf.eval_derivative, hf.eval_eq_prod_roots, ← Multiset.sum_map_mul_left, mul_assoc]
  refine congr_arg Multiset.sum (Multiset.map_congr rfl fun z hz ↦ ?_)
  rw [← Multiset.prod_map_erase hz, mul_one_div, mul_div_cancel_left₀]
  aesop (add simp sub_eq_zero)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
simp :
  Eq (α := R)
    (Multiset.sum
      (Multiset.map
        (fun (i : R) ↦ f.leadingCoeff * Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) (f.roots.erase i)))
        f.roots))
    (Multiset.sum
      (Multiset.map
        (fun (x_1 : R) ↦
          f.leadingCoeff * (Multiset.prod (Multiset.map (fun (x_2 : R) ↦ x - x_2) f.roots) * (1 / (x - x_1))))
        f.roots))
simp₁ :
  ∀ (z : R) (hz : z ∈ f.roots),
    f.leadingCoeff * Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) (f.roots.erase z)) =
      f.leadingCoeff * (Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) f.roots) * (1 / (x - z)))
⊢ eval x ((derivative : (a : R[X]) → R[X]) f) =
    eval x f * Multiset.sum (Multiset.map (fun (z : R) ↦ 1 / (x - z)) f.roots)
have ha : ∀ (z : R) (hz : z ∈ f.roots), x - z ≠ 0
Tactic: classical
  simp only [hf.eval_derivative, hf.eval_eq_prod_roots, ← Multiset.sum_map_mul_left, mul_assoc]
  refine congr_arg Multiset.sum (Multiset.map_congr rfl fun z hz ↦ ?_)
  rw [← Multiset.prod_map_erase hz, mul_one_div, mul_div_cancel_left₀]
  aesop (add simp sub_eq_zero)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
⊢ eval x ((derivative : (a : R[X]) → R[X]) f) / eval x f =
    Multiset.sum (Multiset.map (fun (z : R) ↦ 1 / (x - z)) f.roots)
have rw : eval x f * Multiset.sum (Multiset.map (fun (z : R) ↦ 1 / (x - z)) f.roots) / eval x f =
  Multiset.sum (Multiset.map (fun (z : R) ↦ 1 / (x - z)) f.roots)
Tactic: rw [hf.eval_derivative_eq_eval_mul_sum hx, mul_div_cancel_left₀ _ hx]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
rw :
  eval x f * Multiset.sum (Multiset.map (fun (z : R) ↦ 1 / (x - z)) f.roots) / eval x f =
    Multiset.sum (Multiset.map (fun (z : R) ↦ 1 / (x - z)) f.roots)
⊢ eval x ((derivative : (a : R[X]) → R[X]) f) / eval x f =
    Multiset.sum (Multiset.map (fun (z : R) ↦ 1 / (x - z)) f.roots)
have rw₁ : Eq (α := R) (Multiset.sum (Multiset.map (fun (z : R) ↦ 1 / (x - z)) f.roots))
  (Multiset.sum (Multiset.map (fun (z : R) ↦ 1 / (x - z)) f.roots))
Tactic: rw [hf.eval_derivative_eq_eval_mul_sum hx, mul_div_cancel_left₀ _ hx]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
⊢ (f /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree = 1
have rw : f.natDegree - (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree = 1
Tactic: rw [natDegree_divByMonic f (monic_X_sub_C x), h₁, natDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
rw : f.natDegree - (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree = 1
⊢ (f /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree = 1
have rw₁ : 2 - (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree = 1
Tactic: rw [natDegree_divByMonic f (monic_X_sub_C x), h₁, natDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
rw : f.natDegree - (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree = 1
rw₁ : 2 - (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree = 1
⊢ (f /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree = 1
have rw₂ : HSub.hSub (α := ℕ) 2 1 = 1
Tactic: rw [natDegree_divByMonic f (monic_X_sub_C x), h₁, natDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
Goal:
R : Type u_1
inst : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
⊢ f.Splits
have h : (f /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree = 1
Tactic: have h : (f /ₘ (X - C x)).natDegree = 1 := by
    rw [natDegree_divByMonic f (monic_X_sub_C x), h₁, natDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
h : (f /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree = 1
⊢ f.Splits
have rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).Splits ∧
  (f /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).Splits
Tactic: rw [← mul_divByMonic_eq_iff_isRoot.mpr h₂, splits_mul_iff (X_sub_C_ne_zero x) (by aesop)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
⊢ f.Splits ↔ f = 0 ∨ ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
have refine : (f = 0 ∨ ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1) → f.Splits
Tactic: refine ⟨fun hf ↦ or_iff_not_imp_left.mpr fun h0 g hg hgf ↦
    (hf.of_dvd h0 hgf).degree_eq_one_of_irreducible hg, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
⊢ f.Splits
have pos : ∀ (hf0 : f = 0), f.Splits
Tactic: by_cases hf0 : f = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
pos : ∀ (hf0 : f = 0), f.Splits
⊢ f.Splits
have neg : ∀ (hf0 : ¬f = 0), f.Splits
Tactic: by_cases hf0 : f = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
hf0 : ¬f = 0
⊢ f.Splits
have neg : ∀ (u : R[X]ˣ) (hu : (factors f).prod * (↑u : R[X]) = f), f.Splits
Tactic: obtain ⟨u, hu⟩ := factors_prod hf0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
hf0 : ¬f = 0
u : R[X]ˣ
hu : (factors f).prod * (↑u : R[X]) = f
⊢ f.Splits
have neg : ((factors f).prod * (↑u : R[X])).Splits
Tactic: rw [← hu]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1
hf0 : ¬f = 0
u : R[X]ˣ
hu : (factors f).prod * (↑u : R[X]) = f
⊢ ((factors f).prod * (↑u : R[X])).Splits
have neg : ∀ (g : R[X]) (hg : g ∈ factors f), g.Splits
Tactic: refine (Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits