awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
⊢ f.natDegree ≤ 1
have inr : ∀ (a : R) (ha : a ∈ m), f.natDegree ≤ 1
Tactic: rcases m.empty_or_exists_mem with rfl | ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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])
⊢ f.natDegree ≤ 1
have 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
Tactic: rw [hm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
⊢ f.natDegree ≤ 1
have 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
Tactic: obtain ⟨m, rfl⟩ := Multiset.exists_cons_of_mem ha
Cleared hypotheses: m, hm, ha
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
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
⊢ f.natDegree ≤ 1
have 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)))
Tactic: rw [hm] at h
Cleared hypotheses: h, hm, ha
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
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
⊢ f.natDegree ≤ 1
have 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])
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
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])
⊢ f.natDegree ≤ 1
have this : m = 0
Tactic: have : m = 0 := by simpa [not_isUnit_X_add_C, ← Multiset.eq_zero_iff_forall_notMem] using h.1.2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
⊢ f.natDegree ≤ 1
have 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
Tactic: grw [hm, this, natDegree_mul_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
hf : f.Splits
hg : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
⊢ (f.comp g).Splits
have inl : ∀ (hg : g.natDegree < 1), (f.comp g).Splits
Tactic: rcases lt_or_eq_of_le hg with hg | hg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
⊢ (f.comp g).Splits
have inr : ∀ (hg : g.natDegree = 1), (f.comp g).Splits
Tactic: rcases lt_or_eq_of_le hg with hg | hg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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 g).Splits
have inl : (f.comp ((C : (a : R) → R[X]) (g.coeff 0))).Splits
Tactic: rw [eq_C_of_natDegree_eq_zero (Nat.lt_one_iff.mp hg)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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 g).Splits
have 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
Tactic: obtain ⟨m, hm⟩ := splits_iff_exists_multiset'.mp hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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])
⊢ (f.comp g).Splits
have 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
Tactic: rw [hm, mul_comp, C_comp, multiset_prod_comp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
have 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
Tactic: refine (Splits.C _).mul (multisetProd ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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])
⊢ ∀ (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
have 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
Tactic: simp only [Multiset.mem_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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).Splits
have inr : Invertible ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).comp g).leadingCoeff
Tactic: apply splits_of_natDegree_le_one_of_invertible (by simpa)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
⊢ Invertible ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).comp g).leadingCoeff
have 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
Tactic: rw [leadingCoeff, hg] at h
Cleared hypotheses: h, hg, m, hm, a
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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 (algebraMap R B) f)
have rw : Splits (map (↑e : A →+* B) (map (algebraMap R A) f))
Tactic: rw [← e.comp_algebraMap, ← map_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Ring R
f : R[X]
hf : f.Splits
⊢ (-f).Splits
have rw : ((C : (a : R) → R[X]) (-1) * f).Splits
Tactic: rw [← neg_one_mul, ← C_1, ← C_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Ring R
f : R[X]
hf : f.Splits
⊢ (f.comp (-X)).Splits
have 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
Tactic: refine Submonoid.closure_induction ?_ (by simp)
    (fun f g _ _ hf hg ↦ mul_comp_neg_X f g ▸ hf.mul hg) hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Ring R
f : R[X]
hf : f.Splits
a : R
⊢ ((HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).comp (-X)).Splits
have inr : (-HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).Splits
Tactic: rw [add_comp, X_comp, C_comp, neg_add_eq_sub, ← neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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])
have 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])
Tactic: refine splits_iff_exists_multiset'.trans ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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])
⊢ 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])
have 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])
Tactic: refine splits_iff_exists_multiset'.trans ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
⊢ ∃ (a : R), eval a f = 0
have 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) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
          R[X])),
  ∃ (a : R), eval a f = 0
Tactic: obtain ⟨m, hm⟩ := splits_iff_exists_multiset.mp hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
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) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
⊢ ∃ (a : R), eval a f = 0
have pos : ∀ (hf₀ : f.leadingCoeff = 0), ∃ (a : R), eval a f = 0
Tactic: by_cases hf₀ : f.leadingCoeff = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
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) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
pos : ∀ (hf₀ : f.leadingCoeff = 0), ∃ (a : R), eval a f = 0
⊢ ∃ (a : R), eval a f = 0
have neg : ∀ (hf₀ : ¬f.leadingCoeff = 0), ∃ (a : R), eval a f = 0
Tactic: by_cases hf₀ : f.leadingCoeff = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
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) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
hf₀ : ¬f.leadingCoeff = 0
⊢ ∃ (a : R), eval a f = 0
have neg : ∀
  (hm :
    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])) 0) :
          R[X])),
  ∃ (a : R), eval a f = 0
Tactic: obtain rfl | ⟨a, ha⟩ := m.empty_or_exists_mem
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
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) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
hf₀ : ¬f.leadingCoeff = 0
neg :
  ∀
    (hm :
      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])) 0) :
            R[X])),
    ∃ (a : R), eval a f = 0
⊢ ∃ (a : R), eval a f = 0
have neg₁ : ∀ (a : R) (ha : a ∈ m), ∃ (a : R), eval a f = 0
Tactic: obtain rfl | ⟨a, ha⟩ := m.empty_or_exists_mem
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
hf₀ : ¬f.leadingCoeff = 0
hm :
  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])) 0) :
        R[X])
⊢ ∃ (a : R), eval a f = 0
have hf0₁ : Ne (α := WithBot ℕ) 0 0
Tactic: rw [hm, Multiset.map_zero, Multiset.prod_zero, mul_one, degree_C hf₀] at hf0
Cleared hypotheses: hf0, hf₀, hm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
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) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])
hf₀ : ¬f.leadingCoeff = 0
a : R
ha : a ∈ m
⊢ ∃ (a : R), eval a f = 0
have neg : ∀ (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) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
              (a ::ₘ m)) :
          R[X]))
  (ha : a ∈ a ::ₘ m), ∃ (a : R), eval a f = 0
Tactic: obtain ⟨m, rfl⟩ := Multiset.exists_cons_of_mem ha
Cleared hypotheses: m, hm, ha
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
hf₀ : ¬f.leadingCoeff = 0
a : 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) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) (a ::ₘ m)) :
        R[X])
ha : a ∈ a ::ₘ m
⊢ eval a f = 0
have rw : eval a
    (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])) (a ::ₘ m)) :
        R[X])) =
  0
Tactic: rw [hm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
inst_1 : IsDomain R
hf : f.Splits
⊢ 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])) f.roots) :
        R[X])
have pos : ∀ (hf0 : f.leadingCoeff = 0),
  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])) f.roots) :
        R[X])
Tactic: by_cases hf0 : f.leadingCoeff = 0