awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
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 : π₁ ≤ π₂
⊢ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₁) (θ π₂) ∨ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₂) (θ π₁)
have refine_1 : (θ π₁).carrier ≤ (θ π₂).carrier
Tactic: refine .inl (le_iff.mpr ⟨?_, algHom_ext_of_eq_adjoin _ (eq _) ?_⟩)
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
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 : π₁ ≤ π₂
refine_1 : (θ π₁).carrier ≤ (θ π₂).carrier
⊢ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₁) (θ π₂) ∨ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₂) (θ π₁)
have refine_2 : ∀ (x : E) (hx : x ∈ (↑(↑π₁ : Lifts F E K).carrier : Set E) ∪ (↑S : Set E)),
  Eq.{u_3 + 1} (α := K)
    (((θ π₂).emb.comp (inclusion sorry) : (a : ↥(θ π₁).carrier) → K)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ (θ π₁).carrier) x sorry) :
      K)
    (((θ π₁).emb : (a : ↥(θ π₁).carrier) → K) (Subtype.mk (p := fun (x : E) ↦ x ∈ (θ π₁).carrier) x sorry) : K)
Tactic: refine .inl (le_iff.mpr ⟨?_, algHom_ext_of_eq_adjoin _ (eq _) ?_⟩)
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
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 : π₁ ≤ π₂
⊢ (θ π₁).carrier ≤ (θ π₂).carrier
have refine_1 : LE.le (α := IntermediateField F E) (adjoin F ((↑(↑π₁ : Lifts F E K).carrier : Set E) ∪ (↑S : Set E)))
  (adjoin F ((↑(↑π₂ : Lifts F E K).carrier : Set E) ∪ (↑S : Set E)))
Tactic: rw [eq, eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
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 ∈ (↑(↑π₁ : Lifts F E K).carrier : Set E)
⊢ Eq.{u_3 + 1} (α := K)
    (((θ π₂).emb.comp (inclusion ⋯) : (a : ↥(θ π₁).carrier) → K)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ (θ π₁).carrier) x ⋯) :
      K)
    (((θ π₁).emb : (a : ↥(θ π₁).carrier) → K) (Subtype.mk (p := fun (x : E) ↦ x ∈ (θ π₁).carrier) x ⋯) : K)
have refine_2 : Eq.{u_3 + 1} (α := K)
  (((θ π₂).emb : (a : ↥(θ π₂).carrier) → K)
      ((inclusion sorry : (a : ↥(↑π₂ : Lifts F E K).carrier) → ↥(θ π₂).carrier)
          ((inclusion sorry : (a : ↥(↑π₁ : Lifts F E K).carrier) → ↥(↑π₂ : Lifts F E K).carrier)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx)) :
        ↥(θ π₂).carrier) :
    K)
  (((θ π₁).emb : (a : ↥(θ π₁).carrier) → K)
      ((inclusion sorry : (a : ↥(↑π₁ : Lifts F E K).carrier) → ↥(θ π₁).carrier)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx) :
        ↥(θ π₁).carrier) :
    K)
Tactic: change (θ π₂).emb (inclusion (ge π₂).1 <| inclusion h.1 ⟨x, hx⟩) =
        (θ π₁).emb (inclusion (ge π₁).1 ⟨x, hx⟩)
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
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 ∈ (↑(↑π₁ : Lifts F E K).carrier : Set E)
⊢ Eq.{u_3 + 1} (α := K)
    (((θ π₂).emb : (a : ↥(θ π₂).carrier) → K)
        ((inclusion ⋯ : (a : ↥(↑π₂ : Lifts F E K).carrier) → ↥(θ π₂).carrier)
            ((inclusion ⋯ : (a : ↥(↑π₁ : Lifts F E K).carrier) → ↥(↑π₂ : Lifts F E K).carrier)
              (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx)) :
          ↥(θ π₂).carrier) :
      K)
    (((θ π₁).emb : (a : ↥(θ π₁).carrier) → K)
        ((inclusion ⋯ : (a : ↥(↑π₁ : Lifts F E K).carrier) → ↥(θ π₁).carrier)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx) :
          ↥(θ π₁).carrier) :
      K)
