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
S : Set E
L₁ L₂ : Lifts F E K
c : Set (Lifts F E K)
hc_1 : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
t : (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) → IntermediateField F E :=
  fun (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑i : Lifts F E K).carrier
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (insert ⊥ c)
dir : Directed (fun (x1 x2 : IntermediateField F E) ↦ x1 ≤ x2) t
i j : (↑(insert ⊥ c) : Type (max u_2 u_3))
h :
  LE.le.{u_2} (α := Subalgebra F E) ((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) i)
    ((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) j)
x : ↥(↑i : Lifts F E K).carrier
hji : (↑j : Lifts F E K) ≤ (↑i : Lifts F E K)
rw :
  Eq.{u_3 + 1} (α := K)
    (((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).emb) i :
          (a : ↥(↑i : Lifts F E K).carrier) → K)
        x :
      K)
    (((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).emb) j :
          (a : ↥((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) j)) → K)
        ((inclusion h :
              (a : ↥(↑i : Lifts F E K).carrier) →
                ↥((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) j))
            x :
          ↥((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) j)) :
      K)
⊢ Eq.{u_3 + 1} (α := K)
    (((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).emb) i :
          (a : ↥(↑i : Lifts F E K).carrier) → K)
        x :
      K)
    ((AlgHom.comp ((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).emb) j)
            (Subalgebra.inclusion h) :
          (a : ↥(↑i : Lifts F E K).carrier) → K)
        x :
      K)

Tactic:
rw [AlgHom.comp_apply, ← inclusion]

Premises used: AlgHom.comp_apply, IntermediateField.inclusion
-- 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₁ L₂ : Lifts F E K
c : Set (Lifts F E K)
hc_1 : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
t : (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) → IntermediateField F E :=
  fun (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑i : Lifts F E K).carrier
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (insert ⊥ c)
dir : Directed (fun (x1 x2 : IntermediateField F E) ↦ x1 ≤ x2) t
i j : (↑(insert ⊥ c) : Type (max u_2 u_3))
h :
  LE.le.{u_2} (α := Subalgebra F E) ((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) i)
    ((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) j)
x : ↥(↑i : Lifts F E K).carrier
hji : (↑j : Lifts F E K) ≤ (↑i : Lifts F E K)
dsimp :
  Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
    (((↑j : Lifts F E K).emb : (a : ↥(t j)) → K)
        ((inclusion h : (a : ↥(↑i : Lifts F E K).carrier) → ↥(t j)) x : ↥(t j)) :
      K)
⊢ Eq.{u_3 + 1} (α := K)
    (((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).emb) i :
          (a : ↥(↑i : Lifts F E K).carrier) → K)
        x :
      K)
    (((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).emb) j :
          (a : ↥((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) j)) → K)
        ((inclusion h :
              (a : ↥(↑i : Lifts F E K).carrier) →
                ↥((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) j))
            x :
          ↥((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) j)) :
      K)

Tactic:
dsimp only [coe_type_toSubalgebra]

Premises used: IntermediateField.coe_type_toSubalgebra
-- 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₁ L₂ : Lifts F E K
c : Set (Lifts F E K)
hc_1 : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) c
t : (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) → IntermediateField F E :=
  fun (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑i : Lifts F E K).carrier
hc : IsChain (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (insert ⊥ c)
dir : Directed (fun (x1 x2 : IntermediateField F E) ↦ x1 ≤ x2) t
i j : (↑(insert ⊥ c) : Type (max u_2 u_3))
h :
  LE.le.{u_2} (α := Subalgebra F E) ((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) i)
    ((fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (t x).toSubalgebra) j)
x : ↥(↑i : Lifts F E K).carrier
hji : (↑j : Lifts F E K) ≤ (↑i : Lifts F E K)
rw :
  Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
    (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K)
        ((inclusion ⋯ : (a : ↥(↑j : Lifts F E K).carrier) → ↥(↑i : Lifts F E K).carrier)
            ((inclusion h : (a : ↥(t i)) → ↥(t j)) x) :
          ↥(↑i : Lifts F E K).carrier) :
      K)
rw₁ :
  Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
    (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K)
        ((inclusion ⋯ : (a : ↥(t i)) → ↥(↑i : Lifts F E K).carrier) x : ↥(↑i : Lifts F E K).carrier) :
      K)
rw₂ :
  Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
    (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K)
        ((AlgHom.id F ↥(t i) : (a : ↥(t i)) → ↥(↑i : Lifts F E K).carrier) x : ↥(↑i : Lifts F E K).carrier) :
      K)
