awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
hf :
  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree ≤
    1
ha : a ≠ 0
h : Invertible a
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) b : R[X])).Splits
have inr : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X])
    (HAdd.hAdd (α := R[X]) (β := R[X]) X
      ((C : (a : R) → R[X]) (@Invertible.invOf _ MulOne.toMul MulOne.toOne a _ * b) : R[X]))).Splits
Tactic: rw [← mul_invOf_cancel_left a b, C_mul, ← mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
⊢ Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) p)
have this : ∀ (i : R),
  (HAdd.hAdd (β := R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))
      ((C : (a : R) → R[X]) i : R[X])).Splits
Tactic: have (i : _) : (X + C r + C i).Splits := by simpa [add_assoc] using Splits.X_add_C (r + i)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
this :
  ∀ (i : R),
    (HAdd.hAdd (β := R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))
        ((C : (a : R) → R[X]) i : R[X])).Splits
⊢ Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) p)
have mem : ∀ (x : R[X]),
  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 →
    Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) x)
Tactic: induction hp using Submonoid.closure_induction
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
this :
  ∀ (i : R),
    (HAdd.hAdd (β := R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))
        ((C : (a : R) → R[X]) i : R[X])).Splits
mem :
  ∀ (x : R[X]),
    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 →
      Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) x)
⊢ Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) p)
have one : Splits (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) 1)
Tactic: induction hp using Submonoid.closure_induction
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
hp : p.Splits
r : R
this :
  ∀ (i : R),
    (HAdd.hAdd (β := R[X]) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))
        ((C : (a : R) → R[X]) i : R[X])).Splits
mem :
  ∀ (x : R[X]),
    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 →
      Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) x)
one : Splits (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) 1)
⊢ Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) p)
have mul : ∀ (x y : R[X]),
  Membership.mem (γ := Submonoid R[X])
      (Submonoid.closure
        ({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 →
    Membership.mem (γ := Submonoid R[X])
        (Submonoid.closure
          ({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}))
        y →
      Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) x) →
        Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) y) →
          Splits.{u_1} (R := R) ((Polynomial.taylor r : (a : R[X]) → R[X]) (x * y))
Tactic: induction hp using Submonoid.closure_induction
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommSemiring 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) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
            R[X])
have 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])
Tactic: refine ⟨fun hf ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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])
⊢ 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])
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) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
          R[X])) →
  f.Splits
Tactic: refine ⟨fun hf ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
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
⊢ ∃ (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])
have hS : (↑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
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
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}
⊢ ∃ (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])
have 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
Tactic: rw [Splits, Submonoid.closure_union, ← hS, Submonoid.closure_eq, Submonoid.mem_sup] at hf
Cleared hypotheses: hf, S, hS
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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}
⊢ ∃ (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])
have 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])
Tactic: obtain ⟨-, ⟨a, rfl⟩, g, hg, rfl⟩ := hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
⊢ ∃ (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])
have 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])
Tactic: obtain ⟨mg, hmg, rfl⟩ := Submonoid.exists_multiset_of_mem_closure hg
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
⊢ ∃ (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])
have 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])
Tactic: choose! j hj using hmg
Cleared hypotheses: hmg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (hypothesis)
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
⊢ ∃ (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])
have 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)
Tactic: have hmg : mg = (mg.map j).map (X + C ·) := by simp [Multiset.map_congr rfl hj]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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)
⊢ ∃ (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])
have 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])
Tactic: rw [hmg, leadingCoeff_mul_monic, leadingCoeff_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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])
⊢ ∃ (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])
have 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)))
Tactic: rw [hmg, leadingCoeff_mul_monic, leadingCoeff_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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)
⊢ ∃ (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])
have w : Multiset R
Tactic: use mg.map j
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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
⊢ ∃ (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])
have 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])
Tactic: use mg.map j
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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)
⊢ 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)))
have 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)))))
Tactic: rw [hmg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
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)
⊢ 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)))))
have 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
Tactic: apply monic_multiset_prod_of_monic
-- 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
⊢ f.natDegree ≤ 1
have a : Nontrivial R
Tactic: nontriviality R
-- 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
⊢ f.natDegree ≤ 1
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) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
          R[X])),
  f.natDegree ≤ 1
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 : 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])
⊢ f.natDegree ≤ 1
have 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
Tactic: rcases m.empty_or_exists_mem with rfl | ⟨a, ha⟩
Cleared hypotheses: m, hm