have refine_2 : Eq.{u_3 + 1} (α := K)
  (((θ π₂).emb : (a : ↥(θ π₂).carrier) → K)
      ((inclusion sorry : (a : ↥(↑π₂ : Lifts F E K).carrier) → ↥(θ π₂).carrier)
          ((inclusion sorry : (a : ↥(↑π₁ : Lifts F E K).carrier) → ↥(↑π₂ : Lifts F E K).carrier)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx)) :
        ↥(θ π₂).carrier) :
    K)
  (((↑π₁ : Lifts F E K).emb : (a : ↥(↑π₁ : Lifts F E K).carrier) → K)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx) :
    K)
Tactic: rw [(ge π₁).2, (ge π₂).2, h.2]
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
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 ∈ (↑(↑π₁ : Lifts F E K).carrier : Set E)
refine_2 :
  Eq.{u_3 + 1} (α := K)
    (((θ π₂).emb : (a : ↥(θ π₂).carrier) → K)
        ((inclusion ⋯ : (a : ↥(↑π₂ : Lifts F E K).carrier) → ↥(θ π₂).carrier)
            ((inclusion ⋯ : (a : ↥(↑π₁ : Lifts F E K).carrier) → ↥(↑π₂ : Lifts F E K).carrier)
              (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx)) :
          ↥(θ π₂).carrier) :
      K)
    (((↑π₁ : Lifts F E K).emb : (a : ↥(↑π₁ : Lifts F E K).carrier) → K)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx) :
      K)
⊢ Eq.{u_3 + 1} (α := K)
    (((θ π₂).emb : (a : ↥(θ π₂).carrier) → K)
        ((inclusion ⋯ : (a : ↥(↑π₂ : Lifts F E K).carrier) → ↥(θ π₂).carrier)
            ((inclusion ⋯ : (a : ↥(↑π₁ : Lifts F E K).carrier) → ↥(↑π₂ : Lifts F E K).carrier)
              (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx)) :
          ↥(θ π₂).carrier) :
      K)
    (((θ π₁).emb : (a : ↥(θ π₁).carrier) → K)
        ((inclusion ⋯ : (a : ↥(↑π₁ : Lifts F E K).carrier) → ↥(θ π₁).carrier)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx) :
          ↥(θ π₁).carrier) :
      K)
have refine_2₁ : Eq.{u_3 + 1} (α := K)
  (((↑π₂ : Lifts F E K).emb : (a : ↥(↑π₂ : Lifts F E K).carrier) → K)
      ((inclusion sorry : (a : ↥(↑π₁ : Lifts F E K).carrier) → ↥(↑π₂ : Lifts F E K).carrier)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx) :
        ↥(↑π₂ : Lifts F E K).carrier) :
    K)
  (((↑π₁ : Lifts F E K).emb : (a : ↥(↑π₁ : Lifts F E K).carrier) → K)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx) :
    K)
Tactic: rw [(ge π₁).2, (ge π₂).2, h.2]
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
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 ∈ (↑(↑π₁ : Lifts F E K).carrier : Set E)
refine_2 :
  Eq.{u_3 + 1} (α := K)
    (((θ π₂).emb : (a : ↥(θ π₂).carrier) → K)
        ((inclusion ⋯ : (a : ↥(↑π₂ : Lifts F E K).carrier) → ↥(θ π₂).carrier)
            ((inclusion ⋯ : (a : ↥(↑π₁ : Lifts F E K).carrier) → ↥(↑π₂ : Lifts F E K).carrier)
              (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx)) :
          ↥(θ π₂).carrier) :
      K)
    (((↑π₁ : Lifts F E K).emb : (a : ↥(↑π₁ : Lifts F E K).carrier) → K)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx) :
      K)
