awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : IsDomain A
inst_4 : IsDomain B
inst_5 : Algebra R A
inst_6 : Algebra R B
hf : Splits (map (algebraMap R A) f)
φ : A →ₐ[R] B
hφ : Ne (α := B[X]) (map (algebraMap R B) f) 0
replace : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0
replace₁ :
  ∀ (hφ : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0),
    (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
replace₂ : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0
replace₃ replace₄ :
  ∀ (hφ : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0),
    (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
replace₅ :
  ∀ (hφ : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0)
    (hf :
      roots (map (↑φ : A →+* B) (map (algebraMap R A) f)) =
        Multiset.map (⇑(↑φ : A →+* B) : (a : A) → B) (roots (map (algebraMap R A) f))),
    (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
replace₆ :
  ∀ (hφ : Ne (α := B[X]) (map (↑φ : A →+* B) (map (algebraMap R A) f)) 0)
    (hf :
      roots (map (algebraMap R B) f) = Multiset.map (⇑(↑φ : A →+* B) : (a : A) → B) (roots (map (algebraMap R A) f))),
    (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B
⊢ (⇑φ : (a : A) → B) '' f.rootSet A = f.rootSet B

Tactic:
classical
  replace hφ : (f.map (algebraMap R A)).map (φ : A →+* B) ≠ 0 := by
    rwa [map_map, φ.comp_algebraMap]
  replace hf := hf.roots_map_of_ne_zero hφ
  rw [map_map, φ.comp_algebraMap] at hf
  simp [rootSet, aroots, hf, Multiset.toFinset_map]

Premises used: AlgHom.comp_algebraMap, Polynomial.rootSet, Polynomial.aroots, Multiset.toFinset_map, Polynomial.map_map
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
rw :
  (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])).coeff
    0
| f.coeff 0

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
conv_lhs :
  (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])).coeff
      0 =
    HPow.hPow (α := R) (-1) f.natDegree * f.leadingCoeff * f.roots.prod
⊢ f.coeff 0 = HPow.hPow (α := R) (-1) f.natDegree * f.leadingCoeff * f.roots.prod

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
⊢ (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])).coeff
      0 =
    HPow.hPow (α := R) (-1) f.natDegree * f.leadingCoeff * f.roots.prod

Tactic:
simp [coeff_zero_eq_eval_zero, eval_multiset_prod, hf.natDegree_eq_card_roots,
    mul_assoc, mul_left_comm]

Premises used: Polynomial.eval_multiset_prod, Polynomial.coeff_zero_eq_eval_zero, mul_assoc, mul_left_comm, Polynomial.Splits.natDegree_eq_card_roots
-- 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
⊢ f.coeff 0 = HPow.hPow (α := R) (-1) f.natDegree * f.roots.prod

Tactic:
simp [hf.coeff_zero_eq_leadingCoeff_mul_prod_roots, hm]

Premises used: Polynomial.Splits.coeff_zero_eq_leadingCoeff_mul_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
rw :
  (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])).nextCoeff
| f.nextCoeff

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
conv_lhs :
  (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])).nextCoeff =
    -f.leadingCoeff * f.roots.sum
⊢ f.nextCoeff = -f.leadingCoeff * f.roots.sum

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
⊢ (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])).nextCoeff =
    -f.leadingCoeff * f.roots.sum

