awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
hf : f.Splits
h_1 : Nontrivial R
a : R
m : Multiset R
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))
ha : a ∈ a ::ₘ m
⊢ (Irreducible (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ∧
      ∀ (m_1 : R[X]),
        Membership.mem (γ := List R[X])
            (Multiset.toList
              (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m))
            m_1 →
          IsUnit m_1) ∧
    IsUnit (M := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])

Tactic:
simp only [irreducible_mul_iff, IsUnit.mul_iff, not_isUnit_X_add_C, false_and, and_false,
      or_false, false_or, ← Multiset.prod_toList, List.prod_isUnit_iff] at h

Premises used: IsUnit.mul_iff, List.prod_isUnit_iff, false_and, Multiset.prod_toList, false_or, Polynomial.not_isUnit_X_add_C, or_false, and_false, irreducible_mul_iff
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
hf : f.Splits
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 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ∧
      ∀ (m_1 : R[X]),
        Membership.mem (γ := List R[X])
            (Multiset.toList
              (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m))
            m_1 →
          IsUnit m_1) ∧
    IsUnit (M := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
⊢ m = 0

Tactic:
simpa [not_isUnit_X_add_C, ← Multiset.eq_zero_iff_forall_notMem] using h.1.2

Premises used: Multiset.eq_zero_iff_forall_notMem, Polynomial.not_isUnit_X_add_C, And.right, And.left
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
hf : f.Splits
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 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ∧
      ∀ (m_1 : R[X]),
        Membership.mem (γ := List R[X])
            (Multiset.toList
              (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m))
            m_1 →
          IsUnit m_1) ∧
    IsUnit (M := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
⊢ m = 0

Tactic:
have : m = 0 := by simpa [not_isUnit_X_add_C, ← Multiset.eq_zero_iff_forall_notMem] using h.1.2
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
hf : f.Splits
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 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ∧
      ∀ (m_1 : R[X]),
        Membership.mem (γ := List R[X])
            (Multiset.toList
              (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m))
            m_1 →
          IsUnit m_1) ∧
    IsUnit (M := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
this : m = 0
inr :
  natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) f.leadingCoeff) +
      (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]))
              0)).natDegree ≤
    1
⊢ f.natDegree ≤ 1

Tactic:
grw [hm, this, natDegree_mul_le]

Premises used: Polynomial.natDegree_mul_le
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
hf : f.Splits
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 (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ∧
      ∀ (m_1 : R[X]),
        Membership.mem (γ := List R[X])
            (Multiset.toList
              (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m))
            m_1 →
          IsUnit m_1) ∧
    IsUnit (M := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
this : m = 0
⊢ natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) f.leadingCoeff) +
      (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]))
              0)).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
⊢ f.degree ≤ 1

Tactic:
degree_le_of_natDegree_le (hf.natDegree_le_one_of_irreducible h)

Premises used: Polynomial.Splits.natDegree_le_one_of_irreducible, Polynomial.degree_le_of_natDegree_le
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
hf : f.Splits
hg : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
inl : ∀ (hg : g.natDegree < 1), (f.comp g).Splits
inr : ∀ (hg : g.natDegree = 1), (f.comp g).Splits
⊢ (f.comp g).Splits

Tactic:
rcases lt_or_eq_of_le hg with hg | hg

Premises used: lt_or_eq_of_le
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
hf : f.Splits
hg_1 : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree < 1
inl : (f.comp ((C : (a : R) → R[X]) (g.coeff 0))).Splits
⊢ (f.comp g).Splits

Tactic:
rw [eq_C_of_natDegree_eq_zero (Nat.lt_one_iff.mp hg)]

Premises used: Polynomial.eq_C_of_natDegree_eq_zero, Nat.lt_one_iff, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
hf : f.Splits
hg_1 : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree < 1
⊢ (f.comp ((C : (a : R) → R[X]) (g.coeff 0))).Splits

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
hf : f.Splits
hg_1 : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
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])) m) :
            R[X])),
    (f.comp g).Splits
⊢ (f.comp g).Splits

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 g : R[X]
hf : f.Splits
hg_1 : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
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])
inr :
  (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (p : R[X]) ↦ p.comp g)
            (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m)) :
        R[X])).Splits
⊢ (f.comp g).Splits

Tactic:
rw [hm, mul_comp, C_comp, multiset_prod_comp]

Premises used: Polynomial.multiset_prod_comp, Polynomial.C_comp, Polynomial.mul_comp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
hf : f.Splits
hg_1 : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
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])
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (p : R[X]) ↦ p.comp g)
            (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m)) :
        R[X])).Splits

