awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
⊢ f.roots.Nodup ↔ f.Separable
have refine : ∀ (hnsep : ¬f.Separable), ¬f.roots.Nodup
Tactic: classical
  refine ⟨(fun hnsep ↦ ?_).mtr, nodup_roots⟩
  rw [Separable, ← gcd_isUnit_iff, isUnit_iff_degree_eq_zero] at hnsep
  obtain ⟨x, hx⟩ := Splits.exists_eval_eq_zero (Splits.of_dvd h hf (gcd_dvd_left f _)) hnsep
  simp_rw [Multiset.nodup_iff_count_le_one, not_forall, not_le]
  exact ⟨x, ((one_lt_rootMultiplicity_iff_isRoot_gcd hf).2 hx).trans_eq f.count_roots.symm⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
refine : ∀ (hnsep : ¬f.Separable), ¬f.roots.Nodup
⊢ f.roots.Nodup ↔ f.Separable
have refine₁ : ∀ (hnsep : ¬(@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ f ((derivative : (a : F[X]) → F[X]) f)).degree = 0),
  ¬f.roots.Nodup
Tactic: classical
  refine ⟨(fun hnsep ↦ ?_).mtr, nodup_roots⟩
  rw [Separable, ← gcd_isUnit_iff, isUnit_iff_degree_eq_zero] at hnsep
  obtain ⟨x, hx⟩ := Splits.exists_eval_eq_zero (Splits.of_dvd h hf (gcd_dvd_left f _)) hnsep
  simp_rw [Multiset.nodup_iff_count_le_one, not_forall, not_le]
  exact ⟨x, ((one_lt_rootMultiplicity_iff_isRoot_gcd hf).2 hx).trans_eq f.count_roots.symm⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
refine : ∀ (hnsep : ¬f.Separable), ¬f.roots.Nodup
refine₁ :
  ∀ (hnsep : ¬(@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ f ((derivative : (a : F[X]) → F[X]) f)).degree = 0),
    ¬f.roots.Nodup
⊢ f.roots.Nodup ↔ f.Separable
have refine₂ : ∀ (hnsep : ¬(@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ f ((derivative : (a : F[X]) → F[X]) f)).degree = 0)
  (x : F)
  (hx : eval x (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ f ((derivative : (a : F[X]) → F[X]) f)) = 0),
  ¬f.roots.Nodup
Tactic: classical
  refine ⟨(fun hnsep ↦ ?_).mtr, nodup_roots⟩
  rw [Separable, ← gcd_isUnit_iff, isUnit_iff_degree_eq_zero] at hnsep
  obtain ⟨x, hx⟩ := Splits.exists_eval_eq_zero (Splits.of_dvd h hf (gcd_dvd_left f _)) hnsep
  simp_rw [Multiset.nodup_iff_count_le_one, not_forall, not_le]
  exact ⟨x, ((one_lt_rootMultiplicity_iff_isRoot_gcd hf).2 hx).trans_eq f.count_roots.symm⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
refine : ∀ (hnsep : ¬f.Separable), ¬f.roots.Nodup
refine₁ :
  ∀ (hnsep : ¬(@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ f ((derivative : (a : F[X]) → F[X]) f)).degree = 0),
    ¬f.roots.Nodup
refine₂ :
  ∀ (hnsep : ¬(@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ f ((derivative : (a : F[X]) → F[X]) f)).degree = 0)
    (x : F)
    (hx : eval x (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ f ((derivative : (a : F[X]) → F[X]) f)) = 0),
    ¬f.roots.Nodup
⊢ f.roots.Nodup ↔ f.Separable
have refine₃ : ∀ (hnsep : ¬(@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ f ((derivative : (a : F[X]) → F[X]) f)).degree = 0)
  (x : F)
  (hx : eval x (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ f ((derivative : (a : F[X]) → F[X]) f)) = 0),
  ∃ (x : F), 1 < Multiset.count x f.roots
Tactic: classical
  refine ⟨(fun hnsep ↦ ?_).mtr, nodup_roots⟩
  rw [Separable, ← gcd_isUnit_iff, isUnit_iff_degree_eq_zero] at hnsep
  obtain ⟨x, hx⟩ := Splits.exists_eval_eq_zero (Splits.of_dvd h hf (gcd_dvd_left f _)) hnsep
  simp_rw [Multiset.nodup_iff_count_le_one, not_forall, not_le]
  exact ⟨x, ((one_lt_rootMultiplicity_iff_isRoot_gcd hf).2 hx).trans_eq f.count_roots.symm⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (map (algebraMap F K) f)