Tactic:
simp [Multiset.sum_map_neg', monic_X_sub_C, Monic.nextCoeff_multiset_prod]

Premises used: Polynomial.monic_X_sub_C, Multiset.sum_map_neg', Polynomial.Monic.nextCoeff_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
⊢ f.nextCoeff = -f.roots.sum

Tactic:
simp [hf.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff, hm]

Premises used: Polynomial.Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
a : R
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits ↔ f.Splits

Tactic:
⟨fun hf ↦ ?_, ((Splits.X_sub_C _).mul ·)⟩

Premises used: Polynomial.Splits.X_sub_C, Iff.intro, Polynomial.Splits.mul
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
a : R
refine : ∀ (hf : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits), f.Splits
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits ↔ f.Splits

Tactic:
refine ⟨fun hf ↦ ?_, ((Splits.X_sub_C _).mul ·)⟩
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
a : R
hf : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits
pos : ∀ (hf₀ : f = 0), f.Splits
neg : ∀ (hf₀ : ¬f = 0), f.Splits
⊢ f.Splits

Tactic:
by_cases hf₀ : f = 0
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
a : R
hf : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits
hf₀ : f = 0
⊢ f.Splits

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
a : R
hf : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits
hf₀ : ¬f = 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f =
    HMul.hMul (α := R[X]) (β := R[X])
      ((C : (a : R) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : 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]))
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).roots) :
        R[X])

Tactic:
have := hf.eq_prod_roots
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
a : R
hf : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits
hf₀ : ¬f = 0
this :
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f =
    HMul.hMul (α := R[X]) (β := R[X])
      ((C : (a : R) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : 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]))
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).roots) :
        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]) *
      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:
rw [leadingCoeff_mul, leadingCoeff_X_sub_C, one_mul,
    roots_mul (mul_ne_zero (X_sub_C_ne_zero _) hf₀), roots_X_sub_C,
    Multiset.singleton_add, Multiset.map_cons, Multiset.prod_cons, mul_left_comm] at this

Premises used: Multiset.singleton_add, Multiset.map_cons, Polynomial.leadingCoeff_mul, Multiset.prod_cons, Polynomial.roots_X_sub_C, mul_left_comm, Polynomial.roots_mul, Polynomial.leadingCoeff_X_sub_C, mul_ne_zero, Polynomial.X_sub_C_ne_zero, one_mul
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
a : R
hf : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits
hf₀ : ¬f = 0
this :
  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]) *
      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 :
  (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])).Splits
⊢ f.Splits

Tactic:
rw [mul_left_cancel₀ (X_sub_C_ne_zero _) this]

Premises used: mul_left_cancel₀, Polynomial.X_sub_C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
a : R
hf : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * f).Splits
hf₀ : ¬f = 0
this :
  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]) *
      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])
⊢ (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])).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
⊢ (f * g).Splits ↔ f.Splits ∧ g.Splits

Tactic:
⟨fun h ↦ ?_, and_imp.mpr .mul⟩

Premises used: Iff.mpr, and_imp, Iff.intro, Polynomial.Splits.mul
-- 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
refine : ∀ (h : (f * g).Splits), f.Splits ∧ g.Splits
⊢ (f * g).Splits ↔ f.Splits ∧ g.Splits

Tactic:
refine ⟨fun h ↦ ?_, and_imp.mpr .mul⟩
-- 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
h : (f * g).Splits
generalize : ∀ (p : R[X]) (hp : f * g = p) (h : p.Splits), f.Splits ∧ g.Splits
⊢ f.Splits ∧ g.Splits

Tactic:
generalize hp : f * g = p at *
-- 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
generalize : ∀ (n : ℕ) (hn : p.natDegree = n), f.Splits ∧ g.Splits
⊢ f.Splits ∧ g.Splits

Tactic:
generalize hn : p.natDegree = n

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
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.natDegree = 0 ∧ g.natDegree = 0

Tactic:
rw [← hp, natDegree_mul hf₀ hg₀, Nat.add_eq_zero_iff] at hn

Premises used: Polynomial.natDegree_mul, Nat.add_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
hn : f.natDegree = 0 ∧ g.natDegree = 0
⊢ f.Splits ∧ g.Splits

Tactic:
⟨splits_of_natDegree_eq_zero hn.1, splits_of_natDegree_eq_zero hn.2⟩

