awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Separable
Goal:
F_1 : Type u
inst : Field F_1
p_1 : ℕ
F : Type u
inst_1 : Field F
p : ℕ
HF : CharP F p
hp : 0 < p
n₁ : ℕ
g₂ : F[X]
hg₂ : g₂.Separable
hg₁ : Separable.{u} (R := F) ((expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) g₂)
hf :
  Irreducible (M := F[X])
    ((expand F (p ^ n₁) : (a : F[X]) → F[X]) ((expand F (HPow.hPow (β := ℕ) p 0) : (a : F[X]) → F[X]) g₂) : F[X])
⊢ g₂ = g₂

Tactic:
rfl
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
n : ℕ
a : F
hn : Ne.{u + 1} (α := F) (↑n : F) 0
ha : a ≠ 0
⊢ (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) a : F[X])).Separable

Tactic:
separable_X_pow_sub_C_unit (Units.mk0 a ha) (IsUnit.mk0 (n : F) hn)

Premises used: Polynomial.separable_X_pow_sub_C_unit, Nat.cast, Units.mk0, IsUnit.mk0
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
p n : ℕ
a : F
inst_1 : CharP F p
hn : ¬p ∣ n
ha : a ≠ 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (hn : ¬Eq.{u + 1} (α := F) (↑n : F) 0) (ha : a ≠ 0), Ne.{u + 1} (α := F) (↑n : F) 0
⊢ Ne.{u + 1} (α := F) (↑n : F) 0

Tactic:
rwa [← CharP.cast_eq_zero_iff F p n] at hn

Premises used: CharP.cast_eq_zero_iff
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
n : ℕ
x : F
hn : 0 < n
hx : x ≠ 0
⊢ (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).Separable ↔
    Ne.{u + 1} (α := F) (↑n : F) 0

Tactic:
⟨fun h hn' ↦ ?_, fun h => separable_X_pow_sub_C x h hx⟩

Premises used: Polynomial.separable_X_pow_sub_C, Iff.intro
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
n : ℕ
x : F
hn : 0 < n
hx : x ≠ 0
refine :
  ∀ (h : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).Separable)
    (hn' : Eq.{u + 1} (α := F) (↑n : F) 0), False
⊢ (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).Separable ↔
    Ne.{u + 1} (α := F) (↑n : F) 0

Tactic:
refine ⟨fun h hn' ↦ ?_, fun h => separable_X_pow_sub_C x h hx⟩
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
n : ℕ
x : F
hn : 0 < n
hx : x ≠ 0
h : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).Separable
hn' : Eq.{u + 1} (α := F) (↑n : F) 0
⊢ 0 < (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).natDegree

Tactic:
simp [hn]
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
n : ℕ
x : F
hn : 0 < n
hx : x ≠ 0
h : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).Separable
hn' : Eq.{u + 1} (α := F) (↑n : F) 0
⊢ IsUnit (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X]))

Tactic:
simpa [separable_def, derivative_X_pow, hn', isCoprime_zero_right] using h

Premises used: Polynomial.separable_def, Polynomial.derivative_X_pow, isCoprime_zero_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
n : ℕ
x : F
hn : 0 < n
hx : x ≠ 0
h : (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X n) ((C : (a : F) → F[X]) x : F[X])).Separable
hn' : Eq.{u + 1} (α := F) (↑n : F) 0
⊢ False