rw₃ rw₄ :
  Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
    (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
⊢ Eq.{u_3 + 1} (α := K) (((↑i : Lifts F E K).emb : (a : ↥(↑i : Lifts F E K).carrier) → K) x : K)
    (((↑j : Lifts F E K).emb : (a : ↥(t j)) → K)
        ((inclusion h : (a : ↥(↑i : Lifts F E K).carrier) → ↥(t j)) x : ↥(t j)) :
      K)

Tactic:
rw [← hji.snd (inclusion h x), inclusion_inclusion, inclusion_self, AlgHom.id_apply x]

Premises used: Exists.snd, IntermediateField.inclusion_self, IntermediateField.inclusion_inclusion, IntermediateField.inclusion, DFunLike.coe, AlgHom.id_apply
-- 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
σ : Lifts F E K
hσ_1 : σ ∈ c
hσ : σ ∈ insert ⊥ c
t : (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) → IntermediateField F E :=
  fun (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑i : Lifts F E K).carrier
x : ↥σ.carrier
dsimp :
  Eq.{u_3 + 1} (α := K)
    ((Subalgebra.iSupLift (fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).carrier.toSubalgebra) ⋯
            (fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).emb) ⋯
            (⨆ (x : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑x : Lifts F E K).carrier.toSubalgebra) ⋯ :
          (a : ↥(⨆ (x : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑x : Lifts F E K).carrier.toSubalgebra)) → K)
        (((↑(Subalgebra.equivOfEq
                    (toSubalgebra (⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier))
                    (⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier.toSubalgebra) ⋯) :
                ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier).toSubalgebra →ₐ[F]
                  ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier.toSubalgebra)) :
              (a : ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier)) →
                ↥(⨆ (x : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑x : Lifts F E K).carrier.toSubalgebra))
            (((inclusion ⋯ :
                  ↥σ.carrier →ₐ[F] ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier)) :
                (a : ↥σ.carrier) → ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier))
              x) :
          ↥(⨆ (x : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑x : Lifts F E K).carrier.toSubalgebra)) :
      K)
    ((σ.emb : (a : ↥σ.carrier) → K) x : K)
⊢ Eq.{u_3 + 1} (α := K)
    (((union c hc).emb : (a : ↥(union c hc).carrier) → K)
        (((inclusion ⋯ : ↥σ.carrier →ₐ[F] ↥(union c hc).carrier) : (a : ↥σ.carrier) → ↥(union c hc).carrier) x :
          ↥(union c hc).carrier) :
      K)
    ((σ.emb : (a : ↥σ.carrier) → K) x : K)

Tactic:
dsimp only [union, AlgHom.comp_apply]

Premises used: IntermediateField.Lifts.union, AlgHom.comp_apply
-- 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
σ : Lifts F E K
hσ_1 : σ ∈ c
hσ : σ ∈ insert ⊥ c
t : (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) → IntermediateField F E :=
  fun (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑i : Lifts F E K).carrier
x : ↥σ.carrier
⊢ Eq.{u_3 + 1} (α := K)
    ((Subalgebra.iSupLift (fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).carrier.toSubalgebra) ⋯
            (fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).emb) ⋯
            (⨆ (x : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑x : Lifts F E K).carrier.toSubalgebra) ⋯ :
          (a : ↥(⨆ (x : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑x : Lifts F E K).carrier.toSubalgebra)) → K)
        (((↑(Subalgebra.equivOfEq
                    (toSubalgebra (⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier))
                    (⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier.toSubalgebra) ⋯) :
                ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier).toSubalgebra →ₐ[F]
                  ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier.toSubalgebra)) :
              (a : ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier)) →
                ↥(⨆ (x : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑x : Lifts F E K).carrier.toSubalgebra))
            (((inclusion ⋯ :
                  ↥σ.carrier →ₐ[F] ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier)) :
                (a : ↥σ.carrier) → ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier))
              x) :
          ↥(⨆ (x : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑x : Lifts F E K).carrier.toSubalgebra)) :
      K)
    ((σ.emb : (a : ↥σ.carrier) → K) x : K)

Tactic:
Subalgebra.iSupLift_inclusion (K := (toSubalgebra <| t ·))
      (i := ⟨σ, hσ⟩) x (le_iSup (toSubalgebra <| t ·) ⟨σ, hσ⟩)

Premises used: iInf, Set.Mem, Set.iInter, setOf, le_iSup, Subtype.mk, Subalgebra.iSupLift_inclusion, IntermediateField.toSubalgebra
-- 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
σ : Lifts F E K
hσ_1 : σ ∈ c
hσ : σ ∈ insert ⊥ c
t : (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) → IntermediateField F E :=
  fun (i : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑i : Lifts F E K).carrier