Premises used: Polynomial.splits_of_natDegree_eq_zero, And.right, And.left, And.intro
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
f g : R[X]
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
hn : f.natDegree = 0 ∧ g.natDegree = 0
⊢ f.Splits ∧ g.Splits

Tactic:
exact ⟨splits_of_natDegree_eq_zero hn.1, splits_of_natDegree_eq_zero hn.2⟩
-- 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
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
⊢ n + 1 ≠ Zero.zero

Tactic:
simp
-- 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
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
succ : ∀ (a : R) (ha : eval a p = 0), f.Splits ∧ g.Splits
⊢ f.Splits ∧ g.Splits

Tactic:
obtain ⟨a, ha⟩ := Splits.exists_eval_eq_zero h (degree_ne_of_natDegree_ne <| hn ▸ by simp)

Premises used: Polynomial.degree_ne_of_natDegree_ne, Eq.rec, Polynomial.Splits.exists_eval_eq_zero, Eq.symm
-- 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
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
a : R
ha : eval a p = 0
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p

Tactic:
have := dvd_iff_isRoot.mpr ha
-- 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
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
a : R
ha : eval a p = 0
this : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ p
⊢ 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

Tactic:
rw [← hp, (prime_X_sub_C a).dvd_mul] at this

Premises used: Prime.dvd_mul, Polynomial.prime_X_sub_C
-- 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
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
a : R
ha : eval a p = 0
this :
  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
succ :
  ∀
    (hf2 :
      ∀ {R : Type u_1} [inst : CommRing R] [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)
        {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)
        (a : R) (ha : eval a p = 0)
        (this :
          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)
        (hf : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ f), f.Splits ∧ g.Splits)
    (hf : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ f), f.Splits ∧ g.Splits
wlog :
  ∀ {R : Type u_1} [inst : CommRing R] [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)
    {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)
    (a : R) (ha : eval a p = 0)
    (this :
      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)
    (hf : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ f), f.Splits ∧ g.Splits
⊢ f.Splits ∧ g.Splits

Tactic:
wlog hf : X - C a ∣ f with hf2

Premises used: Polynomial.C, Polynomial.X, DFunLike.coe
-- 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
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
a : R
ha : eval a p = 0
this :
  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
hf2 :
  ∀ {R : Type u_1} [inst : CommRing R] [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)
    {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)
    (a : R) (ha : eval a p = 0)
    (this :
      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)
    (hf : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ f), f.Splits ∧ g.Splits
hf : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ f
⊢ f.Splits ∧ g.Splits

Tactic:
.symm <| hf2 n ih hg₀ hf₀ p ((mul_comm g f).trans hp) h hn a ha this.symm <|
        this.resolve_left hf

Premises used: Or.resolve_left, Or.symm, mul_comm, And.symm, Eq.trans
-- 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
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
a : R
ha : eval a p = 0
this :
  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
hf2 :
  ∀ {R : Type u_1} [inst : CommRing R] [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)
    {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)
    (a : R) (ha : eval a p = 0)
    (this :
      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)
    (hf : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ f), f.Splits ∧ g.Splits
hf : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ f
⊢ f.Splits ∧ g.Splits

Tactic:
exact .symm <| hf2 n ih hg₀ hf₀ p ((mul_comm g f).trans hp) h hn a ha this.symm <|
        this.resolve_left hf

Premises used: Or.resolve_left, Or.symm, mul_comm, Eq.trans
-- 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
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
a : R
ha : eval a p = 0
this :
  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
hf : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) ∣ f
obtain :
  ∀ (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).Splits ∧ g.Splits
⊢ f.Splits ∧ g.Splits

Tactic:
obtain ⟨f, rfl⟩ := hf

Premises used: rfl
-- 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) = p

Tactic:
rw [mul_assoc] at hp

Premises used: mul_assoc
-- 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
hp₁ : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) * (f * g) = p
⊢ 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

Tactic:
rw [mul_assoc] at hp

Premises used: mul_assoc