Tactic:
exact not_isUnit_of_natDegree_pos (X ^ n - C x) (by simp [hn]) <| by
    simpa [separable_def, derivative_X_pow, hn', isCoprime_zero_right] using h

Premises used: Polynomial.C, Polynomial.not_isUnit_of_natDegree_pos, HSub.hSub, HPow.hPow, Polynomial.X, DFunLike.coe
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
n : ℕ
inl : ∀ (hz : n = 0), (HPow.hPow (α := F[X]) X n - 1).Separable ↔ Ne.{u + 1} (α := F) (↑n : F) 0
inr : ∀ (hpos : n > 0), (HPow.hPow (α := F[X]) X n - 1).Separable ↔ Ne.{u + 1} (α := F) (↑n : F) 0
⊢ (HPow.hPow (α := F[X]) X n - 1).Separable ↔ Ne.{u + 1} (α := F) (↑n : F) 0

Tactic:
rcases (Nat.eq_zero_or_pos n) with (hz | hpos)

Premises used: Nat.eq_zero_or_pos
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
n : ℕ
hz : n = 0
⊢ (HPow.hPow (α := F[X]) X n - 1).Separable ↔ Ne.{u + 1} (α := F) (↑n : F) 0

Tactic:
simp_all [not_separable_zero]

Premises used: Polynomial.not_separable_zero
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
n : ℕ
hpos : n > 0
⊢ (HPow.hPow (α := F[X]) X n - 1).Separable ↔ Ne.{u + 1} (α := F) (↑n : F) 0

Tactic:
X_pow_sub_C_separable_iff hpos one_ne_zero

Premises used: Polynomial.X_pow_sub_C_separable_iff, one_ne_zero
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
n : ℕ
hpos : n > 0
⊢ (HPow.hPow (α := F[X]) X n - 1).Separable ↔ Ne.{u + 1} (α := F) (↑n : F) 0

Tactic:
exact X_pow_sub_C_separable_iff hpos one_ne_zero

Premises used: Polynomial.X_pow_sub_C_separable_iff, one_ne_zero
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : Splits (map (algebraMap F K) p)
simp_rw : #(p.aroots K).toFinset = p.natDegree
⊢ Fintype.card.{v} (↑(p.rootSet K) : Type v) = p.natDegree

Tactic:
simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]

Premises used: Finset.coe_sort_coe, Polynomial.rootSet_def, Fintype.card_coe
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : Splits (map (algebraMap F K) p)
rw : (roots (map (algebraMap F K) p)).card = p.natDegree
rw₁ : natDegree (map (algebraMap F K) p) = p.natDegree
rw₂ rw₃ : p.natDegree = p.natDegree
⊢ #(p.aroots K).toFinset = p.natDegree

Tactic:
rw [Multiset.toFinset_card_of_nodup (nodup_roots hsep.map), ← hsplit.natDegree_eq_card_roots,
    natDegree_map]

Premises used: Polynomial.natDegree_map, Polynomial.Separable.map, Polynomial.Splits.natDegree_eq_card_roots, Multiset.toFinset_card_of_nodup, Polynomial.nodup_roots
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
inst_2 : Algebra F K
p : F[X]
hsep : p.Separable
hsplit : Splits (map (algebraMap F K) p)
simp_rw : Fintype.card.{v} (↑(↑(p.aroots K).toFinset : Set K) : Type v) = p.natDegree
simp_rw₁ : Fintype.card.{v} ↥(p.aroots K).toFinset = p.natDegree
simp_rw₂ : #(p.aroots K).toFinset = p.natDegree
⊢ Fintype.card.{v} (↑(p.rootSet K) : Type v) = p.natDegree

Tactic:
classical
  simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
  rw [Multiset.toFinset_card_of_nodup (nodup_roots hsep.map), ← hsplit.natDegree_eq_card_roots,
    natDegree_map]

Premises used: Finset.coe_sort_coe, Polynomial.natDegree_map, Polynomial.rootSet_def, Polynomial.Separable.map, Polynomial.Splits.natDegree_eq_card_roots, Multiset.toFinset_card_of_nodup, Fintype.card_coe, Polynomial.nodup_roots
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
⊢ f.roots.Nodup ↔ f.Separable

Tactic:
⟨(fun hnsep ↦ ?_).mtr, nodup_roots⟩

Premises used: Function.mtr, Iff.intro, Polynomial.nodup_roots
-- Module: Mathlib.FieldTheory.Separable
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

Tactic:
refine ⟨(fun hnsep ↦ ?_).mtr, nodup_roots⟩
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
hnsep : ¬f.Separable
⊢ ¬(@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ f ((derivative : (a : F[X]) → F[X]) f)).degree = 0

Tactic:
rw [Separable, ← gcd_isUnit_iff, isUnit_iff_degree_eq_zero] at hnsep

Premises used: gcd_isUnit_iff, Polynomial.isUnit_iff_degree_eq_zero, Polynomial.Separable
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
hnsep : ¬(@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ f ((derivative : (a : F[X]) → F[X]) f)).degree = 0
obtain :
  ∀ (x : F)
    (hx : eval x (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ f ((derivative : (a : F[X]) → F[X]) f)) = 0),
    ¬f.roots.Nodup
⊢ ¬f.roots.Nodup

