awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
inst_1 : CharZero F
f : F[X]
hf : Irreducible f
⊢ f.Separable
have rw : ¬Eq (α := WithBot ℕ) (↑(f.natDegree - 1) : WithBot ℕ) ⊥
Tactic: rw [separable_iff_derivative_ne_zero hf, Ne, ← degree_eq_bot, degree_derivative_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
inst_1 : CharZero F
f : F[X]
hf : Irreducible f
rw : ¬Eq (α := WithBot ℕ) (↑(f.natDegree - 1) : WithBot ℕ) ⊥
⊢ f.Separable
have hp : 0 < f.natDegree
Tactic: rw [separable_iff_derivative_ne_zero hf, Ne, ← degree_eq_bot, degree_derivative_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u_1
K : Type u_3
inst : CommRing F
inst_1 : Ring K
inst_2 : Algebra F K
x : K
h : IsSeparable F x
⊢ IsIntegral F x
have inl : Subsingleton F → IsIntegral F x
Tactic: cases subsingleton_or_nontrivial F
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u_1
K : Type u_3
inst : CommRing F
inst_1 : Ring K
inst_2 : Algebra F K
x : K
h : IsSeparable F x
inl : Subsingleton F → IsIntegral F x
⊢ IsIntegral F x
have inr : Nontrivial F → IsIntegral F x
Tactic: cases subsingleton_or_nontrivial F
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
F : Type u_1
K : Type u_3
inst : CommRing F
inst_1 : Ring K
inst_2 : Algebra F K
x : K
h : IsSeparable F x
h_1 : Subsingleton F
⊢ IsIntegral F x
have this : Subsingleton K
Tactic: haveI := Module.subsingleton F K
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u_1
L : Type u_2
inst : CommRing F
inst_1 : Ring L
inst_2 : Algebra F L
S : Subalgebra F L
⊢ Algebra.IsSeparable.{u_1, u_2} F ↥S ↔ ∀ x ∈ S, IsSeparable F x
have simp_rw : (∀ (x : ↥S), IsSeparable F x) ↔ ∀ x ∈ S, IsSeparable F x
Tactic: simp_rw [Algebra.isSeparable_def, Subtype.forall,
    ← isSeparable_map_iff S.val Subtype.val_injective, coe_val]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u_1
L : Type u_2
inst : CommRing F
inst_1 : Ring L
inst_2 : Algebra F L
S : Subalgebra F L
simp_rw : (∀ (x : ↥S), IsSeparable F x) ↔ ∀ x ∈ S, IsSeparable F x
⊢ Algebra.IsSeparable.{u_1, u_2} F ↥S ↔ ∀ x ∈ S, IsSeparable F x
have simp_rw₁ : (∀ (a : L) (b : a ∈ S), IsSeparable F (Subtype.mk (p := fun (a : L) ↦ a ∈ S) a b)) ↔ ∀ x ∈ S, IsSeparable F x
Tactic: simp_rw [Algebra.isSeparable_def, Subtype.forall,
    ← isSeparable_map_iff S.val Subtype.val_injective, coe_val]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u_1
L : Type u_2
inst : CommRing F
inst_1 : Ring L
inst_2 : Algebra F L
S : Subalgebra F L
simp_rw : (∀ (x : ↥S), IsSeparable F x) ↔ ∀ x ∈ S, IsSeparable F x
simp_rw₁ : (∀ (a : L) (b : a ∈ S), IsSeparable F (Subtype.mk (p := fun (a : L) ↦ a ∈ S) a b)) ↔ ∀ x ∈ S, IsSeparable F x
⊢ Algebra.IsSeparable.{u_1, u_2} F ↥S ↔ ∀ x ∈ S, IsSeparable F x
have simp_rw₂ : (∀ (a : L) (b : a ∈ S),
    IsSeparable F (K := L) ((S.val : (a : ↥S) → L) (Subtype.mk (p := fun (a : L) ↦ a ∈ S) a b) : L)) ↔
  ∀ x ∈ S, IsSeparable F x
Tactic: simp_rw [Algebra.isSeparable_def, Subtype.forall,
    ← isSeparable_map_iff S.val Subtype.val_injective, coe_val]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
F : Type u_1
inst : Field F
E : Type u_3
E' : Type u_4
inst_1 : Field E
inst_2 : Field E'
inst_3 : Algebra F E
inst_4 : Algebra F E'
f : E →ₐ[F] E'
x : E
h : IsSeparable.{u_1, u_4} F (K := E') ((f : (a : E) → E') x : E')
x_1 : Algebra E E' := f.toAlgebra
⊢ IsSeparable F x
have this : IsScalarTower F E E'
Tactic: haveI : IsScalarTower F E E' := IsScalarTower.of_algebraMap_eq fun x => (f.commutes x).symm
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
⊢ Nat.card (S →ₐ[K] L) = pb.dim
have rw : (aroots (minpoly K pb.gen) L).Nodup
Tactic: rw [Nat.card_congr pb.liftEquiv', Nat.subtype_card _ (fun x => Multiset.mem_toFinset),
    ← pb.natDegree_minpoly, ← natDegree_map (algebraMap K L), h_splits.natDegree_eq_card_roots,
    Multiset.toFinset_card_of_nodup]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
⊢ Nat.card (S →ₐ[K] L) = pb.dim
have rw : Nat.card.{u_5} { y : L // y ∈ aroots (minpoly K pb.gen) L } = pb.dim
Tactic: classical
  rw [Nat.card_congr pb.liftEquiv', Nat.subtype_card _ (fun x => Multiset.mem_toFinset),
    ← pb.natDegree_minpoly, ← natDegree_map (algebraMap K L), h_splits.natDegree_eq_card_roots,
    Multiset.toFinset_card_of_nodup]
  exact nodup_roots ((separable_map (algebraMap K L)).mpr h_sep)
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
rw : Nat.card.{u_5} { y : L // y ∈ aroots (minpoly K pb.gen) L } = pb.dim
⊢ Nat.card (S →ₐ[K] L) = pb.dim
have rw₁ : #(aroots (minpoly K pb.gen) L).toFinset = pb.dim
Tactic: classical
  rw [Nat.card_congr pb.liftEquiv', Nat.subtype_card _ (fun x => Multiset.mem_toFinset),
    ← pb.natDegree_minpoly, ← natDegree_map (algebraMap K L), h_splits.natDegree_eq_card_roots,
    Multiset.toFinset_card_of_nodup]
  exact nodup_roots ((separable_map (algebraMap K L)).mpr h_sep)
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
rw : Nat.card.{u_5} { y : L // y ∈ aroots (minpoly K pb.gen) L } = pb.dim
rw₁ : #(aroots (minpoly K pb.gen) L).toFinset = pb.dim
⊢ Nat.card (S →ₐ[K] L) = pb.dim
have rw₂ : #(aroots (minpoly K pb.gen) L).toFinset = natDegree (minpoly K pb.gen)
Tactic: classical
  rw [Nat.card_congr pb.liftEquiv', Nat.subtype_card _ (fun x => Multiset.mem_toFinset),
    ← pb.natDegree_minpoly, ← natDegree_map (algebraMap K L), h_splits.natDegree_eq_card_roots,
    Multiset.toFinset_card_of_nodup]
  exact nodup_roots ((separable_map (algebraMap K L)).mpr h_sep)
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
rw : Nat.card.{u_5} { y : L // y ∈ aroots (minpoly K pb.gen) L } = pb.dim
rw₁ : #(aroots (minpoly K pb.gen) L).toFinset = pb.dim
rw₂ : #(aroots (minpoly K pb.gen) L).toFinset = natDegree (minpoly K pb.gen)
⊢ Nat.card (S →ₐ[K] L) = pb.dim
have rw₃ : #(aroots (minpoly K pb.gen) L).toFinset = natDegree (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
Tactic: classical
  rw [Nat.card_congr pb.liftEquiv', Nat.subtype_card _ (fun x => Multiset.mem_toFinset),
    ← pb.natDegree_minpoly, ← natDegree_map (algebraMap K L), h_splits.natDegree_eq_card_roots,
    Multiset.toFinset_card_of_nodup]
  exact nodup_roots ((separable_map (algebraMap K L)).mpr h_sep)
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
rw : Nat.card.{u_5} { y : L // y ∈ aroots (minpoly K pb.gen) L } = pb.dim
rw₁ : #(aroots (minpoly K pb.gen) L).toFinset = pb.dim
rw₂ : #(aroots (minpoly K pb.gen) L).toFinset = natDegree (minpoly K pb.gen)
rw₃ : #(aroots (minpoly K pb.gen) L).toFinset = natDegree (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
⊢ Nat.card (S →ₐ[K] L) = pb.dim
have rw₄ : #(aroots (minpoly K pb.gen) L).toFinset = (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen))).card
Tactic: classical
  rw [Nat.card_congr pb.liftEquiv', Nat.subtype_card _ (fun x => Multiset.mem_toFinset),
    ← pb.natDegree_minpoly, ← natDegree_map (algebraMap K L), h_splits.natDegree_eq_card_roots,
    Multiset.toFinset_card_of_nodup]
  exact nodup_roots ((separable_map (algebraMap K L)).mpr h_sep)
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
rw : Nat.card.{u_5} { y : L // y ∈ aroots (minpoly K pb.gen) L } = pb.dim
rw₁ : #(aroots (minpoly K pb.gen) L).toFinset = pb.dim
rw₂ : #(aroots (minpoly K pb.gen) L).toFinset = natDegree (minpoly K pb.gen)
rw₃ : #(aroots (minpoly K pb.gen) L).toFinset = natDegree (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
rw₄ : #(aroots (minpoly K pb.gen) L).toFinset = (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen))).card
⊢ Nat.card (S →ₐ[K] L) = pb.dim
have rw₅ : (aroots (minpoly K pb.gen) L).card = (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen))).card
Tactic: classical
  rw [Nat.card_congr pb.liftEquiv', Nat.subtype_card _ (fun x => Multiset.mem_toFinset),
    ← pb.natDegree_minpoly, ← natDegree_map (algebraMap K L), h_splits.natDegree_eq_card_roots,
    Multiset.toFinset_card_of_nodup]
  exact nodup_roots ((separable_map (algebraMap K L)).mpr h_sep)
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
rw : Nat.card.{u_5} { y : L // y ∈ aroots (minpoly K pb.gen) L } = pb.dim
rw₁ : #(aroots (minpoly K pb.gen) L).toFinset = pb.dim
rw₂ : #(aroots (minpoly K pb.gen) L).toFinset = natDegree (minpoly K pb.gen)
rw₃ : #(aroots (minpoly K pb.gen) L).toFinset = natDegree (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
rw₄ : #(aroots (minpoly K pb.gen) L).toFinset = (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen))).card
rw₅ : (aroots (minpoly K pb.gen) L).card = (roots (Polynomial.map (algebraMap K L) (minpoly K pb.gen))).card
⊢ Nat.card (S →ₐ[K] L) = pb.dim
have rw₆ : (aroots (minpoly K pb.gen) L).Nodup
Tactic: classical
  rw [Nat.card_congr pb.liftEquiv', Nat.subtype_card _ (fun x => Multiset.mem_toFinset),
    ← pb.natDegree_minpoly, ← natDegree_map (algebraMap K L), h_splits.natDegree_eq_card_roots,
    Multiset.toFinset_card_of_nodup]
  exact nodup_roots ((separable_map (algebraMap K L)).mpr h_sep)
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
⊢ Fintype.card (S →ₐ[K] L) = pb.dim
have rw : Nat.card (S →ₐ[K] L) = pb.dim
Tactic: rw [Fintype.card_eq_nat_card, AlgHom.natCard_of_powerBasis pb h_sep h_splits]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
rw : Nat.card (S →ₐ[K] L) = pb.dim
⊢ Fintype.card (S →ₐ[K] L) = pb.dim
have rw₁ : pb.dim = pb.dim
Tactic: rw [Fintype.card_eq_nat_card, AlgHom.natCard_of_powerBasis pb h_sep h_splits]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
⊢ Fintype.card (S →ₐ[K] L) = pb.dim
have rw : Nat.card (S →ₐ[K] L) = pb.dim
Tactic: classical
  rw [Fintype.card_eq_nat_card, AlgHom.natCard_of_powerBasis pb h_sep h_splits]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
L : Type u_5
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K S
inst_4 : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (Polynomial.map (algebraMap K L) (minpoly K pb.gen))
rw : Nat.card (S →ₐ[K] L) = pb.dim
⊢ Fintype.card (S →ₐ[K] L) = pb.dim
have rw₁ : pb.dim = pb.dim
Tactic: classical
  rw [Fintype.card_eq_nat_card, AlgHom.natCard_of_powerBasis pb h_sep h_splits]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
x : E
⊢ Membership.mem (α := K) (γ := IntermediateField F K) (separableClosure F K) ((i : (a : E) → K) x : K) ↔
    Membership.mem (γ := IntermediateField F E) (separableClosure F E) x
have simp_rw : IsSeparable.{u, w} F (K := K) ((i : (a : E) → K) x : K) ↔ IsSeparable F x
Tactic: simp_rw [mem_separableClosure_iff, IsSeparable, minpoly.algHom_eq i i.injective]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
x : E
simp_rw : IsSeparable.{u, w} F (K := K) ((i : (a : E) → K) x : K) ↔ IsSeparable F x
⊢ Membership.mem (α := K) (γ := IntermediateField F K) (separableClosure F K) ((i : (a : E) → K) x : K) ↔
    Membership.mem (γ := IntermediateField F E) (separableClosure F E) x
have simp_rw₁ : Separable (minpoly.{u, w} F (B := K) ((i : (a : E) → K) x : K)) ↔ Separable (minpoly F x)
Tactic: simp_rw [mem_separableClosure_iff, IsSeparable, minpoly.algHom_eq i i.injective]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
⊢ comap i (separableClosure F K) = separableClosure F E
have h : ∀ (x : E), x ∈ comap i (separableClosure F K) ↔ Membership.mem (γ := IntermediateField F E) (separableClosure F E) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h : Eq (α := IntermediateField E K) (separableClosure E K) ⊥
⊢ Eq (α := IntermediateField F K) (IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E))
    (separableClosure F K)
have refine : ∀ (x : K) (hx : Membership.mem (γ := IntermediateField F K) (separableClosure F K) x),
  Membership.mem (γ := IntermediateField F K)
    (IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E)) x
Tactic: refine le_antisymm (map_le_of_algHom _) (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
h : Eq (α := IntermediateField E K) (separableClosure E K) ⊥
x : K
hx : Membership.mem (γ := IntermediateField F K) (separableClosure F K) x
⊢ Membership.mem (γ := IntermediateField F K)
    (IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E)) x
have obtain : ∀ (y : E)
  (hx :
    Membership.mem (α := K) (γ := IntermediateField F K) (separableClosure F K) ((algebraMap E K : (a : E) → K) y : K)),
  Membership.mem (α := K) (γ := IntermediateField F K)
    (IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E)) ((algebraMap E K : (a : E) → K) y : K)
Tactic: obtain ⟨y, rfl⟩ := mem_bot.1 <| h ▸ mem_separableClosure_iff.2
    (IsSeparable.tower_top E <| mem_separableClosure_iff.1 hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Normal F E
⊢ Normal.{u, v} F ↥(separableClosure F E)
have rw : Normal.{u, v} F ↥(normalClosure F (↥(separableClosure F E)) E)
Tactic: rw [← separableClosure.normalClosure_eq_self]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsSepClosed E
⊢ Eq (α := IntermediateField F E) (separableClosure F E) ⊥ ↔ IsSepClosed F
have refine : ∀ (h : Eq (α := IntermediateField F E) (separableClosure F E) ⊥) (p : F[X]),
  p.Monic → ∀ (hirr : Irreducible p) (hsep : p.Separable), ∃ (x : F), eval x p = 0
Tactic: refine ⟨fun h ↦ IsSepClosed.of_exists_root _ fun p _ hirr hsep ↦ ?_,
    fun _ ↦ IntermediateField.eq_bot_of_isSepClosed_of_isSeparable _⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsSepClosed E
h : Eq (α := IntermediateField F E) (separableClosure F E) ⊥
p : F[X]
h_1 : p.Monic
hirr : Irreducible p
hsep : p.Separable
⊢ ∃ (x : F), eval x p = 0
have obtain : ∀ (x : E) (hx : Eq.{v + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E)), ∃ (x : F), eval x p = 0
Tactic: obtain ⟨x, hx⟩ := IsSepClosed.exists_aeval_eq_zero E p (degree_pos_of_irreducible hirr).ne' hsep
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : IsSepClosed E
h : Eq (α := IntermediateField F E) (separableClosure F E) ⊥
p : F[X]
h_1 : p.Monic
hirr : Irreducible p
hsep : p.Separable
x : E
hx : Eq.{v + 1} (α := E) ((aeval x : (a : F[X]) → E) p : E) (0 : E)
⊢ ∃ (x : F), eval x p = 0
have obtain : ∀ (x : F)
  (hx :
    Eq.{v + 1} (α := E)
      (((aeval ((AlgHom.toRingHom (Algebra.ofId F E) : (a : F) → E) x) : F[X] →ₐ[F] E) : (a : F[X]) → E) p : E)
      (0 : E)),
  ∃ (x : F), eval x p = 0
Tactic: obtain ⟨x, rfl⟩ := h ▸ mem_separableClosure_iff.2 (hsep.of_dvd <| minpoly.dvd _ x hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
L1 L2 : IntermediateField F E
h1 : Algebra.IsSeparable.{u, v} F ↥L1
h2 : Algebra.IsSeparable.{u, v} F ↥L2
⊢ Algebra.IsSeparable.{u, v} F ↥(L1 ⊔ L2)
have rw : ∀ (h1 : L1 ≤ separableClosure F E) (h2 : L2 ≤ separableClosure F E), L1 ⊔ L2 ≤ separableClosure F E
Tactic: rw [← le_separableClosure_iff] at h1 h2 ⊢
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
ι : Type u_1
t : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsSeparable.{u, v} F ↥(t i)
⊢ Algebra.IsSeparable.{u, v} F ↥(⨆ (i : ι), t i)
have simp_rw : ∀ (h : ∀ (i : ι), t i ≤ separableClosure F E),
  LE.le (α := IntermediateField F E) (⨆ (i : ι), t i) (separableClosure F E)
Tactic: simp_rw [← le_separableClosure_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
⊢ ClosureOperator (IntermediateField F E)
have refine_1 : ∀ (K L : IntermediateField F E) (le : K ≤ L) (x : E)
  (hx :
    Membership.mem (γ := IntermediateField F E)
      ((fun (K : IntermediateField F E) ↦
          (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E) : IntermediateField F E))
        K)
      x),
  Membership.mem (γ := IntermediateField F E)
    ((fun (K : IntermediateField F E) ↦
        (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E) : IntermediateField F E))
      L)
    x
Tactic: refine .mk' (fun K ↦ (separableClosure K E).restrictScalars F) (fun K L le x hx ↦ ?_)
    le_restrictScalars_separableClosure fun K x hx ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
refine_1 :
  ∀ (K L : IntermediateField F E) (le : K ≤ L) (x : E)
    (hx :
      Membership.mem (γ := IntermediateField F E)
        ((fun (K : IntermediateField F E) ↦
            (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E) : IntermediateField F E))
          K)
        x),
    Membership.mem (γ := IntermediateField F E)
      ((fun (K : IntermediateField F E) ↦
          (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E) : IntermediateField F E))
        L)
      x
⊢ ClosureOperator (IntermediateField F E)
have refine_2 : ∀ (K : IntermediateField F E) (x : E)
  (hx :
    Membership.mem (γ := IntermediateField F E)
      ((fun (K : IntermediateField F E) ↦
          (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E) : IntermediateField F E))
        ((fun (K : IntermediateField F E) ↦
            (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E) : IntermediateField F E))
          K))
      x),
  Membership.mem (γ := IntermediateField F E)
    ((fun (K : IntermediateField F E) ↦
        (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E) : IntermediateField F E))
      K)
    x
Tactic: refine .mk' (fun K ↦ (separableClosure K E).restrictScalars F) (fun K L le x hx ↦ ?_)
    le_restrictScalars_separableClosure fun K x hx ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableClosure (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K_1 : Type w
inst_3 : Field K_1
inst_4 : Algebra F K_1
K L : IntermediateField F E
le : K ≤ L
x : E
hx :
  Membership.mem (γ := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥K) (separableClosure (↥K) E))
    x
x_1 : Algebra ↥K ↥L := (inclusion le).toAlgebra
⊢ Membership.mem (γ := IntermediateField F E) (IntermediateField.restrictScalars F (L' := ↥L) (separableClosure (↥L) E))
    x
have this : IsScalarTower (↥K) (↥L) E
Tactic: have : IsScalarTower K L E := .of_algebraMap_eq' rfl