Tactic:
(Splits.C _).mul (multisetProd ?_)

Premises used: Polynomial.Splits.multisetProd, Polynomial.Splits.C, Polynomial.Splits.mul
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
hf : f.Splits
hg_1 : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
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])
inr :
  ∀ (f : R[X]),
    Membership.mem (γ := Multiset R[X])
        (Multiset.map (fun (p : R[X]) ↦ p.comp g)
          (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m))
        f →
      f.Splits
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (p : R[X]) ↦ p.comp g)
            (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m)) :
        R[X])).Splits

Tactic:
refine (Splits.C _).mul (multisetProd ?_)

Premises used: Polynomial.Splits.multisetProd, Polynomial.Splits.C, Polynomial.Splits.mul
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
hf : f.Splits
hg_1 : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
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])
inr :
  ∀ (f : R[X]),
    (∃ (a : R[X]),
        (∃ a_1 ∈ m, HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a_1 : R[X]) = a) ∧ a.comp g = f) →
      f.Splits
⊢ ∀ (f : R[X]),
    Membership.mem (γ := Multiset R[X])
        (Multiset.map (fun (p : R[X]) ↦ p.comp g)
          (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 only [Multiset.mem_map]

Premises used: Multiset.mem_map
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
hf : f.Splits
hg_1 : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
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
⊢ ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).comp g).natDegree ≤ 1

Tactic:
simpa
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
hf : f.Splits
hg_1 : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
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
inr : Invertible ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).comp g).leadingCoeff
⊢ ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).comp g).Splits

Tactic:
apply splits_of_natDegree_le_one_of_invertible (by simpa)

Premises used: Polynomial.splits_of_natDegree_le_one_of_invertible
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
hf : f.Splits
hg_1 : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree = 1
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
inr :
  (h : Invertible (g.coeff 1)) →
    (hg : g.natDegree = 1) →
      (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) →
            Invertible ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).comp g).leadingCoeff
⊢ Invertible ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).comp g).leadingCoeff

Tactic:
rw [leadingCoeff, hg] at h

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
hf : f.Splits
hg_1 : g.natDegree ≤ 1
h : Invertible (g.coeff 1)
hg : g.natDegree = 1
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
⊢ Invertible ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).comp g).leadingCoeff

Tactic:
simpa [leadingCoeff, hg]

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
hf : f.Splits
hg : g.degree ≤ 1
h : Invertible g.leadingCoeff
⊢ (f.comp g).Splits

Tactic:
hf.comp_of_natDegree_le_one_of_invertible (natDegree_le_of_degree_le hg) h

Premises used: Polynomial.natDegree_le_of_degree_le, Polynomial.Splits.comp_of_natDegree_le_one_of_invertible
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
hf : f.Splits
hg : g.natDegree ≤ 1
h : g.Monic
⊢ (f.comp g).Splits

Tactic:
hf.comp_of_natDegree_le_one_of_invertible hg (h.leadingCoeff ▸ invertibleOne)

Premises used: Eq.rec, Polynomial.Monic.leadingCoeff, Eq.symm, Polynomial.Splits.comp_of_natDegree_le_one_of_invertible, invertibleOne
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
hf : f.Splits
hg : g.degree ≤ 1
h : g.Monic
⊢ (f.comp g).Splits

Tactic:
hf.comp_of_natDegree_le_one_of_monic (natDegree_le_of_degree_le hg) h

Premises used: Polynomial.natDegree_le_of_degree_le, Polynomial.Splits.comp_of_natDegree_le_one_of_monic
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
hf : f.Splits
a : R
⊢ (f.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))).Splits

Tactic:
hf.comp_of_natDegree_le_one_of_monic (natDegree_add_C.trans_le natDegree_X_le) (monic_X_add_C a)

Premises used: Polynomial.monic_X_add_C, Eq.trans_le, Polynomial.natDegree_X_le, Polynomial.Splits.comp_of_natDegree_le_one_of_monic, Polynomial.natDegree_add_C
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
hf : Splits (map (algebraMap R A) f)
e : A →ₐ[R] B
rw : Splits (map (↑e : A →+* B) (map (algebraMap R A) f))
⊢ Splits (map (algebraMap R B) f)

Tactic:
rw [← e.comp_algebraMap, ← map_map]

