awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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])
⊢ 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 neg : ∀ (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
-- 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
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])
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])) 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])) f.roots) :
        R[X])
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]
inst_1 : IsDomain R
hf : f.Splits
hf0 : ¬f.leadingCoeff = 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])
⊢ 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 neg : f.roots = m
Tactic: suffices hf : f.roots = m by rwa [hf]
-- 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
hf0 : ¬f.leadingCoeff = 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])
⊢ f.roots = m
have neg : (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
        R[X])).roots =
  m
Tactic: rw [hm, roots_C_mul _ hf0, roots_multiset_prod_X_sub_C]
-- 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
hf0 : ¬f.leadingCoeff = 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])
neg :
  (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
          R[X])).roots =
    m
⊢ f.roots = m
have neg₁ : roots
    (Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m)) =
  m
Tactic: rw [hm, roots_C_mul _ hf0, roots_multiset_prod_X_sub_C]
-- 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
hf0 : ¬f.leadingCoeff = 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])
neg :
  (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m) :
          R[X])).roots =
    m
neg₁ :
  roots
      (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) m)) =
    m
⊢ f.roots = m
have neg₂ : m = m
Tactic: rw [hm, roots_C_mul _ hf0, roots_multiset_prod_X_sub_C]
-- 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
hm : f.Monic
| f
have rw : Multiset.prod (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots)
Tactic: rw [hf.eq_prod_roots, hm.leadingCoeff, C_1, one_mul]
-- 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
hm : f.Monic
⊢ f =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots)
have conv_lhs : f =
  Multiset.prod
    (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots)
Tactic: conv_lhs => rw [hf.eq_prod_roots, hm.leadingCoeff, C_1, one_mul]
-- 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
hm : f.Monic
conv_lhs :
  f =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots)
⊢ f =
    Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots)
have conv_lhs₁ : Eq (α := 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))
  (Multiset.prod
    (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots))
Tactic: conv_lhs => rw [hf.eq_prod_roots, hm.leadingCoeff, C_1, one_mul]
-- 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
x : R
| eval x f
have rw : eval x
  (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
    (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) :
      R[X]))
Tactic: rw [hf.eq_prod_roots]
-- 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
x : R
⊢ eval x f = f.leadingCoeff * Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) f.roots)
have conv_lhs : eval x
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) :
        R[X])) =
  f.leadingCoeff * Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) f.roots)
Tactic: conv_lhs => rw [hf.eq_prod_roots]
-- 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
inst_2 : DecidableEq R
hf : f.Splits
x : R
| eval x ((derivative : (a : R[X]) → R[X]) f)
have rw : eval x
  ((derivative : (a : R[X]) → R[X])
    (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (Multiset.prod
          (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) :
        R[X])))
Tactic: rw [hf.eq_prod_roots]
-- 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
inst_2 : DecidableEq R
hf : f.Splits
x : R
⊢ eval x ((derivative : (a : R[X]) → R[X]) f) =
    f.leadingCoeff *
      Multiset.sum
        (Multiset.map (fun (a : R) ↦ Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) (f.roots.erase a))) f.roots)
have conv_lhs : eval x
    ((derivative : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (Multiset.prod
            (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) :
          R[X]))) =
  f.leadingCoeff *
    Multiset.sum
      (Multiset.map (fun (a : R) ↦ Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) (f.roots.erase a))) f.roots)
Tactic: conv_lhs => rw [hf.eq_prod_roots]
-- 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
inst_2 : DecidableEq R
hf : f.Splits
hm : f.Monic
x : R
hx : x ∈ f.roots
⊢ eval x ((derivative : (a : R[X]) → R[X]) f) = Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) (f.roots.erase x))
have rw : eval x ((derivative : (a : R[X]) → R[X]) f) =
  eval x
    ((derivative : (a : R[X]) → R[X])
      (Multiset.prod
        (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) f.roots)))
Tactic: rw [← eval_multiset_prod_X_sub_C_derivative hx, ← hf.eq_prod_roots_of_monic 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
inst_2 : DecidableEq R
hf : f.Splits
hm : f.Monic
x : R
hx : x ∈ f.roots
rw :
  eval x ((derivative : (a : R[X]) → R[X]) f) =
    eval x
      ((derivative : (a : R[X]) → R[X])
        (Multiset.prod
          (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) f.roots)))
⊢ eval x ((derivative : (a : R[X]) → R[X]) f) = Multiset.prod (Multiset.map (fun (x_1 : R) ↦ x - x_1) (f.roots.erase x))
have rw₁ : eval x ((derivative : (a : R[X]) → R[X]) f) = eval x ((derivative : (a : R[X]) → R[X]) f)
Tactic: rw [← eval_multiset_prod_X_sub_C_derivative hx, ← hf.eq_prod_roots_of_monic hm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
S : Type u_4
inst_1 : CommRing S
inst_2 : IsDomain S
i : R →+* S
hi_1 : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑i : (a : R) → S)
hf : (map i f).Splits
hi : ∀ a ∈ (map i f).roots, Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_4} (R := R) i) a
⊢ f.Splits
have choose : ∀ (j : (a : S) → a ∈ (map i f).roots → R) (hj : ∀ (a : S) (a_1 : a ∈ (map i f).roots), (i : (a : R) → S) (j a a_1) = a),
  f.Splits
