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
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
ω : Ω
θ : (π : (↑c : Type (max u_2 u_3))) → Lifts F E K
ge : ∀ (π : (↑c : Type (max u_2 u_3))), θ π ≥ (↑π : Lifts F E K)
hθ : ∀ (π : (↑c : Type (max u_2 u_3))), { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ π
eq : ∀ (π : (↑c : Type (max u_2 u_3))), (θ π).carrier = adjoin F ((↑(↑π : Lifts F E K).carrier : Set E) ∪ (↑S : Set E))
π₁ π₂ : (↑c : Type (max u_2 u_3))
h : π₁ ≤ π₂
x : E
hx : x ∈ (↑S : Set E)
refine_2 :
  Eq.{u_3 + 1} (α := K)
    (((θ π₂).emb : (a : ↥(θ π₂).carrier) → K)
        ((inclusion ⋯ : (a : ↥{ carrier := adjoin F (↑S : Set E), emb := ω }.carrier) → ↥(θ π₂).carrier)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K }.carrier) x
              ⋯) :
          ↥(θ π₂).carrier) :
      K)
    (({ carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K }.emb :
          (a : ↥{ carrier := adjoin F (↑S : Set E), emb := ω }.carrier) → K)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K }.carrier) x ⋯) :
      K)
refine_2₁ refine_2₂ :
  Eq.{u_3 + 1} (α := K)
    (({ carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K }.emb :
          (a : ↥{ carrier := adjoin F (↑S : Set E), emb := ω }.carrier) → K)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K }.carrier) x ⋯) :
      K)
    (({ carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K }.emb :
          (a : ↥{ carrier := adjoin F (↑S : Set E), emb := ω }.carrier) → K)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K }.carrier) x ⋯) :
      K)
⊢ Eq.{u_3 + 1} (α := K)
    (((θ π₂).emb : (a : ↥(θ π₂).carrier) → K)
        ((inclusion ⋯ : (a : ↥{ carrier := adjoin F (↑S : Set E), emb := ω }.carrier) → ↥(θ π₂).carrier)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K }.carrier) x
              ⋯) :
          ↥(θ π₂).carrier) :
      K)
    (((θ π₁).emb : (a : ↥(θ π₁).carrier) → K)
        ((inclusion ⋯ : (a : ↥{ carrier := adjoin F (↑S : Set E), emb := ω }.carrier) → ↥(θ π₁).carrier)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K }.carrier) x
              ⋯) :
          ↥(θ π₁).carrier) :
      K)

