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))
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:
exact 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
-- 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
have :
  ∀ (ω : Ω)
    (hω :
      ∀ (π : (↑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)),
    ∃ τ ≥ union c hc, (↑S : Set E) ⊆ (↑τ.carrier : Set E)
⊢ ∃ τ ≥ union c hc, (↑S : Set E) ⊆ (↑τ.carrier : Set E)

Tactic:
have ⟨ω, hω⟩ : ∃ ω : Ω, ∀ π : c, ∃ θ ≥ π.1, ⟨_, ω⟩ ≤ θ ∧ θ.carrier = π.1.1 ⊔ adjoin F S := by
    by_contra!; choose π hπ using this
    have := finiteDimensional_adjoin (S := (S : Set E)) fun _ _ ↦ (alg.isIntegral).1 _
    have ⟨π₀, hπ₀⟩ := hc.directed.finite_le π
    have ⟨θ, hθπ, hθ⟩ := hext _ π₀.2 S
    rw [← adjoin_le_iff] at hθ
    let θ₀ := θ.emb.comp (inclusion hθ)
    have := (hπ₀ θ₀).trans hθπ
    exact hπ θ₀ ⟨_, θ.emb.comp <| inclusion <| sup_le this.1 hθ⟩
      ⟨le_sup_left, this.2⟩ ⟨le_sup_right, fun _ ↦ rfl⟩ 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
ω : Ω
hω :
  ∀ (π : (↑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)
choose :
  ∀ (θ : (π : (↑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)
⊢ ∃ τ ≥ union c hc, (↑S : Set E) ⊆ (↑τ.carrier : Set E)

Tactic:
choose θ ge hθ eq using 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))) → 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)
⊢ ∀ (π : (↑c : Type (max u_2 u_3))), (θ π).carrier = adjoin F ((↑(↑π : Lifts F E K).carrier : Set E) ∪ (↑S : Set E))

Tactic:
simp_rw [← restrictScalars_adjoin_eq_sup, restrictScalars_adjoin] at eq

Premises used: IntermediateField.restrictScalars_adjoin_eq_sup, IntermediateField.restrictScalars_adjoin
-- 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))
inr :
  ∀
    (this :
      ∀ (π₁ π₂ : (↑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) (θ π₂) (θ π₁))
    (h : ¬π₁ ≤ π₂),
    (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₁) (θ π₂) ∨ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₂) (θ π₁)
wlog :
  ∀ (π₁ π₂ : (↑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) (θ π₂) (θ π₁)
⊢ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₁) (θ π₂) ∨ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₂) (θ π₁)

Tactic:
wlog h : π₁ ≤ π₂ generalizing π₁ π₂
-- 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))
this :
  ∀ (π₁ π₂ : (↑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) (θ π₂) (θ π₁)
h : ¬π₁ ≤ π₂
⊢ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₁) (θ π₂) ∨ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₂) (θ π₁)

Tactic:
(this _ _ <| (hc.total π₁.2 π₂.2).resolve_left h).symm

Premises used: Or.resolve_left, Or.symm, IsChain.total, Subtype.property
-- 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))
this :
  ∀ (π₁ π₂ : (↑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) (θ π₂) (θ π₁)
h : ¬π₁ ≤ π₂
⊢ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₁) (θ π₂) ∨ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₂) (θ π₁)

Tactic:
exact (this _ _ <| (hc.total π₁.2 π₂.2).resolve_left h).symm

Premises used: Or.resolve_left, Or.symm, IsChain.total, Subtype.property
-- 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 : π₁ ≤ π₂
⊢ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₁) (θ π₂) ∨ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₂) (θ π₁)

Tactic:
.inl (le_iff.mpr ⟨?_, algHom_ext_of_eq_adjoin _ (eq _) ?_⟩)

Premises used: Iff.mpr, Exists.intro, IntermediateField.algHom_ext_of_eq_adjoin, Or.inl, IntermediateField.Lifts.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))) → 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
refine_2 :
  ∀ (x : E) (hx : x ∈ (↑(↑π₁ : Lifts F E K).carrier : Set E) ∪ (↑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)
⊢ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₁) (θ π₂) ∨ (fun (x1 x2 : Lifts F E K) ↦ x1 ≤ x2) (θ π₂) (θ π₁)

Tactic:
refine .inl (le_iff.mpr ⟨?_, algHom_ext_of_eq_adjoin _ (eq _) ?_⟩)
-- 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 : π₁ ≤ π₂
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)))
⊢ (θ π₁).carrier ≤ (θ π₂).carrier

Tactic:
rw [eq, eq]
-- 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 : π₁ ≤ π₂
⊢ 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:
adjoin.mono _ _ _ (Set.union_subset_union_left _ h.1)

Premises used: IntermediateField.adjoin.mono, Set.union_subset_union_left
-- 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 : π₁ ≤ π₂
⊢ 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:
exact adjoin.mono _ _ _ (Set.union_subset_union_left _ h.1)

Premises used: IntermediateField.adjoin.mono, Set.union_subset_union_left
-- 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 ∈ (↑(↑π₁ : 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)
    (((θ π₁).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)
⊢ 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)

Tactic:
change (θ π₂).emb (inclusion (ge π₂).1 <| inclusion h.1 ⟨x, hx⟩) =
        (θ π₁).emb (inclusion (ge π₁).1 ⟨x, hx⟩)

Premises used: Subtype.mk, IntermediateField.Lifts.emb, IntermediateField.inclusion, DFunLike.coe
-- 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 ∈ (↑(↑π₁ : 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)
refine_2₂ 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)
⊢ 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)

Tactic:
rw [(ge π₁).2, (ge π₂).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 = 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)
    (((θ π₁).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)
⊢ 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)

Tactic:
change (θ π₂).emb (inclusion (hθ π₂).1 ⟨x, subset_adjoin _ _ hx⟩) =
        (θ π₁).emb (inclusion (hθ π₁).1 ⟨x, subset_adjoin _ _ hx⟩)

Premises used: IntermediateField.subset_adjoin, Subtype.mk, IntermediateField.Lifts.emb, IntermediateField.inclusion, DFunLike.coe