⊢ (f.aroots K).Nodup ↔ f.Separable
have rw : Separable (map (algebraMap F K) f) ↔ f.Separable
Tactic: rw [nodup_roots_iff_of_splits (map_ne_zero hf) h, separable_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (map (algebraMap F K) f)
rw : Separable (map (algebraMap F K) f) ↔ f.Separable
⊢ (f.aroots K).Nodup ↔ f.Separable
have rw₁ : f.Separable ↔ f.Separable
Tactic: rw [nodup_roots_iff_of_splits (map_ne_zero hf) h, separable_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (map (algebraMap F K) f)
⊢ Fintype.card.{v} (↑(f.rootSet K) : Type v) = f.natDegree ↔ f.Separable
have simp_rw : Fintype.card.{v} (↑(↑(f.aroots K).toFinset : Set K) : Type v) = f.natDegree ↔ f.Separable
Tactic: simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe,
    ← natDegree_map (algebraMap F K), h.natDegree_eq_card_roots,
    Multiset.toFinset_card_eq_card_iff_nodup, nodup_aroots_iff_of_splits hf h]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (map (algebraMap F K) f)
simp_rw : Fintype.card.{v} (↑(↑(f.aroots K).toFinset : Set K) : Type v) = f.natDegree ↔ f.Separable
⊢ Fintype.card.{v} (↑(f.rootSet K) : Type v) = f.natDegree ↔ f.Separable
have simp_rw₁ : Fintype.card.{v} ↥(f.aroots K).toFinset = f.natDegree ↔ f.Separable
Tactic: simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe,
    ← natDegree_map (algebraMap F K), h.natDegree_eq_card_roots,
    Multiset.toFinset_card_eq_card_iff_nodup, nodup_aroots_iff_of_splits hf h]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (map (algebraMap F K) f)
simp_rw : Fintype.card.{v} (↑(↑(f.aroots K).toFinset : Set K) : Type v) = f.natDegree ↔ f.Separable
simp_rw₁ : Fintype.card.{v} ↥(f.aroots K).toFinset = f.natDegree ↔ f.Separable
⊢ Fintype.card.{v} (↑(f.rootSet K) : Type v) = f.natDegree ↔ f.Separable
have simp_rw₂ : #(f.aroots K).toFinset = f.natDegree ↔ f.Separable
Tactic: simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe,
    ← natDegree_map (algebraMap F K), h.natDegree_eq_card_roots,
    Multiset.toFinset_card_eq_card_iff_nodup, nodup_aroots_iff_of_splits hf h]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (map (algebraMap F K) f)
simp_rw : Fintype.card.{v} (↑(↑(f.aroots K).toFinset : Set K) : Type v) = f.natDegree ↔ f.Separable
simp_rw₁ : Fintype.card.{v} ↥(f.aroots K).toFinset = f.natDegree ↔ f.Separable
simp_rw₂ : #(f.aroots K).toFinset = f.natDegree ↔ f.Separable
⊢ Fintype.card.{v} (↑(f.rootSet K) : Type v) = f.natDegree ↔ f.Separable
have simp_rw₃ : #(f.aroots K).toFinset = natDegree (map (algebraMap F K) f) ↔ f.Separable
Tactic: simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe,
    ← natDegree_map (algebraMap F K), h.natDegree_eq_card_roots,
    Multiset.toFinset_card_eq_card_iff_nodup, nodup_aroots_iff_of_splits hf h]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (map (algebraMap F K) f)
simp_rw : Fintype.card.{v} (↑(↑(f.aroots K).toFinset : Set K) : Type v) = f.natDegree ↔ f.Separable
simp_rw₁ : Fintype.card.{v} ↥(f.aroots K).toFinset = f.natDegree ↔ f.Separable
simp_rw₂ : #(f.aroots K).toFinset = f.natDegree ↔ f.Separable
simp_rw₃ : #(f.aroots K).toFinset = natDegree (map (algebraMap F K) f) ↔ f.Separable
⊢ Fintype.card.{v} (↑(f.rootSet K) : Type v) = f.natDegree ↔ f.Separable
have simp_rw₄ : #(f.aroots K).toFinset = (roots (map (algebraMap F K) f)).card ↔ f.Separable
Tactic: simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe,
    ← natDegree_map (algebraMap F K), h.natDegree_eq_card_roots,
    Multiset.toFinset_card_eq_card_iff_nodup, nodup_aroots_iff_of_splits hf h]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (map (algebraMap F K) f)