Tactic:
rw [(hθ π₁).2, (hθ π₂).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
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
ω : Ω
θ : (π : (↑c : Type (max u_2 u_3))) → Lifts F E K
ge : ∀ (π : (↑c : Type (max u_2 u_3))), θ π ≥ (↑π : Lifts F E K)
hθ : ∀ (π : (↑c : Type (max u_2 u_3))), { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ π
eq : ∀ (π : (↑c : Type (max u_2 u_3))), (θ π).carrier = (↑π : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
⊢ IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (Set.range θ)

Tactic:
have : IsChain (· ≤ ·) (Set.range θ) := by
    simp_rw [← restrictScalars_adjoin_eq_sup, restrictScalars_adjoin] at eq
    rintro _ ⟨π₁, rfl⟩ _ ⟨π₂, rfl⟩ -
    wlog h : π₁ ≤ π₂ generalizing π₁ π₂
    · exact (this _ _ <| (hc.total π₁.2 π₂.2).resolve_left h).symm
    refine .inl (le_iff.mpr ⟨?_, algHom_ext_of_eq_adjoin _ (eq _) ?_⟩)
    · rw [eq, eq]; exact adjoin.mono _ _ _ (Set.union_subset_union_left _ h.1)
    rintro x (hx | hx)
    · change (θ π₂).emb (inclusion (ge π₂).1 <| inclusion h.1 ⟨x, hx⟩) =
        (θ π₁).emb (inclusion (ge π₁).1 ⟨x, hx⟩)
      rw [(ge π₁).2, (ge π₂).2, h.2]
    · change (θ π₂).emb (inclusion (hθ π₂).1 ⟨x, subset_adjoin _ _ hx⟩) =
        (θ π₁).emb (inclusion (hθ π₁).1 ⟨x, subset_adjoin _ _ hx⟩)
      rw [(hθ π₁).2, (hθ π₂).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
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
ω : Ω
θ : (π : (↑c : Type (max u_2 u_3))) → Lifts F E K
ge : ∀ (π : (↑c : Type (max u_2 u_3))), θ π ≥ (↑π : Lifts F E K)
hθ : ∀ (π : (↑c : Type (max u_2 u_3))), { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ π
eq : ∀ (π : (↑c : Type (max u_2 u_3))), (θ π).carrier = (↑π : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
this : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (Set.range θ)
⊢ ∃ τ ≥ union c hc, (↑S : Set E) ⊆ (↑τ.carrier : Set E)

Tactic:
⟨union _ this, le_of_carrier_le_iSup (fun π ↦ le_union c hc π.2)
    (fun π ↦ (ge π).trans <| le_union _ _ ⟨_, rfl⟩) (carrier_union _ _).le, ?_⟩

Premises used: IntermediateField.Lifts.union, IntermediateField.Lifts.le_union, Eq.le, And.intro, Exists.intro, Set.range, LE.le.trans, IntermediateField.Lifts.carrier_union, IntermediateField.Lifts.le_of_carrier_le_iSup, 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
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
ω : Ω
θ : (π : (↑c : Type (max u_2 u_3))) → Lifts F E K
ge : ∀ (π : (↑c : Type (max u_2 u_3))), θ π ≥ (↑π : Lifts F E K)
hθ : ∀ (π : (↑c : Type (max u_2 u_3))), { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ π
eq : ∀ (π : (↑c : Type (max u_2 u_3))), (θ π).carrier = (↑π : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
this : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (Set.range θ)
refine : (↑S : Set E) ⊆ (↑(union (Set.range θ) this).carrier : Set E)
⊢ ∃ τ ≥ union c hc, (↑S : Set E) ⊆ (↑τ.carrier : Set E)

Tactic:
refine ⟨union _ this, le_of_carrier_le_iSup (fun π ↦ le_union c hc π.2)
    (fun π ↦ (ge π).trans <| le_union _ _ ⟨_, rfl⟩) (carrier_union _ _).le, ?_⟩
-- 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
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
ω : Ω
θ : (π : (↑c : Type (max u_2 u_3))) → Lifts F E K
ge : ∀ (π : (↑c : Type (max u_2 u_3))), θ π ≥ (↑π : Lifts F E K)
hθ : ∀ (π : (↑c : Type (max u_2 u_3))), { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ π
eq : ∀ (π : (↑c : Type (max u_2 u_3))), (θ π).carrier = (↑π : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
this : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (Set.range θ)
simp_rw :
  (↑S : Set E) ⊆ (↑(⨆ (i : (↑c : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)) : Set E)
⊢ (↑S : Set E) ⊆ (↑(union (Set.range θ) this).carrier : Set E)

Tactic:
simp_rw [carrier_union, iSup_range', eq]

Premises used: iSup_range', IntermediateField.Lifts.carrier_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
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
ω : Ω
θ : (π : (↑c : Type (max u_2 u_3))) → Lifts F E K
ge : ∀ (π : (↑c : Type (max u_2 u_3))), θ π ≥ (↑π : Lifts F E K)
hθ : ∀ (π : (↑c : Type (max u_2 u_3))), { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ π
eq : ∀ (π : (↑c : Type (max u_2 u_3))), (θ π).carrier = (↑π : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
this : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (Set.range θ)
⊢ (↑S : Set E) ⊆ (↑(⨆ (i : (↑c : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)) : Set E)

Tactic:
(subset_adjoin _ _).trans (SetLike.coe_subset_coe.mpr <|
    le_sup_right.trans <| le_iSup_of_le (Classical.arbitrary _) le_rfl)

Premises used: Iff.mpr, le_rfl, HasSubset.Subset.trans, le_sup_right, IntermediateField.subset_adjoin, SetLike.coe_subset_coe, le_iSup_of_le, Classical.arbitrary, LE.le.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
c : Set (Lifts F E K)
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
alg : Algebra.IsAlgebraic F E
inst_5 : Nonempty (↑c : Type (max u_2 u_3))
hext : ∀ σ ∈ c, σ.IsExtendible
S : Finset E
Ω : Type (max u_2 u_3) := AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K
ω : Ω
θ : (π : (↑c : Type (max u_2 u_3))) → Lifts F E K
ge : ∀ (π : (↑c : Type (max u_2 u_3))), θ π ≥ (↑π : Lifts F E K)
hθ : ∀ (π : (↑c : Type (max u_2 u_3))), { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ π
eq : ∀ (π : (↑c : Type (max u_2 u_3))), (θ π).carrier = (↑π : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
this : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (Set.range θ)
⊢ (↑S : Set E) ⊆ (↑(⨆ (i : (↑c : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)) : Set E)

Tactic:
exact (subset_adjoin _ _).trans (SetLike.coe_subset_coe.mpr <|
    le_sup_right.trans <| le_iSup_of_le (Classical.arbitrary _) le_rfl)

Premises used: Iff.mpr, HasSubset.Subset.trans, le_sup_right, IntermediateField.subset_adjoin, SetLike.coe_subset_coe, le_iSup_of_le, Classical.arbitrary, LE.le.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
alg : Algebra.IsAlgebraic F E
h : ∀ (S : Finset E), ∃ (σ : Lifts F E K), (↑S : Set E) ⊆ (↑σ.carrier : Set E)
⊢ IsExtendible.{u_1, u_2, u_3} (F := F) (E := E) (K := K) ⊥

Tactic:
have : (⊥ : Lifts F E K).IsExtendible := fun S ↦ have ⟨σ, hσ⟩ := h S; ⟨σ, bot_le, hσ⟩
-- 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 : IsExtendible.{u_1, u_2, u_3} (F := F) (E := E) (K := K) ⊥
have :
  ∀ (ϕ : 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) ϕ),
    Nonempty (E →ₐ[F] K)
⊢ Nonempty (E →ₐ[F] K)

Tactic:
have ⟨ϕ, hϕ⟩ := zorn_le₀ {ϕ : Lifts F E K | ϕ.IsExtendible}
    fun c hext hc ↦ (isEmpty_or_nonempty c).elim
      (fun _ ↦ ⟨⊥, this, fun ϕ hϕ ↦ isEmptyElim (⟨ϕ, hϕ⟩ : c)⟩)
      fun _ ↦ ⟨_, union_isExtendible c hc hext, le_union c hc⟩
-- 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 : 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) ϕ
suffices : ϕ.carrier = ⊤
⊢ Nonempty (E →ₐ[F] K)

Tactic:
suffices ϕ.carrier = ⊤ from ⟨ϕ.emb.comp <| ((equivOfEq this).trans topEquiv).symm⟩
-- 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 : 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) ϕ
by_contra! : ∀ (this : ϕ.carrier ≠ ⊤), False
⊢ ϕ.carrier = ⊤

Tactic:
by_contra!
-- 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 : ϕ.carrier ≠ ⊤
obtain : ∀ (α : E) (hα : α ∉ ϕ.carrier), False
⊢ False

Tactic:
obtain ⟨α, -, hα⟩ := SetLike.exists_of_lt this.lt_top

Premises used: SetLike.exists_of_lt, Ne.lt_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
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 : ϕ.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
⊢ FiniteDimensional.{u_2, u_2} ↥ϕ.carrier ↥(↥ϕ.carrier)⟮α⟯

Tactic:
have := finiteDimensional_adjoin (S := {α}) fun _ _ ↦ ((alg.tower_top ϕ.carrier).isIntegral).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 σ }
σ : Λ
⊢ ϕ.carrier < (L σ).carrier

Tactic:
simpa only [L, restrictScalars_adjoin_eq_sup, left_lt_sup, adjoin_simple_le_iff]

Premises used: IntermediateField.restrictScalars_adjoin_eq_sup, left_lt_sup, IntermediateField.adjoin_simple_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 σ }
⊢ ∀ (σ : Λ), ϕ < L σ

Tactic:
have hL (σ : Λ) : ϕ < L σ := lt_iff.mpr
    ⟨by simpa only [L, restrictScalars_adjoin_eq_sup, left_lt_sup, adjoin_simple_le_iff],
      AlgHom.coe_ringHom_injective σ.comp_algebraMap⟩
-- 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 σ
⊢ ϕ.IsExtendible

Tactic:
have ⟨(ϕ_ext : ϕ.IsExtendible), ϕ_max⟩ := maximal_iff_forall_gt.mp hϕ
-- 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
⊢ ∀ ⦃y : Lifts F E K⦄, ϕ < y → y ∉ {ϕ : Lifts F E K | ϕ.IsExtendible}

Tactic:
have ⟨(ϕ_ext : ϕ.IsExtendible), ϕ_max⟩ := maximal_iff_forall_gt.mp hϕ
-- 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 → y ∉ {ϕ : Lifts F E K | ϕ.IsExtendible}
⊢ ∀ ⦃y : Lifts F E K⦄, ϕ < y → ¬∀ (S : Finset E), ∃ τ ≥ y, (↑S : Set E) ⊆ (↑τ.carrier : Set E)

Tactic:
simp_rw [Set.mem_setOf, IsExtendible] at ϕ_max

Premises used: IntermediateField.Lifts.IsExtendible, Set.mem_setOf
-- 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), ∃ τ ≥ y, (↑S : Set E) ⊆ (↑τ.carrier : Set E)
⊢ ∀ ⦃y : Lifts F E K⦄, ϕ < y → ∃ (S : Finset E), ∀ (τ : Lifts F E K) (_ : τ ≥ y), ¬(↑S : Set E) ⊆ (↑τ.carrier : Set E)

Tactic:
push Not at ϕ_max

Premises used: Not
-- 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)
choose :
  ∀ (S : (σ : Λ) → Finset E) (hS : ∀ (σ : Λ) (τ : Lifts F E K) (_ : τ ≥ L σ), ¬(↑(S σ) : Set E) ⊆ (↑τ.carrier : Set E)),
    False
⊢ False

Tactic:
choose S hS using fun σ : Λ ↦ ϕ_max (hL σ)
-- 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 :
  ∀ (θ : Lifts F E K) (hθϕ : θ ≥ ϕ) (hθ : (↑({α} ∪ Finset.biUnion Finset.univ S) : Set E) ⊆ (↑θ.carrier : Set E)), False
⊢ False

Tactic:
have ⟨θ, hθϕ, hθ⟩ := ϕ_ext ({α} ∪ Finset.univ.biUnion S)