awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
refine_1 :
  ∀ (hf : f.Splits),
    ∃ (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])
refine_2 :
  (∃ (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])) →
    f.Splits
⊢ f.Splits ↔
    ∃ (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:
refine ⟨fun hf ↦ ?_, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
hf : f.Splits
S : Submonoid R[X] := MonoidHom.mrange (F := R →+* R[X]) C
⊢ (↑S : Set R[X]) = {x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x}

Tactic:
have hS : S = {C a | a : R} := MonoidHom.coe_mrange C
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
hf : f.Splits
S : Submonoid R[X] := MonoidHom.mrange (F := R →+* R[X]) C
hS : (↑S : Set R[X]) = {x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x}
⊢ let S : Submonoid R[X] := MonoidHom.mrange (F := R →+* R[X]) C;
  ∃ y ∈ S,
    ∃ (z : R[X]),
      Membership.mem (γ := Submonoid R[X])
          (Submonoid.closure
            {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
          z ∧
        y * z = f

Tactic:
rw [Splits, Submonoid.closure_union, ← hS, Submonoid.closure_eq, Submonoid.mem_sup] at hf

Premises used: Submonoid.mem_sup, Submonoid.closure_eq, Submonoid.closure_union, Polynomial.Splits
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
hf : f.Splits
S : Submonoid R[X] := MonoidHom.mrange (F := R →+* R[X]) C
hS : (↑S : Set R[X]) = {x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x}
hf₁ :
  let S : Submonoid R[X] := MonoidHom.mrange (F := R →+* R[X]) C;
  ∃ y ∈ S,
    ∃ (z : R[X]),
      Membership.mem (γ := Submonoid R[X])
          (Submonoid.closure
            {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
          z ∧
        y * z = f
⊢ let S : Submonoid R[X] := MonoidHom.mrange (F := R →+* R[X]) C;
  (↑S : Set R[X]) = {x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x}

Tactic:
rw [Splits, Submonoid.closure_union, ← hS, Submonoid.closure_eq, Submonoid.mem_sup] at hf

Premises used: Submonoid.mem_sup, Submonoid.closure_eq, Submonoid.closure_union, Polynomial.Splits
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
S : Submonoid R[X] := MonoidHom.mrange (F := R →+* R[X]) C
hf :
  ∃ y ∈ S,
    ∃ (z : R[X]),
      Membership.mem (γ := Submonoid R[X])
          (Submonoid.closure
            {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
          z ∧
        y * z = f
hS : (↑S : Set R[X]) = {x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x}
refine_1 :
  ∀ (a : R) (g : R[X])
    (hg :
      Membership.mem (γ := Submonoid R[X])
        (Submonoid.closure
          {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
        g),
    ∃ (m : Multiset R),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) g =
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) g).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])
⊢ ∃ (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:
obtain ⟨-, ⟨a, rfl⟩, g, hg, rfl⟩ := hf

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange (F := R →+* R[X]) C
hS : (↑S : Set R[X]) = {x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x}
a : R
g : R[X]
hg :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
    g
refine_1 :
  ∀ (mg : Multiset R[X])
    (hmg :
      ∀ y ∈ mg,
        Membership.mem (γ := Set R[X])
          {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x} y)
    (hg :
      Membership.mem (γ := Submonoid R[X])
        (Submonoid.closure
          {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
        mg.prod),
    ∃ (m : Multiset R),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) mg.prod =
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) mg.prod).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])
⊢ ∃ (m : Multiset R),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) g =
      HMul.hMul (α := R[X]) (β := R[X])
        ((C : (a : R) → R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) g).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:
obtain ⟨mg, hmg, rfl⟩ := Submonoid.exists_multiset_of_mem_closure hg

Premises used: Submonoid.exists_multiset_of_mem_closure, rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange (F := R →+* R[X]) C
hS : (↑S : Set R[X]) = {x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x}
a : R
mg : Multiset R[X]
hmg :
  ∀ y ∈ mg,
    Membership.mem (γ := Set R[X])
      {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x} y
hg :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
    mg.prod
refine_1 :
  ∀ (j : (y : R[X]) → R) (hj : ∀ y ∈ mg, HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (j y) : R[X]) = y),
    ∃ (m : Multiset R),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) mg.prod =
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) mg.prod).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])
⊢ ∃ (m : Multiset R),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) mg.prod =
      HMul.hMul (α := R[X]) (β := R[X])
        ((C : (a : R) → R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) mg.prod).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:
