awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m : Multiset R
hm :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
⊢ f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
            (Multiset.map (fun (x : R) ↦ -x) m)) :
        R[X])

Tactic:
simpa
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m : Multiset R
hm :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
⊢ ∃ (m : Multiset R),
    f =
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
          R[X])

Tactic:
exact ⟨m.map (- ·), by simpa⟩
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
obtain :
  ∀ (m : Multiset R)
    (hm :
      f =
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
          (Multiset.prod
              (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
            R[X])),
    ∃ (a : R), eval a f = 0
⊢ ∃ (a : R), eval a f = 0

Tactic:
obtain ⟨m, hm⟩ := splits_iff_exists_multiset.mp hf

Premises used: Polynomial.splits_iff_exists_multiset, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
m : Multiset R
hm :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
pos : ∀ (hf₀ : f.leadingCoeff = 0), ∃ (a : R), eval a f = 0
neg : ∀ (hf₀ : ¬f.leadingCoeff = 0), ∃ (a : R), eval a f = 0
⊢ ∃ (a : R), eval a f = 0

Tactic:
by_cases hf₀ : f.leadingCoeff = 0

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
m : Multiset R
hm :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
hf₀ : f.leadingCoeff = 0
⊢ ∃ (a : R), eval a f = 0

Tactic:
simp [leadingCoeff_eq_zero.mp hf₀]

Premises used: Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
m : Multiset R
hm :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
hf₀ : ¬f.leadingCoeff = 0
neg :
  ∀
    (hm :
      f =
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
          (Multiset.prod
              (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) 0) :
            R[X])),
    ∃ (a : R), eval a f = 0
neg₁ : ∀ (a : R) (ha : a ∈ m), ∃ (a : R), eval a f = 0
⊢ ∃ (a : R), eval a f = 0

Tactic:
obtain rfl | ⟨a, ha⟩ := m.empty_or_exists_mem

Premises used: Multiset.empty_or_exists_mem, rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
hf₀ : ¬f.leadingCoeff = 0
hm :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) 0) :
        R[X])
⊢ Ne (α := WithBot ℕ) 0 0

Tactic:
rw [hm, Multiset.map_zero, Multiset.prod_zero, mul_one, degree_C hf₀] at hf0

Premises used: Multiset.prod_zero, Multiset.map_zero, Polynomial.degree_C, mul_one
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
hf₀ : ¬f.leadingCoeff = 0
hm :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) 0) :
        R[X])
hf0₁ : Ne (α := WithBot ℕ) 0 0
⊢ ¬f.leadingCoeff = 0

Tactic:
rw [hm, Multiset.map_zero, Multiset.prod_zero, mul_one, degree_C hf₀] at hf0

Premises used: Multiset.prod_zero, Multiset.map_zero, Polynomial.degree_C, mul_one
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
hf₀ : ¬f.leadingCoeff = 0
hm :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) 0) :
        R[X])
hf0₁ : Ne (α := WithBot ℕ) 0 0
hf₁ : ¬f.leadingCoeff = 0
⊢ f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) 0) :
        R[X])

Tactic:
rw [hm, Multiset.map_zero, Multiset.prod_zero, mul_one, degree_C hf₀] at hf0

Premises used: Multiset.prod_zero, Multiset.map_zero, Polynomial.degree_C, mul_one
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : Ne (α := WithBot ℕ) 0 0
hf₀ : ¬f.leadingCoeff = 0
hm :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) 0) :
        R[X])
⊢ ∃ (a : R), eval a f = 0

Tactic:
contradiction
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
m : Multiset R
hm :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
hf₀ : ¬f.leadingCoeff = 0
a : R
ha : a ∈ m
neg :
  ∀ (m : Multiset R)
    (hm :
      f =
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
          (Multiset.prod
              (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
                (a ::ₘ m)) :
            R[X]))
    (ha : a ∈ a ::ₘ m), ∃ (a : R), eval a f = 0
⊢ ∃ (a : R), eval a f = 0

Tactic:
obtain ⟨m, rfl⟩ := Multiset.exists_cons_of_mem ha

Premises used: Multiset.exists_cons_of_mem, rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
hf₀ : ¬f.leadingCoeff = 0
a : R
m : Multiset R
hm :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (a ::ₘ m)) :
        R[X])
ha : a ∈ a ::ₘ m
rw :
  eval a
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
              (a ::ₘ m)) :
          R[X])) =
    0
⊢ eval a f = 0

Tactic:
rw [hm]
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
hf₀ : ¬f.leadingCoeff = 0
a : R
m : Multiset R
hm :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (a ::ₘ m)) :
        R[X])
