awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ih :
  ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n),
    f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
p : R[X]
h : p.Splits
hn : p.natDegree = n + 1
a : R
ha : eval a p = 0
f : R[X]
hf₀ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ≠ 0
hp : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g) = p
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ∨
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ g
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).Splits

Tactic:
subst hp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ih :
  ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n),
    f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
p : R[X]
h : p.Splits
hn : p.natDegree = n + 1
a : R
ha : eval a p = 0
f : R[X]
hf₀ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ≠ 0
hp : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g) = p
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ∨
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ g
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).Splits
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).natDegree = n + 1

Tactic:
subst hp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ih :
  ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n),
    f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
p : R[X]
h : p.Splits
hn : p.natDegree = n + 1
a : R
ha : eval a p = 0
f : R[X]
hf₀ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ≠ 0
hp : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g) = p
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ∨
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ g
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).Splits
hn₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).natDegree = n + 1
⊢ eval a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)) = 0

Tactic:
subst hp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ih :
  ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n),
    f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ≠ 0
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ∨
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ g
h : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).Splits
hn : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).natDegree = n + 1
ha : eval a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)) = 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ≠ 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ih :
  ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n),
    f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ≠ 0
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ∨
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ g
h : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).Splits
hn : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).natDegree = n + 1
ha : eval a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)) = 0
⊢ f * g ≠ 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ih :
  ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n),
    f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ≠ 0
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ∨
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ g
h : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).Splits
hn : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).natDegree = n + 1
ha : eval a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)) = 0
⊢ (f * g).natDegree = n

Tactic:
rw [natDegree_mul (by aesop) (by aesop), natDegree_X_sub_C, add_comm, Nat.succ_inj] at hn

Premises used: Nat.succ_inj, Polynomial.natDegree_mul, Polynomial.natDegree_X_sub_C, add_comm
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ih :
  ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n),
    f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ≠ 0
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ∨
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ g
h : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).Splits
hn : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).natDegree = n + 1
ha : eval a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)) = 0
hn₁ : (f * g).natDegree = n
⊢ eval a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)) = 0

Tactic:
rw [natDegree_mul (by aesop) (by aesop), natDegree_X_sub_C, add_comm, Nat.succ_inj] at hn

Premises used: Nat.succ_inj, Polynomial.natDegree_mul, Polynomial.natDegree_X_sub_C, add_comm
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ih :
  ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n),
    f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ≠ 0
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ∨
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ g
h : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).Splits
hn : (f * g).natDegree = n
ha : eval a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)) = 0
⊢ f ≠ 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ih :
  ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n),
    f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ≠ 0
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ∨
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ g
h : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).Splits
hn : (f * g).natDegree = n
ha : eval a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)) = 0
⊢ f.Splits ∧ g.Splits

Tactic:
have := ih (by aesop) hg₀ (f * g) rfl (splits_X_sub_C_mul_iff.mp h) hn
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ih :
  ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n),
    f.Splits ∧ g.Splits
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ≠ 0
this_1 :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f ∨
    HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ g
h : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)).Splits
hn : (f * g).natDegree = n
ha : eval a (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g)) = 0
this : f.Splits ∧ g.Splits
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits ∧ g.Splits

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
inst_1 : IsDomain R
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
n : ℕ
hn : p.natDegree = n
zero :
  ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = 0),
    f.Splits ∧ g.Splits
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n),
        f.Splits ∧ g.Splits)
    {f g : R[X]} (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) (p : R[X]) (hp : f * g = p) (h : p.Splits) (hn : p.natDegree = n + 1),
    f.Splits ∧ g.Splits
⊢ f.Splits ∧ g.Splits

Tactic:
induction n generalizing p f g with
  | zero =>
    rw [← hp, natDegree_mul hf₀ hg₀, Nat.add_eq_zero_iff] at hn
    exact ⟨splits_of_natDegree_eq_zero hn.1, splits_of_natDegree_eq_zero hn.2⟩
  | succ n ih =>
    obtain ⟨a, ha⟩ := Splits.exists_eval_eq_zero h (degree_ne_of_natDegree_ne <| hn ▸ by simp)
    have := dvd_iff_isRoot.mpr ha
    rw [← hp, (prime_X_sub_C a).dvd_mul] at this
    wlog hf : X - C a ∣ f with hf2
    · exact .symm <| hf2 n ih hg₀ hf₀ p ((mul_comm g f).trans hp) h hn a ha this.symm <|
        this.resolve_left hf
    obtain ⟨f, rfl⟩ := hf
    rw [mul_assoc] at hp; subst hp
    rw [natDegree_mul (by aesop) (by aesop), natDegree_X_sub_C, add_comm, Nat.succ_inj] at hn
    have := ih (by aesop) hg₀ (f * g) rfl (splits_X_sub_C_mul_iff.mp h) hn
    aesop