x : ↥σ.carrier
⊢ Eq.{u_3 + 1} (α := K)
    ((Subalgebra.iSupLift (fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).carrier.toSubalgebra) ⋯
            (fun (x : (↑(insert ⊥ c) : Type (max u_2 u_3))) ↦ (↑x : Lifts F E K).emb) ⋯
            (⨆ (x : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑x : Lifts F E K).carrier.toSubalgebra) ⋯ :
          (a : ↥(⨆ (x : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑x : Lifts F E K).carrier.toSubalgebra)) → K)
        (((↑(Subalgebra.equivOfEq
                    (toSubalgebra (⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier))
                    (⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier.toSubalgebra) ⋯) :
                ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier).toSubalgebra →ₐ[F]
                  ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier.toSubalgebra)) :
              (a : ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier)) →
                ↥(⨆ (x : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑x : Lifts F E K).carrier.toSubalgebra))
            (((inclusion ⋯ :
                  ↥σ.carrier →ₐ[F] ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier)) :
                (a : ↥σ.carrier) → ↥(⨆ (i : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier))
              x) :
          ↥(⨆ (x : (↑(insert ⊥ c) : Type (max u_2 u_3))), (↑x : Lifts F E K).carrier.toSubalgebra)) :
      K)
    ((σ.emb : (a : ↥σ.carrier) → K) x : K)

Tactic:
exact Subalgebra.iSupLift_inclusion (K := (toSubalgebra <| t ·))
      (i := ⟨σ, hσ⟩) x (le_iSup (toSubalgebra <| t ·) ⟨σ, hσ⟩)