ha : a ∈ a ::ₘ m
⊢ eval a
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
              (a ::ₘ m)) :
          R[X])) =
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
hf₀ : ¬f.leadingCoeff = 0
a : R
m : Multiset R
hm :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (a ::ₘ m)) :
        R[X])
ha : a ∈ a ::ₘ m
⊢ ∃ (a : R), eval a f = 0

Tactic:
exact ⟨a, by rw [hm]; simp⟩
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hfd : f.degree ≠ 0
⊢ eval (rootOfSplits hf hfd) f = 0

Tactic:
Classical.choose_spec <| hf.exists_eval_eq_zero hfd

Premises used: Classical.choose_spec, Polynomial.Splits.exists_eval_eq_zero, Polynomial.rootOfSplits
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
a : R
⊢ (f.comp (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))).Splits

Tactic:
hf.comp_of_natDegree_le_one_of_monic (natDegree_sub_C.trans_le natDegree_X_le) (monic_X_sub_C a)

Premises used: Polynomial.monic_X_sub_C, Eq.trans_le, Polynomial.natDegree_X_le, Polynomial.natDegree_sub_C, Polynomial.Splits.comp_of_natDegree_le_one_of_monic
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
pos :
  ∀ (hf0 : f.leadingCoeff = 0),
    f =
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) :
          R[X])
neg :
  ∀ (hf0 : ¬f.leadingCoeff = 0),
    f =
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) :
          R[X])
⊢ f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) :
        R[X])

Tactic:
by_cases hf0 : f.leadingCoeff = 0

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hf0 : f.leadingCoeff = 0
⊢ f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) :
        R[X])

Tactic:
simp [leadingCoeff_eq_zero.mp hf0]

Premises used: Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 0
neg :
  ∀ (m : Multiset R)
    (hm :
      f =
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
          (Multiset.prod
              (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
            R[X])),
    f =
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) :
          R[X])
⊢ f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) :
        R[X])

Tactic:
obtain ⟨m, hm⟩ := splits_iff_exists_multiset.mp hf

Premises used: Polynomial.splits_iff_exists_multiset, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf_1 : f.Splits
hf0 : ¬f.leadingCoeff = 0
m : Multiset R
hm :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
hf : f.roots = m
rwa rwa₁ rwa₂ rwa₃ :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
⊢ f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) :
        R[X])

Tactic:
rwa [hf]
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 0
m : Multiset R
hm :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
neg : f.roots = m
⊢ f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) :
        R[X])

Tactic:
suffices hf : f.roots = m by rwa [hf]
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 0
m : Multiset R
hm :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
neg :
  (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
          R[X])).roots =
    m
neg₁ :
  roots
      (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m)) =
    m
neg₂ neg₃ : m = m
⊢ f.roots = m

Tactic:
rw [hm, roots_C_mul _ hf0, roots_multiset_prod_X_sub_C]

Premises used: Polynomial.roots_C_mul, Polynomial.roots_multiset_prod_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hm : f.Monic
rw :
  Multiset.prod
    (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots)
| f

Tactic:
rw [hf.eq_prod_roots, hm.leadingCoeff, C_1, one_mul]

Premises used: Polynomial.C_1, Polynomial.Splits.eq_prod_roots, Polynomial.Monic.leadingCoeff, one_mul
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hm : f.Monic
conv_lhs :
  f =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots)
conv_lhs₁ :
  Eq (α := R[X])
    (Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots))
    (Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots))
⊢ f =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots)

Tactic:
conv_lhs => rw [hf.eq_prod_roots, hm.leadingCoeff, C_1, one_mul]

Premises used: Polynomial.C_1, Polynomial.Splits.eq_prod_roots, Polynomial.Monic.leadingCoeff, one_mul
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
x : R
rw :
  eval x
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) :
        R[X]))
| eval x f

Tactic:
rw [hf.eq_prod_roots]

Premises used: Polynomial.Splits.eq_prod_roots
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
x : R
conv_lhs :
  eval x
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) :
          R[X])) =
    f.leadingCoeff * Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) f.roots)
⊢ eval x f = f.leadingCoeff * Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) f.roots)

Tactic:
conv_lhs => rw [hf.eq_prod_roots]

Premises used: Polynomial.Splits.eq_prod_roots
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
x : R
⊢ eval x
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) :
          R[X])) =
    f.leadingCoeff * Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) f.roots)

Tactic:
simp [eval_multiset_prod]