simp_rw : Fintype.card.{v} (↑(↑(f.aroots K).toFinset : Set K) : Type v) = f.natDegree ↔ f.Separable
simp_rw₁ : Fintype.card.{v} ↥(f.aroots K).toFinset = f.natDegree ↔ f.Separable
simp_rw₂ : #(f.aroots K).toFinset = f.natDegree ↔ f.Separable
simp_rw₃ : #(f.aroots K).toFinset = natDegree (map (algebraMap F K) f) ↔ f.Separable
simp_rw₄ : #(f.aroots K).toFinset = (roots (map (algebraMap F K) f)).card ↔ f.Separable
⊢ Fintype.card.{v} (↑(f.rootSet K) : Type v) = f.natDegree ↔ f.Separable
have simp_rw₅ : (f.aroots K).Nodup ↔ f.Separable
Tactic: simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe,
    ← natDegree_map (algebraMap F K), h.natDegree_eq_card_roots,
    Multiset.toFinset_card_eq_card_iff_nodup, nodup_aroots_iff_of_splits hf h]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (map (algebraMap F K) f)
⊢ Fintype.card.{v} (↑(f.rootSet K) : Type v) = f.natDegree ↔ f.Separable
have simp_rw : Fintype.card.{v} (↑(↑(f.aroots K).toFinset : Set K) : Type v) = f.natDegree ↔ f.Separable
Tactic: classical
  simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe,
    ← natDegree_map (algebraMap F K), h.natDegree_eq_card_roots,
    Multiset.toFinset_card_eq_card_iff_nodup, nodup_aroots_iff_of_splits hf h]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (map (algebraMap F K) f)
simp_rw : Fintype.card.{v} (↑(↑(f.aroots K).toFinset : Set K) : Type v) = f.natDegree ↔ f.Separable
⊢ Fintype.card.{v} (↑(f.rootSet K) : Type v) = f.natDegree ↔ f.Separable
have simp_rw₁ : Fintype.card.{v} ↥(f.aroots K).toFinset = f.natDegree ↔ f.Separable
Tactic: classical
  simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe,
    ← natDegree_map (algebraMap F K), h.natDegree_eq_card_roots,
    Multiset.toFinset_card_eq_card_iff_nodup, nodup_aroots_iff_of_splits hf h]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (map (algebraMap F K) f)
simp_rw : Fintype.card.{v} (↑(↑(f.aroots K).toFinset : Set K) : Type v) = f.natDegree ↔ f.Separable
simp_rw₁ : Fintype.card.{v} ↥(f.aroots K).toFinset = f.natDegree ↔ f.Separable
⊢ Fintype.card.{v} (↑(f.rootSet K) : Type v) = f.natDegree ↔ f.Separable
have simp_rw₂ : #(f.aroots K).toFinset = f.natDegree ↔ f.Separable
Tactic: classical
  simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe,
    ← natDegree_map (algebraMap F K), h.natDegree_eq_card_roots,
    Multiset.toFinset_card_eq_card_iff_nodup, nodup_aroots_iff_of_splits hf h]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (map (algebraMap F K) f)
simp_rw : Fintype.card.{v} (↑(↑(f.aroots K).toFinset : Set K) : Type v) = f.natDegree ↔ f.Separable
simp_rw₁ : Fintype.card.{v} ↥(f.aroots K).toFinset = f.natDegree ↔ f.Separable
simp_rw₂ : #(f.aroots K).toFinset = f.natDegree ↔ f.Separable
⊢ Fintype.card.{v} (↑(f.rootSet K) : Type v) = f.natDegree ↔ f.Separable
have simp_rw₃ : #(f.aroots K).toFinset = natDegree (map (algebraMap F K) f) ↔ f.Separable
Tactic: classical
  simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe,
    ← natDegree_map (algebraMap F K), h.natDegree_eq_card_roots,
    Multiset.toFinset_card_eq_card_iff_nodup, nodup_aroots_iff_of_splits hf h]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (map (algebraMap F K) f)
simp_rw : Fintype.card.{v} (↑(↑(f.aroots K).toFinset : Set K) : Type v) = f.natDegree ↔ f.Separable
simp_rw₁ : Fintype.card.{v} ↥(f.aroots K).toFinset = f.natDegree ↔ f.Separable
simp_rw₂ : #(f.aroots K).toFinset = f.natDegree ↔ f.Separable
simp_rw₃ : #(f.aroots K).toFinset = natDegree (map (algebraMap F K) f) ↔ f.Separable
⊢ Fintype.card.{v} (↑(f.rootSet K) : Type v) = f.natDegree ↔ f.Separable
have simp_rw₄ : #(f.aroots K).toFinset = (roots (map (algebraMap F K) f)).card ↔ f.Separable
Tactic: classical
  simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe,
    ← natDegree_map (algebraMap F K), h.natDegree_eq_card_roots,
    Multiset.toFinset_card_eq_card_iff_nodup, nodup_aroots_iff_of_splits hf h]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