Tactic:
obtain ⟨x, hx⟩ := Splits.exists_eval_eq_zero (Splits.of_dvd h hf (gcd_dvd_left f _)) hnsep

Premises used: Polynomial.Splits.of_dvd, Polynomial.Splits.exists_eval_eq_zero, GCDMonoid.gcd_dvd_left
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
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
simp_rw : ∃ (x : F), 1 < Multiset.count x f.roots
⊢ ¬f.roots.Nodup

Tactic:
simp_rw [Multiset.nodup_iff_count_le_one, not_forall, not_le]

Premises used: not_le, Multiset.nodup_iff_count_le_one, Classical.not_forall
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
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:
⟨x, ((one_lt_rootMultiplicity_iff_isRoot_gcd hf).2 hx).trans_eq f.count_roots.symm⟩

Premises used: Iff.mpr, Polynomial.count_roots, LT.lt.trans_eq, Polynomial.one_lt_rootMultiplicity_iff_isRoot_gcd, Exists.intro, Eq.symm
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
f : F[X]
hf : f ≠ 0
h : f.Splits
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:
exact ⟨x, ((one_lt_rootMultiplicity_iff_isRoot_gcd hf).2 hx).trans_eq f.count_roots.symm⟩
-- Module: Mathlib.FieldTheory.Separable
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
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
⊢ f.roots.Nodup ↔ f.Separable

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⟩

Premises used: not_le, Multiset.nodup_iff_count_le_one, gcd_isUnit_iff, Polynomial.isUnit_iff_degree_eq_zero, Classical.not_forall, Polynomial.Separable
-- Module: Mathlib.FieldTheory.Separable
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
rw₁ rw₂ : f.Separable ↔ f.Separable
⊢ (f.aroots K).Nodup ↔ f.Separable

Tactic:
rw [nodup_roots_iff_of_splits (map_ne_zero hf) h, separable_map]

Premises used: Polynomial.nodup_roots_iff_of_splits, Polynomial.map_ne_zero, Polynomial.separable_map
-- Module: Mathlib.FieldTheory.Separable
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
simp_rw₅ : (f.aroots K).Nodup ↔ f.Separable
⊢ Fintype.card.{v} (↑(f.rootSet 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]

Premises used: Finset.coe_sort_coe, Algebra.algebraMap, Polynomial.nodup_aroots_iff_of_splits, Polynomial.natDegree_map, Polynomial.rootSet_def, Polynomial.Splits.natDegree_eq_card_roots, Multiset.toFinset_card_eq_card_iff_nodup, Fintype.card_coe
-- Module: Mathlib.FieldTheory.Separable
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
simp_rw₅ : (f.aroots K).Nodup ↔ f.Separable
⊢ Fintype.card.{v} (↑(f.rootSet 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]

Premises used: Finset.coe_sort_coe, Algebra.algebraMap, Polynomial.nodup_aroots_iff_of_splits, Polynomial.natDegree_map, Polynomial.rootSet_def, Polynomial.Splits.natDegree_eq_card_roots, Multiset.toFinset_card_eq_card_iff_nodup, Fintype.card_coe
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
x : F
h_sep : Separable.{u} (R := F) 0
h_root : eval x 0 = 0
h_splits : (map i 0).Splits
h_roots : ∀ y ∈ (map i 0).roots, y = (i : (a : F) → K) x
⊢ False

Tactic:
not_separable_zero h_sep

Premises used: Polynomial.not_separable_zero
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u
inst : Field F
K : Type v
inst_1 : Field K
i : F →+* K
x : F
h_sep : Separable.{u} (R := F) 0
h_root : eval x 0 = 0
h_splits : (map i 0).Splits
h_roots : ∀ y ∈ (map i 0).roots, y = (i : (a : F) → K) x
⊢ False

Tactic:
exact not_separable_zero h_sep

Premises used: Polynomial.not_separable_zero
-- Module: Mathlib.FieldTheory.Separable
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 ≠ 0

Tactic:
have h_ne_zero : h ≠ 0 := by
    rintro rfl
    exact not_separable_zero h_sep
-- Module: Mathlib.FieldTheory.Separable
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
this : (map i h).roots = singleton (α := K) ((i : (a : F) → K) x : K)
⊢ map i h =
    map i
      (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])))

Tactic:
simpa using h_splits.eq_X_sub_C_of_single_root this