Premises used: Polynomial.eval_multiset_prod
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
hm : f.Monic
x : R
⊢ eval x f = Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) f.roots)

Tactic:
simp [hf.eval_eq_prod_roots, hm]

Premises used: Polynomial.Splits.eval_eq_prod_roots
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
A : Type u_2
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : Algebra R A
hf : Splits (map (algebraMap R A) f)
hm : f.Monic
x : A
⊢ Eq (α := A) ((aeval x : (a : R[X]) → A) f : A)
    (Multiset.prod (Multiset.map (fun (x_1 : A) ↦ x - x_1) (f.aroots A)) : A)

Tactic:
simp [hf.eval_eq_prod_roots_of_monic (hm.map (algebraMap R A)), ← eval_map_algebraMap]

Premises used: Algebra.algebraMap, Polynomial.Splits.eval_eq_prod_roots_of_monic, Polynomial.eval_map_algebraMap, Polynomial.Monic.map
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
inst_2 : DecidableEq R
hf : f.Splits
x : R
rw :
  eval x
    ((derivative : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) :
          R[X])))
| eval x ((derivative : (a : R[X]) → R[X]) f)

Tactic:
rw [hf.eq_prod_roots]

Premises used: Polynomial.Splits.eq_prod_roots
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
inst_2 : DecidableEq R
hf : f.Splits
x : R
conv_lhs :
  eval x
      ((derivative : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
          (Multiset.prod
              (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
                f.roots) :
            R[X]))) =
    f.leadingCoeff *
      Multiset.sum
        (Multiset.map (fun (a : R) ↦ Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) (f.roots.erase a))) f.roots)
⊢ eval x ((derivative : (a : R[X]) → R[X]) f) =
    f.leadingCoeff *
      Multiset.sum
        (Multiset.map (fun (a : R) ↦ Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) (f.roots.erase a))) f.roots)

Tactic:
conv_lhs => rw [hf.eq_prod_roots]

Premises used: Polynomial.Splits.eq_prod_roots
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
inst_2 : DecidableEq R
hf : f.Splits
x : R
⊢ eval x
      ((derivative : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
          (Multiset.prod
              (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
                f.roots) :
            R[X]))) =
    f.leadingCoeff *
      Multiset.sum
        (Multiset.map (fun (a : R) ↦ Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) (f.roots.erase a))) f.roots)

Tactic:
simp [derivative_prod, eval_multisetSum, eval_multiset_prod]

Premises used: Polynomial.eval_multiset_prod, Polynomial.derivative_prod, Polynomial.eval_multisetSum
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
inst_2 : DecidableEq R
hf : f.Splits
hm : f.Monic
x : R
hx : x ∈ f.roots
rw :
  eval x ((derivative : (a : R[X]) → R[X]) f) =
    eval x
      ((derivative : (a : R[X]) → R[X])
        (Multiset.prod
          (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) f.roots)))
rw₁ rw₂ : eval x ((derivative : (a : R[X]) → R[X]) f) = eval x ((derivative : (a : R[X]) → R[X]) f)
⊢ eval x ((derivative : (a : R[X]) → R[X]) f) = Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) (f.roots.erase x))

Tactic:
rw [← eval_multiset_prod_X_sub_C_derivative hx, ← hf.eq_prod_roots_of_monic hm]

Premises used: Polynomial.Splits.eq_prod_roots_of_monic, Polynomial.eval_multiset_prod_X_sub_C_derivative
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
S : Type u_4
inst_1 : CommRing S
inst_2 : IsDomain S
i : R →+* S
hi_1 : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑i : (a : R) → S)
hf : (map i f).Splits
hi : ∀ a ∈ (map i f).roots, Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_4} (R := R) i) a
choose :
  ∀ (j : (a : S) → a ∈ (map i f).roots → R)
    (hj : ∀ (a : S) (a_1 : a ∈ (map i f).roots), (i : (a : R) → S) (j a a_1) = a), f.Splits
⊢ f.Splits

Tactic:
choose j hj using hi
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
S : Type u_4
inst_1 : CommRing S
inst_2 : IsDomain S
i : R →+* S
hi : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑i : (a : R) → S)
hf : (map i f).Splits
j : (a : S) → a ∈ (map i f).roots → R
hj : ∀ (a : S) (a_1 : a ∈ (map i f).roots), (i : (a : R) → S) (j a a_1) = a
rw :
  ∃ (m : Multiset R),
    f =
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
          R[X])
⊢ f.Splits

Tactic:
rw [splits_iff_exists_multiset]

Premises used: Polynomial.splits_iff_exists_multiset