awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Splits
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])))
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
⊢ ((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:
refine Splits.comp_of_natDegree_le_one hf ?_

Premises used: Polynomial.Splits.comp_of_natDegree_le_one
-- Module: Mathlib.Algebra.Polynomial.Splits
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
rw₁ rw₂ : LE.le (α := ℕ) 1 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

Tactic:
rw [natDegree_C_mul (mt inv_eq_zero.mp ha), natDegree_X_sub_C]

Premises used: mt, Polynomial.natDegree_X_sub_C, Polynomial.natDegree_C_mul
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f g : R[X]
hg : g.degree = 1
⊢ f.Splits ↔ (f.comp g).Splits

Tactic:
splits_iff_comp_splits_of_natDegree_eq_one (natDegree_eq_of_degree_eq_some hg)

Premises used: Polynomial.splits_iff_comp_splits_of_natDegree_eq_one, Polynomial.natDegree_eq_of_degree_eq_some
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : f.Splits
h : Irreducible f
⊢ f.degree = 1

Tactic:
le_antisymm (hf.degree_le_one_of_irreducible h)
    ((WithBot.one_le_iff_pos _).mpr (degree_pos_of_irreducible h))

Premises used: Iff.mpr, Polynomial.Splits.degree_le_one_of_irreducible, le_antisymm, Polynomial.degree_pos_of_irreducible, WithBot.one_le_iff_pos
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : f.Splits
h : Irreducible f
⊢ f.natDegree = 1

Tactic:
natDegree_eq_of_degree_eq_some (hf.degree_eq_one_of_irreducible h)

Premises used: Polynomial.Splits.degree_eq_one_of_irreducible, Polynomial.natDegree_eq_of_degree_eq_some
-- Module: Mathlib.Algebra.Polynomial.Splits
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)

Tactic:
simp only [hf.eval_derivative, hf.eval_eq_prod_roots, ← Multiset.sum_map_mul_left, mul_assoc]

Premises used: Polynomial.Splits.eval_derivative, mul_assoc, Polynomial.Splits.eval_eq_prod_roots, Multiset.sum_map_mul_left
-- Module: Mathlib.Algebra.Polynomial.Splits
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))

Tactic:
congr_arg Multiset.sum (Multiset.map_congr rfl fun z hz ↦ ?_)

Premises used: Multiset.sum, congr_arg, Multiset.map_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f : R[X]
hf : f.Splits
x : R
hx : eval x f ≠ 0
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)))
⊢ 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:
refine congr_arg Multiset.sum (Multiset.map_congr rfl fun z hz ↦ ?_)

Premises used: Multiset.sum, congr_arg, Multiset.map_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
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
ha : x - z ≠ 0
⊢ 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:
rw [← Multiset.prod_map_erase hz, mul_one_div, mul_div_cancel_left₀]

Premises used: Multiset.prod_map_erase, mul_div_cancel_left₀, mul_one_div
-- Module: Mathlib.Algebra.Polynomial.Splits
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
⊢ x - z ≠ 0

Tactic:
aesop (add simp sub_eq_zero)

Premises used: sub_eq_zero
-- Module: Mathlib.Algebra.Polynomial.Splits
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)))
ha : ∀ (z : R) (hz : z ∈ f.roots), x - z ≠ 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)

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)

Premises used: Multiset.sum, sub_eq_zero, mul_assoc, mul_div_cancel_left₀, congr_arg, Polynomial.Splits.eval_eq_prod_roots, mul_one_div, Multiset.map_congr, rfl, Multiset.sum_map_mul_left
-- Module: Mathlib.Algebra.Polynomial.Splits
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)
rw₁ 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))
⊢ eval x ((derivative : (a : R[X]) → R[X]) f) / 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]

Premises used: Polynomial.Splits.eval_derivative_eq_eval_mul_sum, mul_div_cancel_left₀
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
F : Subfield R
f : (↥F)[X]
hf : f.Splits
hf0 : f ≠ 0
x : R
hx : (map F.subtype f).IsRoot x
⊢ x ∈ F

Tactic:
simpa using hf.mem_range_of_isRoot hf0 hx

Premises used: Polynomial.Splits.mem_range_of_isRoot
-- Module: Mathlib.Algebra.Polynomial.Splits
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
rw₂ rw₃ : HSub.hSub (α := ℕ) 2 1 = 1
⊢ (f /ₘ 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]

Premises used: Polynomial.monic_X_sub_C, Polynomial.natDegree_divByMonic, Polynomial.natDegree_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.Splits
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