f : F[X]
hf : f ≠ 0
h : Splits (map (algebraMap F K) f)
simp_rw : Fintype.card.{v} (↑(↑(f.aroots K).toFinset : Set K) : Type v) = f.natDegree ↔ f.Separable
simp_rw₁ : Fintype.card.{v} ↥(f.aroots K).toFinset = f.natDegree ↔ f.Separable
simp_rw₂ : #(f.aroots K).toFinset = f.natDegree ↔ f.Separable
simp_rw₃ : #(f.aroots K).toFinset = natDegree (map (algebraMap F K) f) ↔ f.Separable
simp_rw₄ : #(f.aroots K).toFinset = (roots (map (algebraMap F K) f)).card ↔ f.Separable
⊢ Fintype.card.{v} (↑(f.rootSet K) : Type v) = f.natDegree ↔ f.Separable
have simp_rw₅ : (f.aroots K).Nodup ↔ f.Separable
Tactic: classical
  simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe,
    ← natDegree_map (algebraMap F K), h.natDegree_eq_card_roots,
    Multiset.toFinset_card_eq_card_iff_nodup, nodup_aroots_iff_of_splits hf h]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = (i : (a : F) → K) x
⊢ h =
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) h.leadingCoeff : F[X])
      (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X]))
have h_ne_zero : h ≠ 0
Tactic: have h_ne_zero : h ≠ 0 := by
    rintro rfl
    exact not_separable_zero h_sep
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = (i : (a : F) → K) x
h_ne_zero : h ≠ 0
⊢ h =
    HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) h.leadingCoeff : F[X])
      (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X]))
have suffices : (map i h).roots = singleton (α := K) ((i : (a : F) → K) x : K)
Tactic: suffices (map i h).roots = {i x} from
    map_injective i i.injective (by simpa using h_splits.eq_X_sub_C_of_single_root this)
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = (i : (a : F) → K) x
h_ne_zero : h ≠ 0
⊢ (map i h).roots = singleton (α := K) ((i : (a : F) → K) x : K)
have x₁ : { val := (map i h).roots, nodup := sorry : Finset K } = { val := singleton (α := K) ((i : (a : F) → K) x : K), nodup := sorry }
Tactic: apply Finset.mk.inj
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = (i : (a : F) → K) x
h_ne_zero : h ≠ 0
x₁ :
  { val := (map i h).roots, nodup := ⋯ : Finset K } =
    { val := singleton (α := K) ((i : (a : F) → K) x : K), nodup := ⋯ }
⊢ (map i h).roots = singleton (α := K) ((i : (a : F) → K) x : K)
have nodup : (map i h).roots.Nodup
Tactic: apply Finset.mk.inj
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = (i : (a : F) → K) x
h_ne_zero : h ≠ 0
x₁ :
  { val := (map i h).roots, nodup := ⋯ : Finset K } =
    { val := singleton (α := K) ((i : (a : F) → K) x : K), nodup := ⋯ }
nodup : (map i h).roots.Nodup
⊢ (map i h).roots = singleton (α := K) ((i : (a : F) → K) x : K)
have nodup₁ : Multiset.Nodup (α := K) (singleton (α := K) ((i : (a : F) → K) x : K))
Tactic: apply Finset.mk.inj
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = (i : (a : F) → K) x
h_ne_zero : h ≠ 0
⊢ { val := (map i h).roots, nodup := ⋯ : Finset K } = singleton (α := K) ((i : (a : F) → K) x : K)
have x₁ : Membership.mem (α := K) { val := (map i h).roots, nodup := sorry : Finset K } ((i : (a : F) → K) x : K) ∧
  ∀ x_1 ∈ { val := (map i h).roots, nodup := sorry : Finset K }, x_1 = (i : (a : F) → K) x
Tactic: rw [Finset.eq_singleton_iff_unique_mem]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = (i : (a : F) → K) x
h_ne_zero : h ≠ 0
⊢ Membership.mem (α := K) { val := (map i h).roots, nodup := ⋯ : Finset K } ((i : (a : F) → K) x : K) ∧
    ∀ x_1 ∈ { val := (map i h).roots, nodup := ⋯ : Finset K }, x_1 = (i : (a : F) → K) x