refine_2₁ :
  Eq.{u_3 + 1} (α := K)
    (((↑π₂ : Lifts F E K).emb : (a : ↥(↑π₂ : Lifts F E K).carrier) → K)
        ((inclusion ⋯ : (a : ↥(↑π₁ : Lifts F E K).carrier) → ↥(↑π₂ : Lifts F E K).carrier)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx) :
          ↥(↑π₂ : Lifts F E K).carrier) :
      K)
    (((↑π₁ : Lifts F E K).emb : (a : ↥(↑π₁ : Lifts F E K).carrier) → K)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx) :
      K)
⊢ Eq.{u_3 + 1} (α := K)
    (((θ π₂).emb : (a : ↥(θ π₂).carrier) → K)
        ((inclusion ⋯ : (a : ↥(↑π₂ : Lifts F E K).carrier) → ↥(θ π₂).carrier)
            ((inclusion ⋯ : (a : ↥(↑π₁ : Lifts F E K).carrier) → ↥(↑π₂ : Lifts F E K).carrier)
              (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx)) :
          ↥(θ π₂).carrier) :
      K)
    (((θ π₁).emb : (a : ↥(θ π₁).carrier) → K)
        ((inclusion ⋯ : (a : ↥(↑π₁ : Lifts F E K).carrier) → ↥(θ π₁).carrier)
            (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx) :
          ↥(θ π₁).carrier) :
      K)
have refine_2₂ : Eq.{u_3 + 1} (α := K)
  (((↑π₁ : Lifts F E K).emb : (a : ↥(↑π₁ : Lifts F E K).carrier) → K)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx) :
    K)
  (((↑π₁ : Lifts F E K).emb : (a : ↥(↑π₁ : Lifts F E K).carrier) → K)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ (↑π₁ : Lifts F E K).carrier) x hx) :
    K)
Tactic: rw [(ge π₁).2, (ge π₂).2, h.2]
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
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)
⊢ Eq.{u_3 + 1} (α := K)
    (((θ π₂).emb.comp (inclusion ⋯) : (a : ↥(θ π₁).carrier) → K)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ (θ π₁).carrier) x ⋯) :
      K)
    (((θ π₁).emb : (a : ↥(θ π₁).carrier) → K) (Subtype.mk (p := fun (x : E) ↦ x ∈ (θ π₁).carrier) x ⋯) : K)
have refine_2 : Eq.{u_3 + 1} (α := K)
  (((θ π₂).emb : (a : ↥(θ π₂).carrier) → K)
      ((inclusion sorry : (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
            sorry) :
        ↥(θ π₂).carrier) :
    K)
  (((θ π₁).emb : (a : ↥(θ π₁).carrier) → K)
      ((inclusion sorry : (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
            sorry) :
        ↥(θ π₁).carrier) :
    K)
Tactic: change (θ π₂).emb (inclusion (hθ π₂).1 ⟨x, subset_adjoin _ _ hx⟩) =
        (θ π₁).emb (inclusion (hθ π₁).1 ⟨x, subset_adjoin _ _ hx⟩)
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
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)
⊢ 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)
have refine_2 : Eq.{u_3 + 1} (α := K)
  (((θ π₂).emb : (a : ↥(θ π₂).carrier) → K)
      ((inclusion sorry : (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
            sorry) :
        ↥(θ π₂).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 sorry) :
    K)
Tactic: rw [(hθ π₁).2, (hθ π₂).2]
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
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)
⊢ 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)
have 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 sorry) :
    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 sorry) :
    K)
Tactic: rw [(hθ π₁).2, (hθ π₂).2]
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (hypothesis)
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)
⊢ ∃ τ ≥ union c hc, (↑S : Set E) ⊆ (↑τ.carrier : Set E)
have this : 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]
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
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)
have refine : (↑S : Set E) ⊆ (↑(union (Set.range θ) this).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, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Extension (goal)
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) ⊆ (↑(union (Set.range θ) this).carrier : Set E)
have 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)
Tactic: simp_rw [carrier_union, iSup_range', eq]