Tactic: choose j hj using hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
S : Type u_4
inst_1 : CommRing S
inst_2 : IsDomain S
i : R →+* S
hi : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑i : (a : R) → S)
hf : (map i f).Splits
j : (a : S) → a ∈ (map i f).roots → R
hj : ∀ (a : S) (a_1 : a ∈ (map i f).roots), (i : (a : R) → S) (j a a_1) = a
⊢ f.Splits
have rw : ∃ (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: rw [splits_iff_exists_multiset]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
S : Type u_4
inst_1 : CommRing S
inst_2 : IsDomain S
i : R →+* S
hi : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑i : (a : R) → S)
hf : (map i f).Splits
j : (a : S) → a ∈ (map i f).roots → R
hj : ∀ (a : S) (a_1 : a ∈ (map i f).roots), (i : (a : R) → S) (j a a_1) = a
⊢ ∃ (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 : map i f =
  map i
    (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.pmap (p := Membership.mem (map i f).roots) j (map i f).roots sorry)) :
        R[X]))
Tactic: refine ⟨(f.map i).roots.pmap j fun _ ↦ id, map_injective i hi ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
S : Type u_4
inst_1 : CommRing S
inst_2 : IsDomain S
i : R →+* S
hi : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑i : (a : R) → S)
hf : (map i f).Splits
j : (a : S) → a ∈ (map i f).roots → R
hj : ∀ (a : S) (a_1 : a ∈ (map i f).roots), (i : (a : R) → S) (j a a_1) = a
| map i f
have rw : HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((i : (a : R) → S) f.leadingCoeff) : S[X])
  (Multiset.prod
      (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
        (map i f).roots) :
    S[X])
Tactic: rw [hf.eq_prod_roots, leadingCoeff_map_of_injective hi]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
S : Type u_4
inst_1 : CommRing S
inst_2 : IsDomain S
i : R →+* S
hi : Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := S) (⇑i : (a : R) → S)
hf : (map i f).Splits
j : (a : S) → a ∈ (map i f).roots → R
hj : ∀ (a : S) (a_1 : a ∈ (map i f).roots), (i : (a : R) → S) (j a a_1) = a
⊢ map i f =
    map i
      (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.pmap (p := Membership.mem (map i f).roots) j (map i f).roots ⋯)) :
          R[X]))
have conv_lhs : HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) ((i : (a : R) → S) f.leadingCoeff) : S[X])
    (Multiset.prod
        (Multiset.map (fun (x : S) ↦ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]))
          (map i f).roots) :
      S[X]) =
  map i
    (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.pmap (p := Membership.mem (map i f).roots) j (map i f).roots sorry)) :
        R[X]))
Tactic: conv_lhs => rw [hf.eq_prod_roots, leadingCoeff_map_of_injective hi]
-- 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
hm : f.Monic
S : Type u_4
inst_2 : Ring S
i : S →+* R
hr : ∀ a ∈ f.roots, Membership.mem (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) i) a
⊢ f ∈ lifts i
have rw : Multiset.prod
    (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) ∈
  liftsRing i
Tactic: rw [hf.eq_prod_roots_of_monic hm, lifts_iff_liftsRing]
-- 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
hm : f.Monic
S : Type u_4
inst_2 : Ring S
i : S →+* R
hr : ∀ a ∈ f.roots, Membership.mem (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) i) a
⊢ Multiset.prod
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) ∈
    liftsRing i
have refine : ∀ (g : R[X])
  (hg :
    Membership.mem (γ := Multiset R[X])
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) g),
  g ∈ liftsRing i
Tactic: refine Subring.multiset_prod_mem _ _ fun g hg => ?_
-- 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
hm : f.Monic
S : Type u_4
inst_2 : Ring S
i : S →+* R
hr : ∀ a ∈ f.roots, Membership.mem (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) i) a
g : R[X]
hg :
  Membership.mem (γ := Multiset R[X])
    (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots) g
⊢ g ∈ liftsRing i
have obtain : ∀ (x : R) (hx : x ∈ f.roots)
  (hg :
    Membership.mem (γ := Multiset R[X])
      (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) f.roots)
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))),
  HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) ∈ liftsRing i