have x₁ : Membership.mem (α := K) { val := (map i h).roots, nodup := sorry : Finset K } ((i : (a : F) → K) x : K)
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = (i : (a : F) → K) x
h_ne_zero : h ≠ 0
x₁ : Membership.mem (α := K) { val := (map i h).roots, nodup := ⋯ : Finset K } ((i : (a : F) → K) x : K)
⊢ Membership.mem (α := K) { val := (map i h).roots, nodup := ⋯ : Finset K } ((i : (a : F) → K) x : K) ∧
    ∀ x_1 ∈ { val := (map i h).roots, nodup := ⋯ : Finset K }, x_1 = (i : (a : F) → K) x
have x₂ : ∀ x_1 ∈ { val := (map i h).roots, nodup := sorry : Finset K }, x_1 = (i : (a : F) → K) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = (i : (a : F) → K) x
h_ne_zero : h ≠ 0
⊢ Membership.mem (α := K) { val := (map i h).roots, nodup := ⋯ : Finset K } ((i : (a : F) → K) x : K)
have x₁ : Membership.mem (α := K) (map i h).roots ((i : (a : F) → K) x : K)
Tactic: apply Finset.mem_mk.mpr
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = (i : (a : F) → K) x
h_ne_zero : h ≠ 0
x₁ : Membership.mem (α := K) (map i h).roots ((i : (a : F) → K) x : K)
⊢ Membership.mem (α := K) { val := (map i h).roots, nodup := ⋯ : Finset K } ((i : (a : F) → K) x : K)
have nodup : (map i h).roots.Nodup
Tactic: apply Finset.mem_mk.mpr
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = (i : (a : F) → K) x
h_ne_zero : h ≠ 0
⊢ Membership.mem (α := K) (map i h).roots ((i : (a : F) → K) x : K)
have x₁ : (map i h).IsRoot ((i : (a : F) → K) x)
Tactic: rw [mem_roots (show h.map i ≠ 0 from map_ne_zero h_ne_zero)]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : (map i h).Splits
h_roots : ∀ y ∈ (map i h).roots, y = (i : (a : F) → K) x
h_ne_zero : h ≠ 0
⊢ (map i h).IsRoot ((i : (a : F) → K) x)
have x₁ : Eq.{v + 1} (α := K) ((i : (a : F) → K) 0 : K) (0 : K)
Tactic: rw [IsRoot.def, ← eval₂_eq_eval_map, eval₂_hom, h_root]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : (map i f).Splits
⊢ ∃ (s : Finset K),
    map i f =
      HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) ((i : (a : F) → K) f.leadingCoeff) : K[X])
        (∏ a ∈ s, HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) : K[X])
have obtain : ∀ (s : Multiset K)
  (h :
    map i f =
      HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
        (Multiset.prod
            (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) s) :
          K[X])),
  ∃ (s : Finset K),
    map i f =
      HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) ((i : (a : F) → K) f.leadingCoeff) : K[X])
        (∏ a ∈ s, HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) : K[X])
Tactic: obtain ⟨s, h⟩ := splits_iff_exists_multiset.1 sp
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : (map i f).Splits
s : Multiset K
h :
  map i f =
    HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
      (Multiset.prod
          (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) s) :
        K[X])
⊢ ∃ (s : Finset K),
    map i f =
      HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) ((i : (a : F) → K) f.leadingCoeff) : K[X])
        (∏ a ∈ s, HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) : K[X])
have h₁ : map i f =
  HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) ((i : (a : F) → K) f.leadingCoeff) : K[X])
    (∏ a ∈ s.toFinset, HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) : K[X])
Tactic: use s.toFinset
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : (map i f).Splits
s : Multiset K
h :
  map i f =
    HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
      (Multiset.prod
          (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) s) :
        K[X])
⊢ map i f =
    HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) ((i : (a : F) → K) f.leadingCoeff) : K[X])
      (∏ a ∈ s.toFinset, HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X]) : K[X])
have h₁ : s.Nodup
Tactic: rw [h, Finset.prod_eq_multiset_prod, ← Multiset.toFinset_eq, leadingCoeff_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
f : F[X]
sep : f.Separable
sp : (map i f).Splits
s : Multiset K
h :
  map i f =
    HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
      (Multiset.prod
          (Multiset.map (fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) s) :
        K[X])
⊢ s.Nodup
have h₁ : Separable (R := K)
  (Multiset.prod (Multiset.map (fun (a : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) s))
Tactic: apply nodup_of_separable_prod