Premises used: le_iSup, Subtype.mk, Subalgebra.iSupLift_inclusion, IntermediateField.toSubalgebra
-- 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
⊢ (↑(Subtype.mk (p := fun (x : Lifts F E K) ↦ x ∈ insert ⊥ c) ⊥ ⋯) : Lifts F E K).carrier ≤
    ⨆ (i : (↑c : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier

Tactic:
bot_le

Premises used: Set.Mem, bot_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
i : Lifts F E K
hi : i ∈ c
⊢ (↑(Subtype.mk (p := fun (x : Lifts F E K) ↦ x ∈ insert ⊥ c) i ⋯) : Lifts F E K).carrier ≤
    ⨆ (i : (↑c : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier

Tactic:
le_iSup_of_le ⟨i, hi⟩ le_rfl

Premises used: le_rfl, Set.Mem, Subtype.mk, le_iSup_of_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
⊢ (↑(Subtype.mk (p := fun (x : Lifts F E K) ↦ x ∈ insert ⊥ c) ⊥ ⋯) : Lifts F E K).carrier ≤
    ⨆ (i : (↑c : Type (max u_2 u_3))), (↑i : Lifts F E K).carrier

Tactic:
exacts [bot_le, le_iSup_of_le ⟨i, hi⟩ le_rfl]

Premises used: le_rfl, le_iSup_of_le, bot_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
⊢ ∃ (ub : Lifts F E K), ∀ a ∈ c, a ≤ ub

Tactic:
⟨_, le_union c hc⟩

Premises used: IntermediateField.Lifts.le_union, Exists.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
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
by_contra! :
  ∀
    (this :
      ∀ (ω : Ω),
        ∃ (π : (↑c : Type (max u_2 u_3))),
          ∀ (θ : Lifts F E K) (_ : θ ≥ (↑π : Lifts F E K))
            (_ : { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ),
            θ.carrier ≠ (↑π : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)),
    False
⊢ ∃ (ω : Ω),
    ∀ (π : (↑c : Type (max u_2 u_3))),
      ∃ θ ≥ (↑π : Lifts F E K),
        { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ ∧
          θ.carrier = (↑π : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)

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
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
this :
  ∀ (ω : Ω),
    ∃ (π : (↑c : Type (max u_2 u_3))),
      ∀ (θ : Lifts F E K) (_ : θ ≥ (↑π : Lifts F E K))
        (_ : { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ),
        θ.carrier ≠ (↑π : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
choose :
  ∀ (π : (ω : Ω) → (↑c : Type (max u_2 u_3)))
    (hπ :
      ∀ (ω : Ω) (θ : Lifts F E K) (_ : θ ≥ (↑(π ω) : Lifts F E K))
        (_ : { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ),
        θ.carrier ≠ (↑(π ω) : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)),
    False
⊢ False

Tactic:
choose π hπ using 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
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))
hπ :
  ∀ (ω : Ω) (θ : Lifts F E K) (_ : θ ≥ (↑(π ω) : Lifts F E K))
    (_ : { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ),
    θ.carrier ≠ (↑(π ω) : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
⊢ FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))

Tactic:
have := finiteDimensional_adjoin (S := (S : Set E)) fun _ _ ↦ (alg.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
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))
hπ :
  ∀ (ω : Ω) (θ : Lifts F E K) (_ : θ ≥ (↑(π ω) : Lifts F E K))
    (_ : { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ),
    θ.carrier ≠ (↑(π ω) : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
this : FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))
have : ∀ (π₀ : { a : Lifts F E K // a ∈ c }) (hπ₀ : ∀ (i : Ω), (↑(π i) : Lifts F E K) ≤ (↑π₀ : Lifts F E K)), False
⊢ False

Tactic:
have ⟨π₀, hπ₀⟩ := hc.directed.finite_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))
hπ :
  ∀ (ω : Ω) (θ : Lifts F E K) (_ : θ ≥ (↑(π ω) : Lifts F E K))
    (_ : { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ),
    θ.carrier ≠ (↑(π ω) : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
this : FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))
π₀ : { a : Lifts F E K // a ∈ c }
hπ₀ : ∀ (i : Ω), (↑(π i) : Lifts F E K) ≤ (↑π₀ : Lifts F E K)
have : ∀ (θ : Lifts F E K) (hθπ : θ ≥ (↑π₀ : Lifts F E K)) (hθ : (↑S : Set E) ⊆ (↑θ.carrier : Set E)), False
⊢ False

Tactic:
have ⟨θ, hθπ, hθ⟩ := hext _ π₀.2 S
-- 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))
hπ :
  ∀ (ω : Ω) (θ : Lifts F E K) (_ : θ ≥ (↑(π ω) : Lifts F E K))
    (_ : { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ),
    θ.carrier ≠ (↑(π ω) : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
this : FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))
π₀ : { a : Lifts F E K // a ∈ c }
hπ₀ : ∀ (i : Ω), (↑(π i) : Lifts F E K) ≤ (↑π₀ : Lifts F E K)
θ : Lifts F E K
hθπ : θ ≥ (↑π₀ : Lifts F E K)
hθ : (↑S : Set E) ⊆ (↑θ.carrier : Set E)
⊢ adjoin F (↑S : Set E) ≤ θ.carrier

Tactic:
rw [← adjoin_le_iff] at hθ

Premises used: IntermediateField.adjoin_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
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))
hπ :
  ∀ (ω : Ω) (θ : Lifts F E K) (_ : θ ≥ (↑(π ω) : Lifts F E K))
    (_ : { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ),
    θ.carrier ≠ (↑(π ω) : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
this : FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))
π₀ : { a : Lifts F E K // a ∈ c }
hπ₀ : ∀ (i : Ω), (↑(π i) : Lifts F E K) ≤ (↑π₀ : Lifts F E K)
θ : Lifts F E K
hθπ : θ ≥ (↑π₀ : Lifts F E K)
hθ : adjoin F (↑S : Set E) ≤ θ.carrier
θ₀ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K := θ.emb.comp (inclusion hθ)
⊢ (↑(π θ₀) : Lifts F E K) ≤ θ

Tactic:
have := (hπ₀ θ₀).trans 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
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))
hπ :
  ∀ (ω : Ω) (θ : Lifts F E K) (_ : θ ≥ (↑(π ω) : Lifts F E K))
    (_ : { carrier := adjoin F (↑S : Set E), emb := ω : Lifts F E K } ≤ θ),
    θ.carrier ≠ (↑(π ω) : Lifts F E K).carrier ⊔ adjoin F (↑S : Set E)
this_1 : FiniteDimensional.{u_1, u_2} F ↥(adjoin F (↑S : Set E))
π₀ : { a : Lifts F E K // a ∈ c }
hπ₀ : ∀ (i : Ω), (↑(π i) : Lifts F E K) ≤ (↑π₀ : Lifts F E K)
θ : Lifts F E K
hθπ : θ ≥ (↑π₀ : Lifts F E K)
hθ : adjoin F (↑S : Set E) ≤ θ.carrier
θ₀ : AlgHom.{u_1, u_2, u_3} F (↥(adjoin F (↑S : Set E))) K := θ.emb.comp (inclusion hθ)
this : (↑(π θ₀) : Lifts F E K) ≤ θ
⊢ False

Tactic:
hπ θ₀ ⟨_, θ.emb.comp <| inclusion <| sup_le this.1 hθ⟩
      ⟨le_sup_left, this.2⟩ ⟨le_sup_right, fun _ ↦ rfl⟩ rfl

Premises used: le_sup_left, le_sup_right, IntermediateField.Lifts.emb, Exists.intro, sup_le, IntermediateField.inclusion, AlgHom.comp, rfl, IntermediateField.Lifts.mk