Premises used: Polynomial.Splits.eq_X_sub_C_of_single_root
-- Module: Mathlib.FieldTheory.Separable
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
suffices : (map i h).roots = singleton (α := K) ((i : (a : F) → K) x : K)
⊢ 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]))

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)
-- Module: Mathlib.FieldTheory.Separable
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
nodup₁ : Multiset.Nodup (α := K) (singleton (α := K) ((i : (a : F) → K) x : K))
⊢ (map i h).roots = singleton (α := K) ((i : (a : F) → K) x : K)

Tactic:
apply Finset.mk.inj

Premises used: Finset.mk.inj
-- Module: Mathlib.FieldTheory.Separable
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) ∧
    ∀ x_1 ∈ { val := (map i h).roots, nodup := ⋯ : Finset K }, x_1 = (i : (a : F) → K) x
⊢ { val := (map i h).roots, nodup := ⋯ : Finset K } = singleton (α := K) ((i : (a : F) → K) x : K)

Tactic:
rw [Finset.eq_singleton_iff_unique_mem]

Premises used: Finset.eq_singleton_iff_unique_mem
-- Module: Mathlib.FieldTheory.Separable
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)
x₂ : ∀ x_1 ∈ { val := (map i h).roots, nodup := ⋯ : Finset K }, x_1 = (i : (a : F) → K) x
⊢ 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

Tactic:
constructor
-- Module: Mathlib.FieldTheory.Separable
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)
nodup : (map i h).roots.Nodup
⊢ Membership.mem (α := K) { val := (map i h).roots, nodup := ⋯ : Finset K } ((i : (a : F) → K) x : K)

Tactic:
apply Finset.mem_mk.mpr

Premises used: Iff.mpr, Finset.mem_mk
-- Module: Mathlib.FieldTheory.Separable
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₁ : (map i h).IsRoot ((i : (a : F) → K) x)
⊢ Membership.mem (α := K) (map i h).roots ((i : (a : F) → K) x : K)

Tactic:
rw [mem_roots (show h.map i ≠ 0 from map_ne_zero h_ne_zero)]

Premises used: Polynomial.mem_roots, Polynomial.map_ne_zero
-- Module: Mathlib.FieldTheory.Separable
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₁ : Eq.{v + 1} (α := K) ((i : (a : F) → K) 0 : K) (0 : K)
⊢ (map i h).IsRoot ((i : (a : F) → K) x)

Tactic:
rw [IsRoot.def, ← eval₂_eq_eval_map, eval₂_hom, h_root]

Premises used: Polynomial.eval₂_hom, Polynomial.IsRoot.def, Polynomial.eval₂_eq_eval_map
-- Module: Mathlib.FieldTheory.Separable
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
⊢ Eq.{v + 1} (α := K) ((i : (a : F) → K) 0 : K) (0 : K)

Tactic:
map_zero i

Premises used: map_zero
-- Module: Mathlib.FieldTheory.Separable
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
⊢ Eq.{v + 1} (α := K) ((i : (a : F) → K) 0 : K) (0 : K)

Tactic:
exact map_zero i

Premises used: map_zero
-- Module: Mathlib.FieldTheory.Separable
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.Nodup

Tactic:
nodup_roots (Separable.map h_sep)

Premises used: Polynomial.Separable.map, Polynomial.nodup_roots
-- Module: Mathlib.FieldTheory.Separable
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.Nodup

Tactic:
exact nodup_roots (Separable.map h_sep)

Premises used: Polynomial.Separable.map, Polynomial.nodup_roots
-- Module: Mathlib.FieldTheory.Separable
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_1 ∈ { val := (map i h).roots, nodup := ⋯ : Finset K }, x_1 = (i : (a : F) → K) x

Tactic:
h_roots

Premises used: Polynomial.roots, Set.Mem, setOf, dite, Multiset.Mem
-- Module: Mathlib.FieldTheory.Separable
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_1 ∈ { val := (map i h).roots, nodup := ⋯ : Finset K }, x_1 = (i : (a : F) → K) x

Tactic:
exact h_roots
-- Module: Mathlib.FieldTheory.Separable
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])

Tactic:
obtain ⟨s, h⟩ := splits_iff_exists_multiset.1 sp

Premises used: Polynomial.splits_iff_exists_multiset, Iff.mp
-- Module: Mathlib.FieldTheory.Separable
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₁ :
  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])

Tactic:
use s.toFinset

Premises used: Multiset.toFinset