awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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])
⊢ 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))
have h₁ : (HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
    (Multiset.prod
        (Multiset.map (fun (a : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) s) :
      K[X])).Separable
Tactic: apply Separable.of_mul_right
-- 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])
h₁ :
  (HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
      (Multiset.prod
          (Multiset.map (fun (a : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) s) :
        K[X])).Separable
⊢ 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))
have h₂ : K[X]
Tactic: apply Separable.of_mul_right
-- 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: classical
  obtain ⟨s, h⟩ := splits_iff_exists_multiset.1 sp
  use s.toFinset
  rw [h, Finset.prod_eq_multiset_prod, ← Multiset.toFinset_eq, leadingCoeff_map]
  apply nodup_of_separable_prod
  apply Separable.of_mul_right
  rw [← h]
  exact sep.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
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])
⊢ ∃ (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 : ∀ (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])
Tactic: classical
  obtain ⟨s, h⟩ := splits_iff_exists_multiset.1 sp
  use s.toFinset
  rw [h, Finset.prod_eq_multiset_prod, ← Multiset.toFinset_eq, leadingCoeff_map]
  apply nodup_of_separable_prod
  apply Separable.of_mul_right
  rw [← h]
  exact sep.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
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])
h :
  ∀ (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])
⊢ ∃ (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₁ : ∀ (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
Tactic: classical
  obtain ⟨s, h⟩ := splits_iff_exists_multiset.1 sp
  use s.toFinset
  rw [h, Finset.prod_eq_multiset_prod, ← Multiset.toFinset_eq, leadingCoeff_map]
  apply nodup_of_separable_prod
  apply Separable.of_mul_right
  rw [← h]
  exact sep.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
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])
h :
  ∀ (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])
h₁ :
  ∀ (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
⊢ ∃ (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₂ : ∀ (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])),
  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: classical
  obtain ⟨s, h⟩ := splits_iff_exists_multiset.1 sp
  use s.toFinset
  rw [h, Finset.prod_eq_multiset_prod, ← Multiset.toFinset_eq, leadingCoeff_map]
  apply nodup_of_separable_prod
  apply Separable.of_mul_right
  rw [← h]
  exact sep.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
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])
h :
  ∀ (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])
h₁ :
  ∀ (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
h₂ :
  ∀ (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])),
    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))
⊢ ∃ (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₃ : ∀ (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])),
  (HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) (map i f).leadingCoeff : K[X])
      (Multiset.prod
          (Multiset.map (fun (a : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) a : K[X])) s) :
        K[X])).Separable
Tactic: classical
  obtain ⟨s, h⟩ := splits_iff_exists_multiset.1 sp
  use s.toFinset
  rw [h, Finset.prod_eq_multiset_prod, ← Multiset.toFinset_eq, leadingCoeff_map]
  apply nodup_of_separable_prod
  apply Separable.of_mul_right
  rw [← h]
  exact sep.map