choose! j hj using hmg
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange (F := R →+* R[X]) C
hS : (↑S : Set R[X]) = {x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x}
a : R
mg : Multiset R[X]
hg :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
    mg.prod
j : (y : R[X]) → R
hj : ∀ y ∈ mg, HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (j y) : R[X]) = y
⊢ mg =
    Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (Multiset.map j mg)

Tactic:
simp [Multiset.map_congr rfl hj]

Premises used: Multiset.map_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange (F := R →+* R[X]) C
hS : (↑S : Set R[X]) = {x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x}
a : R
mg : Multiset R[X]
hg :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
    mg.prod
j : (y : R[X]) → R
hj : ∀ y ∈ mg, HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (j y) : R[X]) = y
⊢ mg =
    Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (Multiset.map j mg)

Tactic:
have hmg : mg = (mg.map j).map (X + C ·) := by simp [Multiset.map_congr rfl hj]
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange (F := R →+* R[X]) C
hS : (↑S : Set R[X]) = {x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x}
a : R
mg : Multiset R[X]
hg :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
    mg.prod
j : (y : R[X]) → R
hj : ∀ y ∈ mg, HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (j y) : R[X]) = y
hmg :
  mg =
    Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (Multiset.map j mg)
refine_1 :
  ∃ (m : Multiset R),
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : 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 j mg)) :
          R[X]) =
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : 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])
refine_1₁ :
  Monic (R := R)
    (Multiset.prod
      (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
        (Multiset.map j mg)))
⊢ ∃ (m : Multiset R),
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) mg.prod =
      HMul.hMul (α := R[X]) (β := R[X])
        ((C : (a : R) → R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) mg.prod).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:
rw [hmg, leadingCoeff_mul_monic, leadingCoeff_C]

Premises used: Polynomial.leadingCoeff_mul_monic, Polynomial.leadingCoeff_C
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange (F := R →+* R[X]) C
hS : (↑S : Set R[X]) = {x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x}
a : R
mg : Multiset R[X]
hg :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
    mg.prod
j : (y : R[X]) → R
hj : ∀ y ∈ mg, HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (j y) : R[X]) = y
hmg :
  mg =
    Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (Multiset.map j mg)
w : Multiset R
h :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : 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 j mg)) :
        R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : 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 j mg)) :
        R[X])
⊢ ∃ (m : Multiset R),
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : 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 j mg)) :
          R[X]) =
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : 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:
use mg.map j

Premises used: Multiset.map
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange (F := R →+* R[X]) C
hS : (↑S : Set R[X]) = {x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x}
a : R
mg : Multiset R[X]
hg :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
    mg.prod
j : (y : R[X]) → R
hj : ∀ y ∈ mg, HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (j y) : R[X]) = y
hmg :
  mg =
    Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (Multiset.map j mg)
refine_1 :
  Monic (R := R)
    (Multiset.prod
      (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
        (Multiset.map j
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
            (Multiset.map j mg)))))
⊢ Monic (R := R)
    (Multiset.prod
      (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
        (Multiset.map j mg)))

Tactic:
rw [hmg]
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange (F := R →+* R[X]) C
hS : (↑S : Set R[X]) = {x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x}
a : R
mg : Multiset R[X]
hg :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
    mg.prod
j : (y : R[X]) → R
hj : ∀ y ∈ mg, HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (j y) : R[X]) = y
hmg :
  mg =
    Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (Multiset.map j mg)
refine_1 :
  ∀
    i ∈
      Multiset.map j
        (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
          (Multiset.map j mg)),
    (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X])).Monic