Tactic: obtain ⟨x, hx, rfl⟩ := Multiset.mem_map.mp hg
Cleared hypotheses: g, hg
-- 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
x : R
hr : f.roots = {x}
⊢ f =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
have rw : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
    (Multiset.prod
        (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) {x}) :
      R[X]) =
  HMul.hMul (α := R[X])
    ((C : (a : R) → R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
            (Multiset.prod
                (Multiset.map (fun (x : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) {x}) :
              R[X])).leadingCoeff :
      R[X])
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
Tactic: rw [hf.eq_prod_roots, hr]
-- 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.natDegree = f.roots.card
have pos : ∀ (hf0 : f.leadingCoeff = 0), f.natDegree = f.roots.card
Tactic: by_cases hf0 : f.leadingCoeff = 0
-- 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
pos : ∀ (hf0 : f.leadingCoeff = 0), f.natDegree = f.roots.card
⊢ f.natDegree = f.roots.card
have neg : ∀ (hf0 : ¬f.leadingCoeff = 0), f.natDegree = f.roots.card
Tactic: by_cases hf0 : f.leadingCoeff = 0
-- 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
hf0 : ¬f.leadingCoeff = 0
| f.natDegree
have rw : f.roots.card
Tactic: rw [hf.eq_prod_roots, natDegree_C_mul hf0, natDegree_multiset_prod_X_sub_C_eq_card]
-- 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
hf0 : ¬f.leadingCoeff = 0
⊢ f.natDegree = f.roots.card
have conv_lhs : f.natDegree = f.roots.card
Tactic: conv_lhs => rw [hf.eq_prod_roots, natDegree_C_mul hf0, natDegree_multiset_prod_X_sub_C_eq_card]
-- 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
hf0 : ¬f.leadingCoeff = 0
conv_lhs : f.natDegree = f.roots.card
⊢ f.natDegree = f.roots.card
have neg : f.roots.card = f.roots.card
Tactic: conv_lhs => rw [hf.eq_prod_roots, natDegree_C_mul hf0, natDegree_multiset_prod_X_sub_C_eq_card]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_4
inst_2 : CommRing S
inst_3 : IsDomain S
f : R[X]
φ : R →+* S
p : R[X]
hp :
  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})
    p
hφ : map φ p ≠ 0
⊢ (map φ p).roots = Multiset.map (⇑φ : (a : R) → S) p.roots
have mem : ∀ (r : R) (hφ : map φ ((C : (a : R) → R[X]) r) ≠ 0),
  (map φ ((C : (a : R) → R[X]) r)).roots =
    Multiset.map.{u_4, u_1} (α := R) (⇑φ : (a : R) → S) (roots ((C : (a : R) → R[X]) r))
Tactic: obtain (⟨r, rfl⟩ | ⟨a, rfl⟩) := hp
Cleared hypotheses: p, hp, hφ
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_4
inst_2 : CommRing S
inst_3 : IsDomain S
f : R[X]
φ : R →+* S
p : R[X]
hp :
  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})
    p
hφ : map φ p ≠ 0
mem :
  ∀ (r : R) (hφ : map φ ((C : (a : R) → R[X]) r) ≠ 0),
    (map φ ((C : (a : R) → R[X]) r)).roots =
      Multiset.map.{u_4, u_1} (α := R) (⇑φ : (a : R) → S) (roots ((C : (a : R) → R[X]) r))
⊢ (map φ p).roots = Multiset.map (⇑φ : (a : R) → S) p.roots
have mem₁ : ∀ (a : R) (hφ : map φ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ≠ 0),
  (map φ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))).roots =
    Multiset.map (⇑φ : (a : R) → S) (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).roots
Tactic: obtain (⟨r, rfl⟩ | ⟨a, rfl⟩) := hp
Cleared hypotheses: p, hp, hφ
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_4
inst_2 : CommRing S
inst_3 : IsDomain S
f : R[X]
hf : f.Splits
φ : R →+* S
hφ : map φ f ≠ 0
⊢ (map φ f).roots = Multiset.map (⇑φ : (a : R) → S) f.roots
have mem : ∀ (p : R[X])
  (hp :
    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})
      p)
  (hφ : map φ p ≠ 0), (map φ p).roots = Multiset.map (⇑φ : (a : R) → S) p.roots
Tactic: induction hf using Submonoid.closure_induction with
  | mem p hp => obtain (⟨r, rfl⟩ | ⟨a, rfl⟩) := hp <;> simp
  | one => simp
  | mul x y _ _ hx hy => simp_all [roots_mul, show x * y ≠ 0 by aesop]
Cleared hypotheses: hf, hφ
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Splits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_4
inst_2 : CommRing S
inst_3 : IsDomain S
f : R[X]
hf : f.Splits
φ : R →+* S
hφ : map φ f ≠ 0
mem :
  ∀ (p : R[X])
    (hp :
      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})
        p)
    (hφ : map φ p ≠ 0), (map φ p).roots = Multiset.map (⇑φ : (a : R) → S) p.roots
⊢ (map φ f).roots = Multiset.map (⇑φ : (a : R) → S) f.roots
have one : ∀ (hφ : map φ 1 ≠ 0), (map φ 1).roots = Multiset.map.{u_4, u_1} (α := R) (⇑φ : (a : R) → S) (roots 1)
Tactic: induction hf using Submonoid.closure_induction with
  | mem p hp => obtain (⟨r, rfl⟩ | ⟨a, rfl⟩) := hp <;> simp
  | one => simp
  | mul x y _ _ hx hy => simp_all [roots_mul, show x * y ≠ 0 by aesop]
Cleared hypotheses: hf, hφ