Premises used: Nat.succ_inj, Polynomial.natDegree_mul, mul_assoc, Polynomial.degree_ne_of_natDegree_ne, Eq.rec, Polynomial.natDegree_X_sub_C, add_comm, Polynomial.Splits.exists_eval_eq_zero, Eq.symm, Polynomial.X, Nat.add_eq_zero_iff, rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f g : R[X]
inst_1 : IsDomain R
hg : g.Splits
hg₀ : g ≠ 0
hfg : f ∣ g
obtain : ∀ (g : R[X]) (hg : (f * g).Splits) (hg₀ : f * g ≠ 0), f.Splits
⊢ f.Splits

Tactic:
obtain ⟨g, rfl⟩ := hfg

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
g : R[X]
hg : (f * g).Splits
hg₀ : f * g ≠ 0
⊢ f ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
g : R[X]
hg : (f * g).Splits
hg₀ : f * g ≠ 0
⊢ g ≠ 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
g : R[X]
hg : (f * g).Splits
hg₀ : f * g ≠ 0
⊢ f.Splits

Tactic:
exact ((splits_mul_iff (by simp_all) (by simp_all)).mp hg).1

Premises used: Polynomial.splits_mul_iff, And.left, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
ι : Type u_4
f : ι → R[X]
s : Finset ι
hf : ∀ i ∈ s, f i ≠ 0
⊢ Splits.{u_1} (R := R) (∏ x ∈ s, f x) ↔ ∀ x ∈ s, (f x).Splits

Tactic:
⟨fun h _ hx ↦ h.of_dvd (Finset.prod_ne_zero_iff.mpr hf) (Finset.dvd_prod_of_mem f hx),
    Splits.prod⟩

Premises used: Iff.mpr, Finset.dvd_prod_of_mem, Finset.prod_ne_zero_iff, Iff.intro, Polynomial.Splits.of_dvd, Polynomial.Splits.prod
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
⊢ f = 0 ∨ ∀ {g : R[X]}, Irreducible g → g ∣ f → g.degree ≤ 1

Tactic:
or_iff_not_imp_left.mpr fun hf0 _ hg hgf ↦ degree_le_of_natDegree_le <|
    (hf.of_dvd hf0 hgf).natDegree_le_one_of_irreducible hg

Premises used: Iff.mpr, Polynomial.Splits.natDegree_le_one_of_irreducible, Polynomial.degree_le_of_natDegree_le, Classical.or_iff_not_imp_left, Polynomial.Splits.of_dvd
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ g =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) g.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])) g.roots) :
        R[X])

Tactic:
have := hg'.eq_prod_roots
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this :
  g =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) g.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])) g.roots) :
        R[X])
⊢ g =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) g.roots)

Tactic:
rw [hg.leadingCoeff, map_one, one_mul] at this

Premises used: map_one, Polynomial.Monic.leadingCoeff, one_mul
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this :
  g =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) g.roots)
rw :
  Multiset.prod
    (Multiset.map
      (fun (x : R) ↦
        eval x
          (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) g.roots)))
      s)
| Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) s)

Tactic:
rw [this]
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this :
  g =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) g.roots)
conv_rhs :
  Eq (α := R) (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (s ×ˢ g.roots)))
    (Multiset.prod
      (Multiset.map
        (fun (x : R) ↦
          eval x
            (Multiset.prod
              (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
                g.roots)))
        s))
⊢ Eq (α := R) (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (s ×ˢ g.roots)))
    (Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) s))

Tactic:
conv_rhs => rw [this]
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this :
  g =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) g.roots)
simp_rw :
  Eq (α := R)
    (Multiset.prod (Multiset.map (fun (x : R) ↦ Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) g.roots)) s))
    (Multiset.prod
      (Multiset.map
        (fun (x : R) ↦
          (Multiset.map
              (Function.comp (β := R[X]) (eval x) fun (x : R) ↦
                HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
              g.roots).prod)
        s))
⊢ Eq (α := R) (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (s ×ˢ g.roots)))
    (Multiset.prod
      (Multiset.map
        (fun (x : R) ↦
          eval x
            (Multiset.prod
              (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
                g.roots)))
        s))

Tactic:
simp_rw [eval_multiset_prod, Multiset.prod_map_product_eq_prod_prod, Multiset.map_map]

Premises used: Polynomial.eval_multiset_prod, Multiset.prod_map_product_eq_prod_prod, Multiset.map_map
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this :
  g =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) g.roots)