Premises used: AlgHom.comp_algebraMap, Polynomial.map_map
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
A : Type u_2
B : Type u_3
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
hf : Splits (map (algebraMap R A) f)
e : A →ₐ[R] B
⊢ Splits (map (↑e : A →+* B) (map (algebraMap R A) f))

Tactic:
apply hf.map

Premises used: Polynomial.Splits.map
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
A : Type u_2
B : Type u_3
inst_1 : CommSemiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
hf : Splits (map (algebraMap R A) f)
⊢ Splits (map (algebraMap R B) f)

Tactic:
hf.of_algHom (IsScalarTower.toAlgHom R A B)

Premises used: IsScalarTower.toAlgHom, Polynomial.Splits.of_algHom
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Ring R
a : R
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).Splits

Tactic:
simpa using Splits.X_add_C (-a)

Premises used: Polynomial.Splits.X_add_C, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Ring R
f : R[X]
hf : f.Splits
rw : ((C : (a : R) → R[X]) (-1) * f).Splits
⊢ (-f).Splits

Tactic:
rw [← neg_one_mul, ← C_1, ← C_neg]

Premises used: Polynomial.C_1, neg_one_mul, Polynomial.C_neg
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Ring R
f : R[X]
hf : f.Splits
⊢ ((C : (a : R) → R[X]) (-1) * f).Splits

Tactic:
hf.C_mul (-1)

Premises used: Polynomial.Splits.C_mul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Ring R
f : R[X]
hf : f.Splits
⊢ ((C : (a : R) → R[X]) (-1) * f).Splits

Tactic:
exact hf.C_mul (-1)

Premises used: Polynomial.Splits.C_mul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Ring R
f : R[X]
⊢ (-f).Splits ↔ f.Splits

Tactic:
⟨fun hf ↦ neg_neg f ▸ hf.neg, .neg⟩

Premises used: Eq.rec, neg_neg, Iff.intro, Polynomial.Splits.neg
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Ring R
f : R[X]
hf : f.Splits
⊢ Splits.{u_1} (R := R) (comp 1 (-X))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Ring R
f : R[X]
hf : f.Splits
refine :
  ∀ (x : R[X])
    (h :
      Membership.mem (γ := Set R[X])
        ({x : R[X] | ∃ (a : R), (C : (a : R) → R[X]) a = x} ∪
          {x : R[X] | ∃ (a : R), HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]) = x})
        x),
    (x.comp (-X)).Splits
⊢ (f.comp (-X)).Splits

Tactic:
refine Submonoid.closure_induction ?_ (by simp)
    (fun f g _ _ hf hg ↦ mul_comp_neg_X f g ▸ hf.mul hg) hf
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Ring R
f : R[X]
hf : f.Splits
a : R
⊢ Splits.{u_1} (R := R) (comp ((C : (a : R) → R[X]) a) (-X))

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Ring R
f : R[X]
hf : f.Splits
a : R
inr : (-HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).Splits
⊢ ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).comp (-X)).Splits

Tactic:
rw [add_comp, X_comp, C_comp, neg_add_eq_sub, ← neg_sub]

Premises used: neg_sub, neg_add_eq_sub, Polynomial.X_comp, Polynomial.add_comp, Polynomial.C_comp
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Ring R
f : R[X]
hf : f.Splits
a : R
⊢ (-HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).Splits

Tactic:
(X_sub_C a).neg

Premises used: Polynomial.Splits.X_sub_C, Polynomial.Splits.neg
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : Ring R
f : R[X]
hf : f.Splits
a : R
⊢ (-HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).Splits

Tactic:
exact (X_sub_C a).neg

Premises used: Polynomial.Splits.X_sub_C, Polynomial.Splits.neg
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
⊢ 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) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
            R[X])

Tactic:
splits_iff_exists_multiset'.trans ⟨?_, ?_⟩

Premises used: Iff.intro, Iff.trans, Polynomial.splits_iff_exists_multiset'
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
refine_1 :
  (∃ (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])) →
    ∃ (m : Multiset R),
      f =
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
          (Multiset.prod
              (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
            R[X])
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) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
            R[X])) →
    ∃ (m : Multiset R),
      f =
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
          (Multiset.prod
              (Multiset.map (fun (x : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
            R[X])
⊢ 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) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
            R[X])

Tactic:
refine splits_iff_exists_multiset'.trans ⟨?_, ?_⟩

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

Tactic:
simpa
-- Module: Mathlib.Algebra.Polynomial.Splits
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
m : Multiset R
hm :
  f =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ 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) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
          R[X])

Tactic:
exact ⟨m.map (- ·), by simpa⟩