⊢ Monic (R := R)
    (Multiset.prod
      (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
        (Multiset.map j
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
            (Multiset.map j mg)))))

Tactic:
apply monic_multiset_prod_of_monic

Premises used: Polynomial.monic_multiset_prod_of_monic
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R[X] := MonoidHom.mrange (F := R →+* R[X]) C
hS : (↑S : Set R[X]) = {x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x}
a : R
mg : Multiset R[X]
hg :
  Membership.mem (γ := Submonoid R[X])
    (Submonoid.closure {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
    mg.prod
j : (y : R[X]) → R
hj : ∀ y ∈ mg, HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (j y) : R[X]) = y
hmg :
  mg =
    Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (Multiset.map j mg)
⊢ ∀
    i ∈
      Multiset.map j
        (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
          (Multiset.map j mg)),
    (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) i : R[X])).Monic

Tactic:
simp [monic_X_add_C]

Premises used: Polynomial.monic_X_add_C
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring 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) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
⊢ ∀ (f : R[X]),
    Membership.mem (γ := Multiset R[X])
        (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) f →
      f.Splits

Tactic:
simp [Splits.X_add_C]

Premises used: Polynomial.Splits.X_add_C
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring 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) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
⊢ f.Splits

Tactic:
exact hm ▸ (Splits.C _).mul (.multisetProd (by simp [Splits.X_add_C]))
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
hf : f.Splits
h : Irreducible f
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
hf : f.Splits
h : Irreducible f
h_1 : Nontrivial R
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) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
            R[X])),
    f.natDegree ≤ 1
⊢ f.natDegree ≤ 1

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

Premises used: Iff.mp, Polynomial.splits_iff_exists_multiset'
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
hf : f.Splits
h : Irreducible f
h_1 : Nontrivial 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) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
inl :
  ∀
    (hm :
      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])) 0) :
            R[X])),
    f.natDegree ≤ 1
inr : ∀ (a : R) (ha : a ∈ m), f.natDegree ≤ 1
⊢ f.natDegree ≤ 1

Tactic:
rcases m.empty_or_exists_mem with rfl | ⟨a, ha⟩

Premises used: Multiset.empty_or_exists_mem, rfl
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
hf : f.Splits
h : Irreducible f
h_1 : Nontrivial 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) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) 0) :
        R[X])
inl :
  (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])) 0) :
          R[X])).natDegree ≤
    1
⊢ f.natDegree ≤ 1

Tactic:
rw [hm]
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
hf : f.Splits
h : Irreducible f
h_1 : Nontrivial 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) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) 0) :
        R[X])
⊢ (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])) 0) :
          R[X])).natDegree ≤
    1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
hf : f.Splits
h : Irreducible f
h_1 : Nontrivial 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) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
a : R
ha : a ∈ m
inr :
  ∀ (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) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
                (a ::ₘ m)) :
            R[X]))
    (ha : a ∈ a ::ₘ m), f.natDegree ≤ 1
⊢ f.natDegree ≤ 1

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 : CommSemiring R
f : R[X]
hf : f.Splits
h : Irreducible f
h_1 : Nontrivial R
a : R
m : Multiset R
hm :
  f =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : 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))
ha : a ∈ a ::ₘ m
⊢ Irreducible
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : 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)))

Tactic:
rw [hm] at h
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
hf : f.Splits
h : Irreducible f
h_1 : Nontrivial R
a : R
m : Multiset R
hm :
  f =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : 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))
ha : a ∈ a ::ₘ m
h₁ :
  Irreducible
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : 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)))
⊢ f =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : 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))

Tactic:
rw [hm] at h
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
hf : f.Splits
h : Irreducible f
h_1 : Nontrivial R
a : R
m : Multiset R
hm :
  f =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : 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))
ha : a ∈ a ::ₘ m
h₁ :
  Irreducible
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : 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)))
hm₁ :
  f =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : 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))
⊢ a ∈ a ::ₘ m

Tactic:
rw [hm] at h