h :
  ∀ (x : R) (hx : x ∈ s),
    ∀ x_1 ∈ g.roots,
      Eq (α := R → R) (HSub.hSub x)
        (Function.comp (β := R[X]) (eval x) fun (x : R) ↦
          HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
⊢ Eq (α := R)
    (Multiset.prod (Multiset.map (fun (x : R) ↦ Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) g.roots)) s))
    (Multiset.prod
      (Multiset.map
        (fun (x : R) ↦
          (Multiset.map
              (Function.comp (β := R[X]) (eval x) fun (x : R) ↦
                HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
              g.roots).prod)
        s))

Tactic:
congr! with x hx
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this :
  g =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) g.roots)
x : R
hx : x ∈ s
x_1 : R
h_1 : x_1 ∈ g.roots
h :
  ∀ (x_2 : R),
    x - x_2 =
      Function.comp (β := R[X]) (eval x)
        (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) x_2
⊢ Eq (α := R → R) (HSub.hSub x)
    (Function.comp (β := R[X]) (eval x) fun (x : R) ↦
      HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this :
  g =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) g.roots)
x : R
hx : x ∈ s
x_1 : R
h : x_1 ∈ g.roots
x_2 : R
⊢ x - x_2 =
    Function.comp (β := R[X]) (eval x)
      (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) x_2

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
trans :
  Eq (α := R) (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (g.roots ×ˢ s)))
    (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)))
trans₁ :
  Multiset.prod (Multiset.map (fun (ij : R × R) ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)) =
    HPow.hPow (α := R) (-1) (s.card * g.roots.card) * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) s)
⊢ Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (g.roots ×ˢ s)) =
    HPow.hPow (α := R) (-1) (s.card * g.roots.card) * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) s)

Tactic:
trans ((s ×ˢ g.roots).map fun ij ↦ (-1) * (ij.1 - ij.2)).prod

Premises used: Polynomial.roots, HMul.hMul, Multiset.map, SProd.sprod, Multiset.prod, HSub.hSub, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
rw :
  Eq (α := R) (Multiset.prod (Multiset.map ((fun (ij : R × R) ↦ ij.1 - ij.2) ∘ Prod.swap) (s ×ˢ g.roots)))
    (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)))
⊢ Eq (α := R) (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (g.roots ×ˢ s)))
    (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)))

Tactic:
rw [← Multiset.map_swap_product, Multiset.map_map]

Premises used: Multiset.map_map, Multiset.map_swap_product
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ Eq (α := R) (Multiset.prod (Multiset.map ((fun (ij : R × R) ↦ ij.1 - ij.2) ∘ Prod.swap) (s ×ˢ g.roots)))
    (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
rw :
  HMul.hMul (α := R) (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ -1) (s ×ˢ g.roots)))
      (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (s ×ˢ g.roots))) =
    HPow.hPow (α := R) (-1) (s.card * g.roots.card) * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) s)
⊢ Multiset.prod (Multiset.map (fun (ij : R × R) ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)) =
    HPow.hPow (α := R) (-1) (s.card * g.roots.card) * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) s)

Tactic:
rw [Multiset.prod_map_mul]

Premises used: Multiset.prod_map_mul
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ HMul.hMul (α := R) (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ -1) (s ×ˢ g.roots)))
      (Multiset.prod (Multiset.map (fun (ij : R × R) ↦ ij.1 - ij.2) (s ×ˢ g.roots))) =
    HPow.hPow (α := R) (-1) (s.card * g.roots.card) * Multiset.prod (Multiset.map (fun (x : R) ↦ eval x g) s)

Tactic:
simp [map_sub_sprod_roots_eq_prod_map_eval _ _ hg hg']

Premises used: Polynomial.map_sub_sprod_roots_eq_prod_map_eval
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : DivisionSemiring R
f : R[X]
hf : f.natDegree ≤ 1
obtain :
  ∀ (a b : R)
    (hf :
      (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),
    (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
⊢ f.Splits

Tactic:
obtain ⟨a, b, rfl⟩ := exists_eq_X_add_C_of_natDegree_le_one hf

Premises used: Polynomial.exists_eq_X_add_C_of_natDegree_le_one, rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : DivisionSemiring R
a b : R
hf :
  (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
pos :
  ∀ (ha : a = 0),
    (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
neg :
  ∀ (ha : ¬a = 0),
    (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
⊢ (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

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : DivisionSemiring R
a b : R
hf :
  (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
ha : a = 0
⊢ (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

Tactic:
simp_all