Tactic:
have h : (f /ₘ (X - C x)).natDegree = 1 := by
    rw [natDegree_divByMonic f (monic_X_sub_C x), h₁, natDegree_X_sub_C]
-- Module: Mathlib.Algebra.Polynomial.Splits
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 /ₘ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ≠ 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Splits
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
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
⊢ f.Splits

Tactic:
rw [← mul_divByMonic_eq_iff_isRoot.mpr h₂, splits_mul_iff (X_sub_C_ne_zero x) (by aesop)]

Premises used: Iff.mpr, Polynomial.mul_divByMonic_eq_iff_isRoot, Polynomial.splits_mul_iff, Polynomial.X_sub_C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Splits
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
⊢ (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:
⟨Splits.X_sub_C x, Splits.of_natDegree_eq_one h⟩

Premises used: Polynomial.Splits.of_natDegree_eq_one, Polynomial.Splits.X_sub_C, And.intro
-- Module: Mathlib.Algebra.Polynomial.Splits
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
⊢ (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:
exact ⟨Splits.X_sub_C x, Splits.of_natDegree_eq_one h⟩
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f : R[X]
x : R
h₁ : f.degree = 2
h₂ : eval x f = 0
⊢ f.Splits

Tactic:
Splits.of_natDegree_eq_two (natDegree_eq_of_degree_eq_some h₁) h₂

Premises used: Polynomial.natDegree_eq_of_degree_eq_some, Polynomial.Splits.of_natDegree_eq_two
-- Module: Mathlib.Algebra.Polynomial.Splits
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

Tactic:
⟨fun hf ↦ or_iff_not_imp_left.mpr fun h0 g hg hgf ↦
    (hf.of_dvd h0 hgf).degree_eq_one_of_irreducible hg, ?_⟩

Premises used: Iff.mpr, Polynomial.Splits.degree_eq_one_of_irreducible, Classical.or_iff_not_imp_left, Iff.intro, Polynomial.Splits.of_dvd
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
f : R[X]
refine : (f = 0 ∨ ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1) → f.Splits
⊢ f.Splits ↔ f = 0 ∨ ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree = 1

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, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Field R
⊢ Splits.{u_1} (R := R) 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Splits
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
neg : ∀ (hf0 : ¬f = 0), f.Splits
⊢ f.Splits

Tactic:
by_cases hf0 : f = 0
-- Module: Mathlib.Algebra.Polynomial.Splits
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

Tactic:
simp [hf0]
-- Module: Mathlib.Algebra.Polynomial.Splits
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
neg : ∀ (u : R[X]ˣ) (hu : (factors f).prod * (↑u : R[X]) = f), f.Splits
⊢ f.Splits

Tactic:
obtain ⟨u, hu⟩ := factors_prod hf0

Premises used: UniqueFactorizationMonoid.factors_prod
-- Module: Mathlib.Algebra.Polynomial.Splits
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
neg : ((factors f).prod * (↑u : R[X])).Splits
⊢ f.Splits

Tactic:
rw [← hu]
-- Module: Mathlib.Algebra.Polynomial.Splits
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

Tactic:
(Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits

Premises used: Polynomial.Splits.multisetProd, IsUnit.splits, Units.isUnit, Polynomial.Splits.mul
-- Module: Mathlib.Algebra.Polynomial.Splits
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
neg : ∀ (g : R[X]) (hg : g ∈ factors f), g.Splits
⊢ ((factors f).prod * (↑u : R[X])).Splits

Tactic:
refine (Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits

Premises used: Polynomial.Splits.multisetProd, IsUnit.splits, Units.isUnit, Polynomial.Splits.mul
-- Module: Mathlib.Algebra.Polynomial.Splits
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
g : R[X]
hg : g ∈ factors f
⊢ g.Splits

Tactic:
Splits.of_degree_eq_one (hf (irreducible_of_factor g hg) (dvd_of_mem_factors hg))

Premises used: UniqueFactorizationMonoid.irreducible_of_factor, Polynomial.Splits.of_degree_eq_one, UniqueFactorizationMonoid.dvd_of_mem_factors
-- Module: Mathlib.Algebra.Polynomial.Splits
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
g : R[X]
hg : g ∈ factors f
⊢ g.Splits

Tactic:
exact Splits.of_degree_eq_one (hf (irreducible_of_factor g hg) (dvd_of_mem_factors hg))

Premises used: UniqueFactorizationMonoid.irreducible_of_factor, Polynomial.Splits.of_degree_eq_one, UniqueFactorizationMonoid.dvd_of_mem_factors
-- Module: Mathlib.Algebra.Polynomial.Splits
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
neg neg₁ : ∀ (hf0 : ¬f = 0), f.Splits
neg₂ : ∀ (hf0 : ¬f = 0) (u : R[X]ˣ) (hu : (factors f).prod * (↑u : R[X]) = f), f.Splits
neg₃ : ∀ (hf0 : ¬f = 0) (u : R[X]ˣ) (hu : (factors f).prod * (↑u : R[X]) = f), ((factors f).prod * (↑u : R[X])).Splits
neg₄ : ∀ (hf0 : ¬f = 0) (u : R[X]ˣ) (hu : (factors f).prod * (↑u : R[X]) = f) (g : R[X]) (hg : g ∈ factors f), g.Splits
⊢ f.Splits

Tactic:
classical
  by_cases hf0 : f = 0
  · simp [hf0]
  obtain ⟨u, hu⟩ := factors_prod hf0
  rw [← hu]
  refine (Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits
  exact Splits.of_degree_eq_one (hf (irreducible_of_factor g hg) (dvd_of_mem_factors hg))
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
K : Type v
L : Type w
inst : CommRing K
inst_1 : Field L
i : K →+* L
f : K[X]
a : L
h : map i f = (C : (a : L) → L[X]) a
⊢ (map i f).Splits

Tactic:
h ▸ Splits.C a

Premises used: Eq.rec, Eq.symm, Polynomial.Splits.C
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
F : Type u
K : Type v
inst : CommRing K
inst_1 : Field F
L : Type u_2
inst_2 : CommRing L
i : K →+* L
j : L →+* F
f : K[X]
rw rw₁ : (map (j.comp i) f).Splits ↔ (map (j.comp i) f).Splits
⊢ (map j (map i f)).Splits ↔ (map (j.comp i) f).Splits

Tactic:
rw [Polynomial.map_map]

Premises used: Polynomial.map_map
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
K : Type v
L : Type w
inst : CommRing K
inst_1 : Field L
i : K →+* L
f : K[X]
rw rw₁ : (map i f).Splits ↔ (map i f).Splits
⊢ (map (RingHom.id L) (map i f)).Splits ↔ (map i f).Splits

Tactic:
rw [map_id]

Premises used: Polynomial.map_id
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
K : Type v
inst : Field K
inst_1 : DecidableEq K
f g : K[X]
hf0 : f ≠ 0
hf : f.Splits
⊢ (EuclideanDomain.gcd f g).Splits

Tactic:
Splits.of_dvd hf hf0 <| EuclideanDomain.gcd_dvd_left f g

Premises used: Polynomial.Splits.of_dvd, EuclideanDomain.gcd_dvd_left
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
K : Type v
inst : Field K
inst_1 : DecidableEq K
f g : K[X]
hg0 : g ≠ 0
hg : g.Splits
⊢ (EuclideanDomain.gcd f g).Splits

Tactic:
Splits.of_dvd hg hg0 <| EuclideanDomain.gcd_dvd_right f g

Premises used: EuclideanDomain.gcd_dvd_right, Polynomial.Splits.of_dvd
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
K : Type v
L : Type w
inst : Field K
inst_1 : Field L
i : K →+* L
f : K[X]
hf : (map i f).Splits
hfd : (map i f).degree ≠ 0
⊢ rootOfSplits hf hfd = rootOfSplits hf ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ Finsupp.support.{0, u_1} (M := R[X]) ((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) p) ⊆ range (p.natDegree + 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ ∀ i ∈ range (p.natDegree + 1), Eq.{u_1 + 1} (α := R[X]) (id 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ Eq.{u_1 + 1} (α := R[X]) (Finsupp.sum (M := R[X]) ((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) p) fun (i : ℕ) ↦ id)
    (∑ i ∈ range (p.natDegree + 1), (⇑derivative : (a : R[X]) → R[X])^[i] p)

Tactic:
exact Finsupp.sum_of_support_subset _ (by simp) _ (by simp)

Premises used: Finsupp.sum_of_support_subset
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
⊢ Finsupp.support.{0, u_1} (M := R[X]) ((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) p) ⊆ range n

Tactic:
simp [hn]
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
⊢ ∀ i ∈ range n, Eq.{u_1 + 1} (α := R[X]) (id 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
⊢ Eq.{u_1 + 1} (α := R[X]) (Finsupp.sum (M := R[X]) ((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) p) fun (i : ℕ) ↦ id)
    (∑ i ∈ range n, (⇑derivative : (a : R[X]) → R[X])^[i] p)

Tactic:
exact Finsupp.sum_of_support_subset _ (by simp [hn]) _ (by simp)

Premises used: Finsupp.sum_of_support_subset
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ Finsupp.support.{0, u_1} (M := R[X]) ((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) p) ⊆ range (n + 1)

Tactic:
simp [hn]
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ ∀ i ∈ range (n + 1), Eq.{u_1 + 1} (α := R[X]) (id 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ Eq.{u_1 + 1} (α := R[X]) (Finsupp.sum (M := R[X]) ((derivativeFinsupp : (a : R[X]) → ℕ →₀ R[X]) p) fun (i : ℕ) ↦ id)
    (∑ i ∈ range (n + 1), (⇑derivative : (a : R[X]) → R[X])^[i] p)

Tactic:
exact Finsupp.sum_of_support_subset _ (by simp [hn]) _ (by simp)

Premises used: Finsupp.sum_of_support_subset
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
R : Type u_1
inst : Semiring R
a : R
rw :
  Eq (α := R[X])
    (∑ i ∈ range (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) a) + 1),
        (⇑derivative : (a : R[X]) → R[X])^[i] ((C : (a : R) → R[X]) a) :
      R[X])
    ((C : (a : R) → R[X]) a : R[X])
rw₁ :
  Eq (α := R[X])
    (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), (⇑derivative : (a : R[X]) → R[X])^[i] ((C : (a : R) → R[X]) a) : R[X])
    ((C : (a : R) → R[X]) a : R[X])
rw₂ :
  Eq (α := R[X]) (∑ i ∈ range 1, (⇑derivative : (a : R[X]) → R[X])^[i] ((C : (a : R) → R[X]) a) : R[X])
    ((C : (a : R) → R[X]) a : R[X])
rw₃ :
  Eq (α := R[X]) ((⇑derivative : (a : R[X]) → R[X])^[0] ((C : (a : R) → R[X]) a) : R[X]) ((C : (a : R) → R[X]) a : R[X])
rw₄ rw₅ : Eq (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a : R[X])
⊢ Eq (α := R[X]) ((sumIDeriv : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) a) : R[X]) ((C : (a : R) → R[X]) a : R[X])

Tactic:
rw [sumIDeriv_apply, natDegree_C, zero_add, sum_range_one, Function.iterate_zero_apply]

Premises used: Polynomial.natDegree_C, Finset.sum_range_one, zero_add, Polynomial.sumIDeriv_apply, Function.iterate_zero_apply
-- Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative
Goal:
rw :
  ∑ i ∈ range (natDegree (R := ℕ) X + 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₁ :
  ∑ i ∈ range (HAdd.hAdd (α := ℕ) 1 1), (⇑derivative : (a : ℕ[X]) → ℕ[X])^[i] X =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₂ :
  HAdd.hAdd (α := ℕ[X]) (∑ x ∈ range 1, (⇑derivative : (a : ℕ[X]) → ℕ[X])^[x] X)
      ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₃ :
  HAdd.hAdd (α := ℕ[X]) ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[0] X) ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₄ :
  HAdd.hAdd (α := ℕ[X]) X ((⇑derivative : (a : ℕ[X]) → ℕ[X])^[1] X) = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₅ :
  HAdd.hAdd (α := ℕ[X]) (β := ℕ[X]) X ((derivative : (a : ℕ[X]) → ℕ[X]) X : ℕ[X]) =
    HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₆ : HAdd.hAdd (α := ℕ[X]) X 1 = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)
rw₇ : HAdd.hAdd (α := ℕ[X]) X 1 = HAdd.hAdd (α := ℕ[X]) X (↑1 : ℕ[X])
rw₈ rw₉ : HAdd.hAdd (α := ℕ[X]) X 1 = HAdd.hAdd (α := ℕ[X]) X 1
⊢ (sumIDeriv : (a : ℕ[X]) → ℕ[X]) X = HAdd.hAdd (α := ℕ[X]) X ((C : (a : ℕ) → ℕ[X]) 1)

Tactic:
rw [sumIDeriv_apply, natDegree_X, sum_range_succ, sum_range_one, Function.iterate_zero_apply,
    Function.iterate_one, derivative_X, eq_natCast, Nat.cast_one]

Premises used: Polynomial.natDegree_X, Polynomial.derivative_X, Finset.sum_range_one, Polynomial.sumIDeriv_apply, Function.iterate_one, Function.iterate_zero_apply, Nat.cast_one, Finset.sum_range_succ, eq_natCast