awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ (σ : Lifts F E K), (↑S : Set E) ⊆ (↑σ.carrier : Set E)
this_1 : IsExtendible.{u_1, u_2, u_3} (F := F) (E := E) (K := K) ⊥
ϕ : Lifts F E K
hϕ : Maximal (fun (x : Lifts F E K) ↦ Membership.mem (γ := Set (Lifts F E K)) {ϕ : Lifts F E K | ϕ.IsExtendible} x) ϕ
this_2 : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x : Algebra.{u_2, u_3} (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := AlgHom.{u_2, u_2, u_3} (↥ϕ.carrier) (↥(↥ϕ.carrier)⟮α⟯) K
this : FiniteDimensional.{u_2, u_2} ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : (σ : Λ) → Lifts F E K :=
  fun (σ : Λ) ↦ { carrier := restrictScalars F (L' := ↥ϕ.carrier) (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max :
  ∀ ⦃y : Lifts F E K⦄, ϕ < y → ∃ (S : Finset E), ∀ (τ : Lifts F E K) (_ : τ ≥ y), ¬(↑S : Set E) ⊆ (↑τ.carrier : Set E)
S : (σ : Λ) → Finset E
hS : ∀ (σ : Λ) (τ : Lifts F E K) (_ : τ ≥ L σ), ¬(↑(S σ) : Set E) ⊆ (↑τ.carrier : Set E)
θ : Lifts F E K
hθϕ : θ ≥ ϕ
hθ : (↑({α} ∪ Finset.biUnion Finset.univ S) : Set E) ⊆ (↑θ.carrier : Set E)
⊢ α ∈ (↑θ.carrier : Set E) ∧ ∀ (i : Λ), (↑(S i) : Set E) ⊆ (↑θ.carrier : Set E)

Tactic:
simp_rw [Finset.coe_union, Set.union_subset_iff, Finset.coe_singleton, Set.singleton_subset_iff,
    Finset.coe_biUnion, Finset.coe_univ, Set.mem_univ, Set.iUnion_true, Set.iUnion_subset_iff] at hθ

Premises used: Set.singleton_subset_iff, Finset.coe_biUnion, Finset.coe_singleton, Finset.coe_univ, Set.iUnion_subset_iff, Set.union_subset_iff, Set.iUnion_true, Set.mem_univ, Finset.coe_union
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ (σ : Lifts F E K), (↑S : Set E) ⊆ (↑σ.carrier : Set E)
this_1 : IsExtendible.{u_1, u_2, u_3} (F := F) (E := E) (K := K) ⊥
ϕ : Lifts F E K
hϕ : Maximal (fun (x : Lifts F E K) ↦ Membership.mem (γ := Set (Lifts F E K)) {ϕ : Lifts F E K | ϕ.IsExtendible} x) ϕ
this_2 : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x : Algebra.{u_2, u_3} (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := AlgHom.{u_2, u_2, u_3} (↥ϕ.carrier) (↥(↥ϕ.carrier)⟮α⟯) K
this : FiniteDimensional.{u_2, u_2} ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : (σ : Λ) → Lifts F E K :=
  fun (σ : Λ) ↦ { carrier := restrictScalars F (L' := ↥ϕ.carrier) (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max :
  ∀ ⦃y : Lifts F E K⦄, ϕ < y → ∃ (S : Finset E), ∀ (τ : Lifts F E K) (_ : τ ≥ y), ¬(↑S : Set E) ⊆ (↑τ.carrier : Set E)
S : (σ : Λ) → Finset E
hS : ∀ (σ : Λ) (τ : Lifts F E K) (_ : τ ≥ L σ), ¬(↑(S σ) : Set E) ⊆ (↑τ.carrier : Set E)
θ : Lifts F E K
hθϕ : θ ≥ ϕ
hθ : α ∈ (↑θ.carrier : Set E) ∧ ∀ (i : Λ), (↑(S i) : Set E) ⊆ (↑θ.carrier : Set E)
rw : ϕ.carrier ≤ θ.carrier ∧ α ∈ θ.carrier
⊢ restrictScalars F (L' := ↥ϕ.carrier) (↥ϕ.carrier)⟮α⟯ ≤ θ.carrier

Tactic:
rw [restrictScalars_adjoin_eq_sup, sup_le_iff, adjoin_simple_le_iff]

Premises used: IntermediateField.restrictScalars_adjoin_eq_sup, IntermediateField.adjoin_simple_le_iff, sup_le_iff
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ (σ : Lifts F E K), (↑S : Set E) ⊆ (↑σ.carrier : Set E)
this_1 : IsExtendible.{u_1, u_2, u_3} (F := F) (E := E) (K := K) ⊥
ϕ : Lifts F E K
hϕ : Maximal (fun (x : Lifts F E K) ↦ Membership.mem (γ := Set (Lifts F E K)) {ϕ : Lifts F E K | ϕ.IsExtendible} x) ϕ
this_2 : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x : Algebra.{u_2, u_3} (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := AlgHom.{u_2, u_2, u_3} (↥ϕ.carrier) (↥(↥ϕ.carrier)⟮α⟯) K
this : FiniteDimensional.{u_2, u_2} ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : (σ : Λ) → Lifts F E K :=
  fun (σ : Λ) ↦ { carrier := restrictScalars F (L' := ↥ϕ.carrier) (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max :
  ∀ ⦃y : Lifts F E K⦄, ϕ < y → ∃ (S : Finset E), ∀ (τ : Lifts F E K) (_ : τ ≥ y), ¬(↑S : Set E) ⊆ (↑τ.carrier : Set E)
S : (σ : Λ) → Finset E
hS : ∀ (σ : Λ) (τ : Lifts F E K) (_ : τ ≥ L σ), ¬(↑(S σ) : Set E) ⊆ (↑τ.carrier : Set E)
θ : Lifts F E K
hθϕ : θ ≥ ϕ
hθ : α ∈ (↑θ.carrier : Set E) ∧ ∀ (i : Λ), (↑(S i) : Set E) ⊆ (↑θ.carrier : Set E)
⊢ ϕ.carrier ≤ θ.carrier ∧ α ∈ θ.carrier

Tactic:
⟨hθϕ.1, hθ.1⟩

Premises used: And.left, And.intro
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ (σ : Lifts F E K), (↑S : Set E) ⊆ (↑σ.carrier : Set E)
this_1 : IsExtendible.{u_1, u_2, u_3} (F := F) (E := E) (K := K) ⊥
ϕ : Lifts F E K
hϕ : Maximal (fun (x : Lifts F E K) ↦ Membership.mem (γ := Set (Lifts F E K)) {ϕ : Lifts F E K | ϕ.IsExtendible} x) ϕ
this_2 : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x : Algebra.{u_2, u_3} (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := AlgHom.{u_2, u_2, u_3} (↥ϕ.carrier) (↥(↥ϕ.carrier)⟮α⟯) K
this : FiniteDimensional.{u_2, u_2} ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : (σ : Λ) → Lifts F E K :=
  fun (σ : Λ) ↦ { carrier := restrictScalars F (L' := ↥ϕ.carrier) (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max :
  ∀ ⦃y : Lifts F E K⦄, ϕ < y → ∃ (S : Finset E), ∀ (τ : Lifts F E K) (_ : τ ≥ y), ¬(↑S : Set E) ⊆ (↑τ.carrier : Set E)
S : (σ : Λ) → Finset E
hS : ∀ (σ : Λ) (τ : Lifts F E K) (_ : τ ≥ L σ), ¬(↑(S σ) : Set E) ⊆ (↑τ.carrier : Set E)
θ : Lifts F E K
hθϕ : θ ≥ ϕ
hθ : α ∈ (↑θ.carrier : Set E) ∧ ∀ (i : Λ), (↑(S i) : Set E) ⊆ (↑θ.carrier : Set E)
⊢ ϕ.carrier ≤ θ.carrier ∧ α ∈ θ.carrier

Tactic:
exact ⟨hθϕ.1, hθ.1⟩
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ (σ : Lifts F E K), (↑S : Set E) ⊆ (↑σ.carrier : Set E)
this_1 : IsExtendible.{u_1, u_2, u_3} (F := F) (E := E) (K := K) ⊥
ϕ : Lifts F E K
hϕ : Maximal (fun (x : Lifts F E K) ↦ Membership.mem (γ := Set (Lifts F E K)) {ϕ : Lifts F E K | ϕ.IsExtendible} x) ϕ
this_2 : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x : Algebra.{u_2, u_3} (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := AlgHom.{u_2, u_2, u_3} (↥ϕ.carrier) (↥(↥ϕ.carrier)⟮α⟯) K
this : FiniteDimensional.{u_2, u_2} ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : (σ : Λ) → Lifts F E K :=
  fun (σ : Λ) ↦ { carrier := restrictScalars F (L' := ↥ϕ.carrier) (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max :
  ∀ ⦃y : Lifts F E K⦄, ϕ < y → ∃ (S : Finset E), ∀ (τ : Lifts F E K) (_ : τ ≥ y), ¬(↑S : Set E) ⊆ (↑τ.carrier : Set E)
S : (σ : Λ) → Finset E
hS : ∀ (σ : Λ) (τ : Lifts F E K) (_ : τ ≥ L σ), ¬(↑(S σ) : Set E) ⊆ (↑τ.carrier : Set E)
θ : Lifts F E K
hθϕ : θ ≥ ϕ
hθ : α ∈ (↑θ.carrier : Set E) ∧ ∀ (i : Λ), (↑(S i) : Set E) ⊆ (↑θ.carrier : Set E)
⊢ restrictScalars F (L' := ↥ϕ.carrier) (↥ϕ.carrier)⟮α⟯ ≤ θ.carrier

Tactic:
have : ϕ.carrier⟮α⟯.restrictScalars F ≤ θ.carrier := by
    rw [restrictScalars_adjoin_eq_sup, sup_le_iff, adjoin_simple_le_iff]; exact ⟨hθϕ.1, hθ.1⟩
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ (σ : Lifts F E K), (↑S : Set E) ⊆ (↑σ.carrier : Set E)
this_1 : IsExtendible.{u_1, u_2, u_3} (F := F) (E := E) (K := K) ⊥
ϕ : Lifts F E K
hϕ : Maximal (fun (x : Lifts F E K) ↦ Membership.mem (γ := Set (Lifts F E K)) {ϕ : Lifts F E K | ϕ.IsExtendible} x) ϕ
this_2 : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x : Algebra.{u_2, u_3} (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := AlgHom.{u_2, u_2, u_3} (↥ϕ.carrier) (↥(↥ϕ.carrier)⟮α⟯) K
this_3 : FiniteDimensional.{u_2, u_2} ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : (σ : Λ) → Lifts F E K :=
  fun (σ : Λ) ↦ { carrier := restrictScalars F (L' := ↥ϕ.carrier) (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max :
  ∀ ⦃y : Lifts F E K⦄, ϕ < y → ∃ (S : Finset E), ∀ (τ : Lifts F E K) (_ : τ ≥ y), ¬(↑S : Set E) ⊆ (↑τ.carrier : Set E)
S : (σ : Λ) → Finset E
hS : ∀ (σ : Λ) (τ : Lifts F E K) (_ : τ ≥ L σ), ¬(↑(S σ) : Set E) ⊆ (↑τ.carrier : Set E)
θ : Lifts F E K
hθϕ : θ ≥ ϕ
hθ : α ∈ (↑θ.carrier : Set E) ∧ ∀ (i : Λ), (↑(S i) : Set E) ⊆ (↑θ.carrier : Set E)
this : restrictScalars F (L' := ↥ϕ.carrier) (↥ϕ.carrier)⟮α⟯ ≤ θ.carrier
⊢ False

Tactic:
hS ⟨(θ.emb.comp <| inclusion this).toRingHom, hθϕ.2⟩ θ ⟨this, fun _ ↦ rfl⟩ (hθ.2 _)

Premises used: And.right, AlgHom.toRingHom, IntermediateField.Lifts.emb, Exists.intro, AlgHom.mk, IntermediateField.inclusion, AlgHom.comp, rfl
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ (σ : Lifts F E K), (↑S : Set E) ⊆ (↑σ.carrier : Set E)
this_1 : IsExtendible.{u_1, u_2, u_3} (F := F) (E := E) (K := K) ⊥
ϕ : Lifts F E K
hϕ : Maximal (fun (x : Lifts F E K) ↦ Membership.mem (γ := Set (Lifts F E K)) {ϕ : Lifts F E K | ϕ.IsExtendible} x) ϕ
this_2 : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x : Algebra.{u_2, u_3} (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := AlgHom.{u_2, u_2, u_3} (↥ϕ.carrier) (↥(↥ϕ.carrier)⟮α⟯) K
this_3 : FiniteDimensional.{u_2, u_2} ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : (σ : Λ) → Lifts F E K :=
  fun (σ : Λ) ↦ { carrier := restrictScalars F (L' := ↥ϕ.carrier) (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max :
  ∀ ⦃y : Lifts F E K⦄, ϕ < y → ∃ (S : Finset E), ∀ (τ : Lifts F E K) (_ : τ ≥ y), ¬(↑S : Set E) ⊆ (↑τ.carrier : Set E)
S : (σ : Λ) → Finset E
hS : ∀ (σ : Λ) (τ : Lifts F E K) (_ : τ ≥ L σ), ¬(↑(S σ) : Set E) ⊆ (↑τ.carrier : Set E)
θ : Lifts F E K
hθϕ : θ ≥ ϕ
hθ : α ∈ (↑θ.carrier : Set E) ∧ ∀ (i : Λ), (↑(S i) : Set E) ⊆ (↑θ.carrier : Set E)
this : restrictScalars F (L' := ↥ϕ.carrier) (↥ϕ.carrier)⟮α⟯ ≤ θ.carrier
⊢ False

Tactic:
exact hS ⟨(θ.emb.comp <| inclusion this).toRingHom, hθϕ.2⟩ θ ⟨this, fun _ ↦ rfl⟩ (hθ.2 _)

Premises used: And.right, AlgHom.toRingHom, IntermediateField.Lifts.emb, Exists.intro, AlgHom.mk, IntermediateField.inclusion, AlgHom.comp, rfl
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ (σ : Lifts F E K), (↑S : Set E) ⊆ (↑σ.carrier : Set E)
this_1 : IsExtendible.{u_1, u_2, u_3} (F := F) (E := E) (K := K) ⊥
ϕ : Lifts F E K
hϕ : Maximal (fun (x : Lifts F E K) ↦ Membership.mem (γ := Set (Lifts F E K)) {ϕ : Lifts F E K | ϕ.IsExtendible} x) ϕ
this_2 : ϕ.carrier ≠ ⊤
α : E
hα : α ∉ ϕ.carrier
x : Algebra.{u_2, u_3} (↥ϕ.carrier) K := ϕ.emb.toAlgebra
Λ : Type (max u_2 u_3) := AlgHom.{u_2, u_2, u_3} (↥ϕ.carrier) (↥(↥ϕ.carrier)⟮α⟯) K
this : FiniteDimensional.{u_2, u_2} ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯
L : (σ : Λ) → Lifts F E K :=
  fun (σ : Λ) ↦ { carrier := restrictScalars F (L' := ↥ϕ.carrier) (↥ϕ.carrier)⟮α⟯, emb := AlgHom.restrictScalars F σ }
hL : ∀ (σ : Λ), ϕ < L σ
ϕ_ext : ϕ.IsExtendible
ϕ_max :
  ∀ ⦃y : Lifts F E K⦄, ϕ < y → ∃ (S : Finset E), ∀ (τ : Lifts F E K) (_ : τ ≥ y), ¬(↑S : Set E) ⊆ (↑τ.carrier : Set E)
S : (σ : Λ) → Finset E
hS : ∀ (σ : Λ) (τ : Lifts F E K) (_ : τ ≥ L σ), ¬(↑(S σ) : Set E) ⊆ (↑τ.carrier : Set E)
have have₁ have₂ :
  ∀ (θ : Lifts F E K) (hθϕ : θ ≥ ϕ) (hθ : (↑({α} ∪ Finset.biUnion Finset.univ S) : Set E) ⊆ (↑θ.carrier : Set E)), False
have₃ :
  ∀ (θ : Lifts F E K) (hθϕ : θ ≥ ϕ)
    (hθ : α ∈ (↑θ.carrier : Set E) ∧ ∀ (i : Λ), (↑(S i) : Set E) ⊆ (↑θ.carrier : Set E)), False
have₄ :
  ∀ (θ : Lifts F E K) (hθϕ : θ ≥ ϕ) (hθ : α ∈ (↑θ.carrier : Set E) ∧ ∀ (i : Λ), (↑(S i) : Set E) ⊆ (↑θ.carrier : Set E))
    (this : restrictScalars F (L' := ↥ϕ.carrier) (↥ϕ.carrier)⟮α⟯ ≤ θ.carrier), False
⊢ False

Tactic:
classical
  have ⟨θ, hθϕ, hθ⟩ := ϕ_ext ({α} ∪ Finset.univ.biUnion S)
  simp_rw [Finset.coe_union, Set.union_subset_iff, Finset.coe_singleton, Set.singleton_subset_iff,
    Finset.coe_biUnion, Finset.coe_univ, Set.mem_univ, Set.iUnion_true, Set.iUnion_subset_iff] at hθ
  have : ϕ.carrier⟮α⟯.restrictScalars F ≤ θ.carrier := by
    rw [restrictScalars_adjoin_eq_sup, sup_le_iff, adjoin_simple_le_iff]; exact ⟨hθϕ.1, hθ.1⟩
  exact hS ⟨(θ.emb.comp <| inclusion this).toRingHom, hθϕ.2⟩ θ ⟨this, fun _ ↦ rfl⟩ (hθ.2 _)

Premises used: Set.singleton_subset_iff, Finset.coe_biUnion, Finset.coe_singleton, Finset.coe_univ, Set.iUnion_subset_iff, Set.union_subset_iff, Set.iUnion_true, Set.mem_univ, Finset.coe_union
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
x : Lifts F E K
s : E
h1 : IsIntegral (↥x.carrier) s
h2 : (Polynomial.map x.emb.toRingHom (minpoly (↥x.carrier) s)).Splits
I2 : degree (R := ↥x.carrier) (minpoly (↥x.carrier) s) ≠ 0
this_1 : Algebra.{u_2, u_3} (↥x.carrier) K := x.emb.toAlgebra
carrier : IntermediateField F E := restrictScalars F (L' := ↥x.carrier) (↥x.carrier)⟮s⟯
this : Algebra ↥x.carrier ↥carrier := Subalgebra.algebra (toSubalgebra (↥x.carrier)⟮s⟯)
rwa rwa₁ rwa₂ rwa₃ : degree (R := ↥x.carrier) (minpoly (↥x.carrier) s) ≠ 0
⊢ (Polynomial.map x.emb.toRingHom (minpoly (↥x.carrier) s)).degree ≠ 0

Tactic:
rwa [degree_map]

Premises used: Polynomial.degree_map
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
x : Lifts F E K
s : E
h1 : IsIntegral (↥x.carrier) s
h2 : (Polynomial.map x.emb.toRingHom (minpoly (↥x.carrier) s)).Splits
I2 : degree (R := ↥x.carrier) (minpoly (↥x.carrier) s) ≠ 0
this_1 : Algebra.{u_2, u_3} (↥x.carrier) K := x.emb.toAlgebra
carrier : IntermediateField F E := restrictScalars F (L' := ↥x.carrier) (↥x.carrier)⟮s⟯
this : Algebra ↥x.carrier ↥carrier := Subalgebra.algebra (toSubalgebra (↥x.carrier)⟮s⟯)
rw :
  Eq.{u_3 + 1} (α := K) ((aeval (rootOfSplits h2 ⋯) : (a : (↥x.carrier)[X]) → K) (minpoly (↥x.carrier) s) : K) (0 : K)
⊢ rootOfSplits h2 ⋯ ∈ aroots (T := ↥x.carrier) (minpoly (↥x.carrier) s) K

Tactic:
rw [mem_aroots, and_iff_right (minpoly.ne_zero h1)]

Premises used: and_iff_right, Polynomial.mem_aroots, minpoly.ne_zero
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
x : Lifts F E K
s : E
h1 : IsIntegral (↥x.carrier) s
h2 : (Polynomial.map x.emb.toRingHom (minpoly (↥x.carrier) s)).Splits
I2 : degree (R := ↥x.carrier) (minpoly (↥x.carrier) s) ≠ 0
this_1 : Algebra.{u_2, u_3} (↥x.carrier) K := x.emb.toAlgebra
carrier : IntermediateField F E := restrictScalars F (L' := ↥x.carrier) (↥x.carrier)⟮s⟯
this : Algebra ↥x.carrier ↥carrier := Subalgebra.algebra (toSubalgebra (↥x.carrier)⟮s⟯)
⊢ Eq.{u_3 + 1} (α := K) ((aeval (rootOfSplits h2 ⋯) : (a : (↥x.carrier)[X]) → K) (minpoly (↥x.carrier) s) : K) (0 : K)

Tactic:
(eval_map _ _).symm.trans (eval_rootOfSplits _ _)

Premises used: Polynomial.eval_map, Polynomial.eval_rootOfSplits, Eq.symm, Eq.trans
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
x : Lifts F E K
s : E
h1 : IsIntegral (↥x.carrier) s
h2 : (Polynomial.map x.emb.toRingHom (minpoly (↥x.carrier) s)).Splits
I2 : degree (R := ↥x.carrier) (minpoly (↥x.carrier) s) ≠ 0
this_1 : Algebra.{u_2, u_3} (↥x.carrier) K := x.emb.toAlgebra
carrier : IntermediateField F E := restrictScalars F (L' := ↥x.carrier) (↥x.carrier)⟮s⟯
this : Algebra ↥x.carrier ↥carrier := Subalgebra.algebra (toSubalgebra (↥x.carrier)⟮s⟯)
⊢ Eq.{u_3 + 1} (α := K) ((aeval (rootOfSplits h2 ⋯) : (a : (↥x.carrier)[X]) → K) (minpoly (↥x.carrier) s) : K) (0 : K)

Tactic:
exact (eval_map _ _).symm.trans (eval_rootOfSplits _ _)

Premises used: Polynomial.eval_map, Polynomial.eval_rootOfSplits, Eq.symm, Eq.trans
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
x : Lifts F E K
s : E
h1 : IsIntegral F s
h2 : Splits (Polynomial.map (algebraMap F K) (minpoly F s))
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (h2 :
      Splits
        (Polynomial.map
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑x.emb : ↥x.carrier →+* K) (algebraMap F ↥x.carrier))
          (minpoly F s))),
    (Polynomial.map (x.emb.comp (algebraMap F ↥x.carrier)) (minpoly F s)).Splits
⊢ (Polynomial.map (x.emb.comp (algebraMap F ↥x.carrier)) (minpoly F s)).Splits

Tactic:
rwa [← x.emb.comp_algebraMap] at h2

Premises used: AlgHom.comp_algebraMap, IntermediateField.Lifts.emb
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
obtain :
  ∀ (φ : Lifts F E K) (hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ) (hφ : IsMax φ),
    ∃ (φ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin (↥L) S)) K), AlgHom.restrictDomain (↥L) φ = f
⊢ ∃ (φ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin (↥L) S)) K), AlgHom.restrictDomain (↥L) φ = f

Tactic:
obtain ⟨φ, hfφ, hφ⟩ := zorn_le_nonempty_Ici₀ _
    (fun c _ hc _ _ ↦ Lifts.exists_upper_bound c hc) ⟨L, f⟩ le_rfl

Premises used: le_rfl, zorn_le_nonempty_Ici₀, IntermediateField.Lifts.exists_upper_bound, IntermediateField.Lifts.mk
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
⊢ ∃ (φ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin (↥L) S)) K), AlgHom.restrictDomain (↥L) φ = f

Tactic:
⟨φ.emb.comp (inclusion <| (le_extendScalars_iff hfφ.1 <| adjoin L S).mp <|
    adjoin_le_iff.mpr fun s h ↦ ?_), AlgHom.ext hfφ.2⟩

Premises used: Iff.mpr, IntermediateField.adjoin_le_iff, Membership.mem, Subtype, AlgHom.ext, IntermediateField.le_extendScalars_iff, IntermediateField.Lifts.emb, IntermediateField.adjoin, Exists.intro, Iff.mp, IntermediateField.inclusion, AlgHom.comp
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
refine : ∀ (s : E) (h : s ∈ S), s ∈ (↑(extendScalars (E := φ.carrier) ⋯) : Set E)
⊢ ∃ (φ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin (↥L) S)) K), AlgHom.restrictDomain (↥L) φ = f

Tactic:
refine ⟨φ.emb.comp (inclusion <| (le_extendScalars_iff hfφ.1 <| adjoin L S).mp <|
    adjoin_le_iff.mpr fun s h ↦ ?_), AlgHom.ext hfφ.2⟩
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this_1 : Algebra ↥{ carrier := L, emb := f : Lifts F E K }.carrier ↥φ.carrier :=
  RingHom.toAlgebra (AlgHom.toRingHom (inclusion ⋯))
this : SMul ↥L ↥φ.carrier :=
  @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring { carrier := L, emb := f : Lifts F E K }.carrier)
    CommSemiring.toSemiring _
⊢ IsScalarTower (↥L) (↥φ.carrier) E

Tactic:
have : IsScalarTower L φ.carrier E := ⟨fun x y ↦ smul_assoc x (y : E)⟩
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this_1 : Algebra ↥{ carrier := L, emb := f : Lifts F E K }.carrier ↥φ.carrier :=
  RingHom.toAlgebra (AlgHom.toRingHom (inclusion ⋯))
this_2 : SMul ↥L ↥φ.carrier :=
  @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring { carrier := L, emb := f : Lifts F E K }.carrier)
    CommSemiring.toSemiring _
this : IsScalarTower (↥L) (↥φ.carrier) E
refine_2 : ∀ (this : ∃ (y : Lifts F E K), φ ≤ y ∧ s ∈ y.carrier), s ∈ (↑(extendScalars (E := φ.carrier) ⋯) : Set E)
refine_1 : (Polynomial.map (R := ↥L) (φ.emb.comp (algebraMap ↥L ↥φ.carrier)) (minpoly (↥L) s)).Splits
⊢ s ∈ (↑(extendScalars (E := φ.carrier) ⋯) : Set E)

Tactic:
have := φ.exists_lift_of_splits' (hK s h).1.tower_top ((hK s h).1.minpoly_splits_tower_top' ?_)
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this_1 : Algebra ↥{ carrier := L, emb := f : Lifts F E K }.carrier ↥φ.carrier :=
  RingHom.toAlgebra (AlgHom.toRingHom (inclusion ⋯))
this_2 : SMul ↥L ↥φ.carrier :=
  @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring { carrier := L, emb := f : Lifts F E K }.carrier)
    CommSemiring.toSemiring _
this_3 : IsScalarTower (↥L) (↥φ.carrier) E
this : ∃ (y : Lifts F E K), φ ≤ y ∧ s ∈ y.carrier
refine_2 : ∀ (y : Lifts F E K) (h1 : φ ≤ y) (h2 : s ∈ y.carrier), s ∈ (↑(extendScalars (E := φ.carrier) ⋯) : Set E)
⊢ s ∈ (↑(extendScalars (E := φ.carrier) ⋯) : Set E)

Tactic:
obtain ⟨y, h1, h2⟩ := this
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L : IntermediateField F E
f : AlgHom.{u_1, u_2, u_3} F (↥L) K
hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ (Polynomial.map f.toRingHom (minpoly (↥L) s)).Splits
φ : Lifts F E K
hfφ : { carrier := L, emb := f : Lifts F E K } ≤ φ
hφ : IsMax φ
s : E
h : s ∈ S
this_1 : Algebra ↥{ carrier := L, emb := f : Lifts F E K }.carrier ↥φ.carrier :=
  RingHom.toAlgebra (AlgHom.toRingHom (inclusion ⋯))
this_2 : SMul ↥L ↥φ.carrier :=
  @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring { carrier := L, emb := f : Lifts F E K }.carrier)
    CommSemiring.toSemiring _
this : IsScalarTower (↥L) (↥φ.carrier) E
y : Lifts F E K
h1 : φ ≤ y
h2 : s ∈ y.carrier
⊢ s ∈ (↑(extendScalars (E := φ.carrier) ⋯) : Set E)

Tactic:
(hφ h1).1 h2

Premises used: Set.Mem