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₂ L₃ : Lifts F E K
h₁₂ : L₁.carrier ≤ L₂.carrier
h₁₂' :
  ∀ (x : ↥L₁.carrier),
    Eq.{u_3 + 1} (α := K)
      ((L₂.emb : (a : ↥L₂.carrier) → K) ((inclusion h₁₂ : (a : ↥L₁.carrier) → ↥L₂.carrier) x : ↥L₂.carrier) : K)
      ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
h₂₃ : L₂.carrier ≤ L₃.carrier
h₂₃' :
  ∀ (x : ↥L₂.carrier),
    Eq.{u_3 + 1} (α := K)
      ((L₃.emb : (a : ↥L₃.carrier) → K) ((inclusion h₂₃ : (a : ↥L₂.carrier) → ↥L₃.carrier) x : ↥L₃.carrier) : K)
      ((L₂.emb : (a : ↥L₂.carrier) → K) x : K)
⊢ ∃ (h : L₁.carrier ≤ L₃.carrier),
    ∀ (x : ↥L₁.carrier),
      Eq.{u_3 + 1} (α := K)
        ((L₃.emb : (a : ↥L₃.carrier) → K) ((inclusion h : (a : ↥L₁.carrier) → ↥L₃.carrier) x : ↥L₃.carrier) : K)
        ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)

Tactic:
⟨h₁₂.trans h₂₃, fun _ ↦ ?_⟩

Premises used: Exists.intro, 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
S : Set E
L₁ L₂ L₃ : Lifts F E K
h₁₂ : L₁.carrier ≤ L₂.carrier
h₁₂' :
  ∀ (x : ↥L₁.carrier),
    Eq.{u_3 + 1} (α := K)
      ((L₂.emb : (a : ↥L₂.carrier) → K) ((inclusion h₁₂ : (a : ↥L₁.carrier) → ↥L₂.carrier) x : ↥L₂.carrier) : K)
      ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
h₂₃ : L₂.carrier ≤ L₃.carrier
h₂₃' :
  ∀ (x : ↥L₂.carrier),
    Eq.{u_3 + 1} (α := K)
      ((L₃.emb : (a : ↥L₃.carrier) → K) ((inclusion h₂₃ : (a : ↥L₂.carrier) → ↥L₃.carrier) x : ↥L₃.carrier) : K)
      ((L₂.emb : (a : ↥L₂.carrier) → K) x : K)
refine :
  ∀ (x : ↥L₁.carrier),
    Eq.{u_3 + 1} (α := K)
      ((L₃.emb : (a : ↥L₃.carrier) → K) ((inclusion ⋯ : (a : ↥L₁.carrier) → ↥L₃.carrier) x : ↥L₃.carrier) : K)
      ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
⊢ ∃ (h : L₁.carrier ≤ L₃.carrier),
    ∀ (x : ↥L₁.carrier),
      Eq.{u_3 + 1} (α := K)
        ((L₃.emb : (a : ↥L₃.carrier) → K) ((inclusion h : (a : ↥L₁.carrier) → ↥L₃.carrier) x : ↥L₃.carrier) : K)
        ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)

Tactic:
refine ⟨h₁₂.trans h₂₃, fun _ ↦ ?_⟩
-- 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₂ L₃ : Lifts F E K
h₁₂ : L₁.carrier ≤ L₂.carrier
h₁₂' :
  ∀ (x : ↥L₁.carrier),
    Eq.{u_3 + 1} (α := K)
      ((L₂.emb : (a : ↥L₂.carrier) → K) ((inclusion h₁₂ : (a : ↥L₁.carrier) → ↥L₂.carrier) x : ↥L₂.carrier) : K)
      ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
h₂₃ : L₂.carrier ≤ L₃.carrier
h₂₃' :
  ∀ (x : ↥L₂.carrier),
    Eq.{u_3 + 1} (α := K)
      ((L₃.emb : (a : ↥L₃.carrier) → K) ((inclusion h₂₃ : (a : ↥L₂.carrier) → ↥L₃.carrier) x : ↥L₃.carrier) : K)
      ((L₂.emb : (a : ↥L₂.carrier) → K) x : K)
x : ↥L₁.carrier
rw :
  Eq.{u_3 + 1} (α := K)
    ((L₃.emb : (a : ↥L₃.carrier) → K)
        ((inclusion h₂₃ : (a : ↥L₂.carrier) → ↥L₃.carrier) ((inclusion h₁₂ : (a : ↥L₁.carrier) → ↥L₂.carrier) x) :
          ↥L₃.carrier) :
      K)
    ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
rw₁ :
  Eq.{u_3 + 1} (α := K)
    ((L₂.emb : (a : ↥L₂.carrier) → K) ((inclusion h₁₂ : (a : ↥L₁.carrier) → ↥L₂.carrier) x : ↥L₂.carrier) : K)
    ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
rw₂ rw₃ : Eq.{u_3 + 1} (α := K) ((L₁.emb : (a : ↥L₁.carrier) → K) x : K) ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
⊢ Eq.{u_3 + 1} (α := K)
    ((L₃.emb : (a : ↥L₃.carrier) → K) ((inclusion ⋯ : (a : ↥L₁.carrier) → ↥L₃.carrier) x : ↥L₃.carrier) : K)
    ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)

Tactic:
rw [← inclusion_inclusion h₁₂ h₂₃, h₂₃', h₁₂']

Premises used: IntermediateField.inclusion_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₁ : IntermediateField F E
e₁ : AlgHom.{u_1, u_2, u_3} F (↥L₁) K
L₂ : IntermediateField F E
e₂ : AlgHom.{u_1, u_2, u_3} F (↥L₂) K
h₁₂ : { carrier := L₁, emb := e₁ : Lifts F E K }.carrier ≤ { carrier := L₂, emb := e₂ : Lifts F E K }.carrier
h₁₂' :
  ∀ (x : ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier),
    Eq.{u_3 + 1} (α := K)
      (({ carrier := L₂, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₂, emb := e₂ }.carrier) → K)
          ((inclusion h₁₂ : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → ↥{ carrier := L₂, emb := e₂ }.carrier) x :
            ↥{ carrier := L₂, emb := e₂ : Lifts F E K }.carrier) :
        K)
      (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K) x : K)
h₂₁ : { carrier := L₂, emb := e₂ : Lifts F E K }.carrier ≤ { carrier := L₁, emb := e₁ : Lifts F E K }.carrier
h₂₁' :
  ∀ (x : ↥{ carrier := L₂, emb := e₂ : Lifts F E K }.carrier),
    Eq.{u_3 + 1} (α := K)
      (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K)
          ((inclusion h₂₁ : (a : ↥{ carrier := L₂, emb := e₂ }.carrier) → ↥{ carrier := L₁, emb := e₁ }.carrier) x :
            ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier) :
        K)
      (({ carrier := L₂, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₂, emb := e₂ }.carrier) → K) x : K)
⊢ L₁ = L₂

Tactic:
h₁₂.antisymm h₂₁

Premises used: LE.le.antisymm
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L₁ : IntermediateField F E
e₁ : AlgHom.{u_1, u_2, u_3} F (↥L₁) K
L₂ : IntermediateField F E
e₂ : AlgHom.{u_1, u_2, u_3} F (↥L₂) K
h₁₂ : { carrier := L₁, emb := e₁ : Lifts F E K }.carrier ≤ { carrier := L₂, emb := e₂ : Lifts F E K }.carrier
h₁₂' :
  ∀ (x : ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier),
    Eq.{u_3 + 1} (α := K)
      (({ carrier := L₂, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₂, emb := e₂ }.carrier) → K)
          ((inclusion h₁₂ : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → ↥{ carrier := L₂, emb := e₂ }.carrier) x :
            ↥{ carrier := L₂, emb := e₂ : Lifts F E K }.carrier) :
        K)
      (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K) x : K)
h₂₁ : { carrier := L₂, emb := e₂ : Lifts F E K }.carrier ≤ { carrier := L₁, emb := e₁ : Lifts F E K }.carrier
h₂₁' :
  ∀ (x : ↥{ carrier := L₂, emb := e₂ : Lifts F E K }.carrier),
    Eq.{u_3 + 1} (α := K)
      (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K)
          ((inclusion h₂₁ : (a : ↥{ carrier := L₂, emb := e₂ }.carrier) → ↥{ carrier := L₁, emb := e₁ }.carrier) x :
            ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier) :
        K)
      (({ carrier := L₂, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₂, emb := e₂ }.carrier) → K) x : K)
obtain :
  ∀ (e₂ : AlgHom.{u_1, u_2, u_3} F (↥L₁) K)
    (h₁₂ : { carrier := L₁, emb := e₁ : Lifts F E K }.carrier ≤ { carrier := L₁, emb := e₂ : Lifts F E K }.carrier)
    (h₁₂' :
      ∀ (x : ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier),
        Eq.{u_3 + 1} (α := K)
          (({ carrier := L₁, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → K)
              ((inclusion h₁₂ : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → ↥{ carrier := L₁, emb := e₂ }.carrier) x :
                ↥{ carrier := L₁, emb := e₂ : Lifts F E K }.carrier) :
            K)
          (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K) x : K))
    (h₂₁ : { carrier := L₁, emb := e₂ : Lifts F E K }.carrier ≤ { carrier := L₁, emb := e₁ : Lifts F E K }.carrier)
    (h₂₁' :
      ∀ (x : ↥{ carrier := L₁, emb := e₂ : Lifts F E K }.carrier),
        Eq.{u_3 + 1} (α := K)
          (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K)
              ((inclusion h₂₁ : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → ↥{ carrier := L₁, emb := e₁ }.carrier) x :
                ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier) :
            K)
          (({ carrier := L₁, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → K) x : K)),
    { carrier := L₁, emb := e₁ : Lifts F E K } = { carrier := L₁, emb := e₂ }
⊢ { carrier := L₁, emb := e₁ : Lifts F E K } = { carrier := L₂, emb := e₂ }

Tactic:
obtain rfl : L₁ = L₂ := h₁₂.antisymm h₂₁

Premises used: LE.le.antisymm, 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
S : Set E
L₁ : IntermediateField F E
e₁ e₂ : AlgHom.{u_1, u_2, u_3} F (↥L₁) K
h₁₂ : { carrier := L₁, emb := e₁ : Lifts F E K }.carrier ≤ { carrier := L₁, emb := e₂ : Lifts F E K }.carrier
h₁₂' :
  ∀ (x : ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier),
    Eq.{u_3 + 1} (α := K)
      (({ carrier := L₁, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → K)
          ((inclusion h₁₂ : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → ↥{ carrier := L₁, emb := e₂ }.carrier) x :
            ↥{ carrier := L₁, emb := e₂ : Lifts F E K }.carrier) :
        K)
      (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K) x : K)
h₂₁ : { carrier := L₁, emb := e₂ : Lifts F E K }.carrier ≤ { carrier := L₁, emb := e₁ : Lifts F E K }.carrier
h₂₁' :
  ∀ (x : ↥{ carrier := L₁, emb := e₂ : Lifts F E K }.carrier),
    Eq.{u_3 + 1} (α := K)
      (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K)
          ((inclusion h₂₁ : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → ↥{ carrier := L₁, emb := e₁ }.carrier) x :
            ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier) :
        K)
      (({ carrier := L₁, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → K) x : K)
e_emb : e₁ = e₂
⊢ { carrier := L₁, emb := e₁ : Lifts F E K } = { carrier := L₁, emb := e₂ }

Tactic:
congr
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L₁ : IntermediateField F E
e₁ e₂ : AlgHom.{u_1, u_2, u_3} F (↥L₁) K
h₁₂ : { carrier := L₁, emb := e₁ : Lifts F E K }.carrier ≤ { carrier := L₁, emb := e₂ : Lifts F E K }.carrier
h₁₂' :
  ∀ (x : ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier),
    Eq.{u_3 + 1} (α := K)
      (({ carrier := L₁, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → K)
          ((inclusion h₁₂ : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → ↥{ carrier := L₁, emb := e₂ }.carrier) x :
            ↥{ carrier := L₁, emb := e₂ : Lifts F E K }.carrier) :
        K)
      (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K) x : K)
h₂₁ : { carrier := L₁, emb := e₂ : Lifts F E K }.carrier ≤ { carrier := L₁, emb := e₁ : Lifts F E K }.carrier
h₂₁' :
  ∀ (x : ↥{ carrier := L₁, emb := e₂ : Lifts F E K }.carrier),
    Eq.{u_3 + 1} (α := K)
      (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K)
          ((inclusion h₂₁ : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → ↥{ carrier := L₁, emb := e₁ }.carrier) x :
            ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier) :
        K)
      (({ carrier := L₁, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → K) x : K)
⊢ e₁ = e₂

Tactic:
AlgHom.ext h₂₁'

Premises used: AlgHom.ext
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
S : Set E
L₁ : IntermediateField F E
e₁ e₂ : AlgHom.{u_1, u_2, u_3} F (↥L₁) K
h₁₂ : { carrier := L₁, emb := e₁ : Lifts F E K }.carrier ≤ { carrier := L₁, emb := e₂ : Lifts F E K }.carrier
h₁₂' :
  ∀ (x : ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier),
    Eq.{u_3 + 1} (α := K)
      (({ carrier := L₁, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → K)
          ((inclusion h₁₂ : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → ↥{ carrier := L₁, emb := e₂ }.carrier) x :
            ↥{ carrier := L₁, emb := e₂ : Lifts F E K }.carrier) :
        K)
      (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K) x : K)
h₂₁ : { carrier := L₁, emb := e₂ : Lifts F E K }.carrier ≤ { carrier := L₁, emb := e₁ : Lifts F E K }.carrier
h₂₁' :
  ∀ (x : ↥{ carrier := L₁, emb := e₂ : Lifts F E K }.carrier),
    Eq.{u_3 + 1} (α := K)
      (({ carrier := L₁, emb := e₁ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₁ }.carrier) → K)
          ((inclusion h₂₁ : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → ↥{ carrier := L₁, emb := e₁ }.carrier) x :
            ↥{ carrier := L₁, emb := e₁ : Lifts F E K }.carrier) :
        K)
      (({ carrier := L₁, emb := e₂ : Lifts F E K }.emb : (a : ↥{ carrier := L₁, emb := e₂ }.carrier) → K) x : K)
⊢ e₁ = e₂

Tactic:
exact AlgHom.ext h₂₁'

Premises used: AlgHom.ext
-- 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 : Lifts F E K
x : ↥(carrier { carrier := ⊥, emb := AlgHom.comp (Algebra.ofId F K) (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) })
obtain :
  ∀ (x : F),
    Eq.{u_3 + 1} (α := K)
      ((L.emb : (a : ↥L.carrier) → K)
          ((inclusion ⋯ :
                (a : ↥{ carrier := ⊥, emb := (Algebra.ofId F K).comp (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) }.carrier) →
                  ↥L.carrier)
              (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) x) :
            ↥L.carrier) :
        K)
      ((emb { carrier := ⊥, emb := AlgHom.comp (Algebra.ofId F K) (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) } :
            (a : ↥{ carrier := ⊥, emb := (Algebra.ofId F K).comp (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) }.carrier) → K)
          (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) x : ↥⊥) :
        K)
⊢ Eq.{u_3 + 1} (α := K)
    ((L.emb : (a : ↥L.carrier) → K)
        ((inclusion ⋯ :
              (a : ↥{ carrier := ⊥, emb := (Algebra.ofId F K).comp (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) }.carrier) →
                ↥L.carrier)
            x :
          ↥L.carrier) :
      K)
    ((emb { carrier := ⊥, emb := AlgHom.comp (Algebra.ofId F K) (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) } :
          (a : ↥{ carrier := ⊥, emb := (Algebra.ofId F K).comp (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) }.carrier) → K)
        x :
      K)

Tactic:
obtain ⟨x, rfl⟩ := (botEquiv F E).symm.surjective x

Premises used: AlgEquiv.symm, IntermediateField.botEquiv, AlgEquiv.surjective, 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
S : Set E
L : Lifts F E K
x : F
simp_rw :
  Eq.{u_3 + 1} (α := K)
    ((L.emb : (a : ↥L.carrier) → K)
        ((inclusion ⋯ : (a : ↥⊥) → ↥L.carrier)
            (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) x) :
          ↥L.carrier) :
      K)
    ((Algebra.ofId F K : (a : F) → K) x : K)
⊢ Eq.{u_3 + 1} (α := K)
    ((L.emb : (a : ↥L.carrier) → K)
        ((inclusion ⋯ :
              (a : ↥{ carrier := ⊥, emb := (Algebra.ofId F K).comp (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) }.carrier) →
                ↥L.carrier)
            (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) x) :
          ↥L.carrier) :
      K)
    ((emb { carrier := ⊥, emb := AlgHom.comp (Algebra.ofId F K) (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) } :
          (a : ↥{ carrier := ⊥, emb := (Algebra.ofId F K).comp (↑(botEquiv F E) : ↥⊥ →ₐ[F] F) }.carrier) → K)
        (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) x : ↥⊥) :
      K)

Tactic:
simp_rw [AlgHom.comp_apply, AlgEquiv.coe_algHom, AlgEquiv.apply_symm_apply]

Premises used: AlgHom.comp_apply, AlgEquiv.apply_symm_apply, AlgEquiv.coe_algHom
-- 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 : Lifts F E K
x : F
⊢ Eq.{u_3 + 1} (α := K)
    ((L.emb : (a : ↥L.carrier) → K)
        ((inclusion ⋯ : (a : ↥⊥) → ↥L.carrier)
            (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) x) :
          ↥L.carrier) :
      K)
    ((Algebra.ofId F K : (a : F) → K) x : K)

Tactic:
L.emb.commutes x

Premises used: IntermediateField.Lifts.emb, AlgHom.commutes
-- 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 : Lifts F E K
x : F
⊢ Eq.{u_3 + 1} (α := K)
    ((L.emb : (a : ↥L.carrier) → K)
        ((inclusion ⋯ : (a : ↥⊥) → ↥L.carrier)
            (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) x) :
          ↥L.carrier) :
      K)
    ((Algebra.ofId F K : (a : F) → K) x : K)

Tactic:
exact L.emb.commutes x

Premises used: IntermediateField.Lifts.emb, AlgHom.commutes
-- 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
L₁ L₂ : Lifts F E K
simp_rw :
  L₁ ≤ L₂ ↔
    ∃ (h : L₁.carrier ≤ L₂.carrier),
      ∀ (x : ↥L₁.carrier),
        Eq.{u_3 + 1} (α := K) ((L₂.emb.comp (inclusion ⋯) : (a : ↥L₁.carrier) → K) x : K)
          ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)
⊢ L₁ ≤ L₂ ↔ ∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb

Tactic:
simp_rw [AlgHom.ext_iff]

Premises used: AlgHom.ext_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
L₁ L₂ : Lifts F E K
⊢ L₁ ≤ L₂ ↔
    ∃ (h : L₁.carrier ≤ L₂.carrier),
      ∀ (x : ↥L₁.carrier),
        Eq.{u_3 + 1} (α := K) ((L₂.emb.comp (inclusion ⋯) : (a : ↥L₁.carrier) → K) x : K)
          ((L₁.emb : (a : ↥L₁.carrier) → K) x : K)

Tactic:
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
L₁ L₂ : Lifts F E K
⊢ L₁ = L₂ ↔ L₁ ≤ L₂ ∧ L₁.carrier = L₂.carrier

Tactic:
⟨fun eq ↦ ⟨eq.le, congr_arg _ eq⟩, fun ⟨le, eq⟩ ↦ le.antisymm ⟨eq.ge, fun x ↦ (le.2 ⟨x, _⟩).symm⟩⟩

Premises used: _private.0.IntermediateField.Lifts.eq_iff_le_carrier_eq.match_1, Eq.ge, LE.le.antisymm, Eq.le, Subtype.mk, congr_arg, Set.inclusion._proof_1, And.intro, Iff.intro, Exists.intro, IntermediateField.Lifts.carrier, Eq.symm, Subtype.val, 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
L₁ L₂ : Lifts F E K
rw :
  (∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb) ∧ L₁.carrier = L₂.carrier ↔
    ∃ (h : L₁.carrier = L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb
⊢ L₁ = L₂ ↔ ∃ (h : L₁.carrier = L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb

Tactic:
rw [eq_iff_le_carrier_eq, le_iff]

Premises used: IntermediateField.Lifts.eq_iff_le_carrier_eq, 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
L₁ L₂ : Lifts F E K
⊢ (∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb) ∧ L₁.carrier = L₂.carrier ↔
    ∃ (h : L₁.carrier = L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb

Tactic:
⟨fun h ↦ ⟨h.2, h.1.2⟩, fun h ↦ ⟨⟨h.1.le, h.2⟩, h.1⟩⟩

Premises used: Eq.le, And.right, And.left, And.intro, Iff.intro, 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
L₁ L₂ : Lifts F E K
⊢ (∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb) ∧ L₁.carrier = L₂.carrier ↔
    ∃ (h : L₁.carrier = L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb

Tactic:
exact ⟨fun h ↦ ⟨h.2, h.1.2⟩, fun h ↦ ⟨⟨h.1.le, h.2⟩, h.1⟩⟩
-- Module: Mathlib.FieldTheory.Extension
Goal:
F : Type u_1
E : Type u_2
K : Type u_3
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra F K
L₁ L₂ : Lifts F E K
rw : L₁ ≤ L₂ → (L₁ ≠ L₂ ↔ L₁.carrier ≠ L₂.carrier)
⊢ L₁ < L₂ ↔ L₁ ≤ L₂ ∧ L₁.carrier ≠ L₂.carrier

Tactic:
rw [lt_iff_le_and_ne, and_congr_right]

Premises used: lt_iff_le_and_ne, and_congr_right
-- 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
L₁ L₂ : Lifts F E K
h : L₁ ≤ L₂
simp_rw : ¬L₁ = L₂ ↔ ¬L₁.carrier = L₂.carrier
simp_rw₁ : ¬(L₁ ≤ L₂ ∧ L₁.carrier = L₂.carrier) ↔ ¬L₁.carrier = L₂.carrier
simp_rw₂ : ¬(True ∧ L₁.carrier = L₂.carrier) ↔ ¬L₁.carrier = L₂.carrier
⊢ L₁ ≠ L₂ ↔ L₁.carrier ≠ L₂.carrier

Tactic:
simp_rw [Ne, eq_iff_le_carrier_eq, h, true_and]

Premises used: IntermediateField.Lifts.eq_iff_le_carrier_eq, Ne, true_and
-- 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
L₁ L₂ : Lifts F E K
rw :
  (∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb) ∧ L₁.carrier ≠ L₂.carrier ↔
    ∃ (h : L₁.carrier < L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb
⊢ L₁ < L₂ ↔ ∃ (h : L₁.carrier < L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb

Tactic:
rw [lt_iff_le_carrier_ne, le_iff]

Premises used: IntermediateField.Lifts.lt_iff_le_carrier_ne, 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
L₁ L₂ : Lifts F E K
⊢ (∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb) ∧ L₁.carrier ≠ L₂.carrier ↔
    ∃ (h : L₁.carrier < L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb

Tactic:
⟨fun h ↦ ⟨h.1.1.lt_of_ne h.2, h.1.2⟩, fun h ↦ ⟨⟨h.1.le, h.2⟩, h.1.ne⟩⟩

Premises used: LT.lt.le, LE.le.lt_of_ne, And.right, And.left, And.intro, Iff.intro, Exists.intro, LT.lt.ne
-- 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
L₁ L₂ : Lifts F E K
⊢ (∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb) ∧ L₁.carrier ≠ L₂.carrier ↔
    ∃ (h : L₁.carrier < L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb

Tactic:
exact ⟨fun h ↦ ⟨h.1.1.lt_of_ne h.2, h.1.2⟩, fun h ↦ ⟨⟨h.1.le, h.2⟩, h.1.ne⟩⟩
-- 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
ι : Sort u_4
ρ : ι → Lifts F E K
σ τ : Lifts F E K
hσ : ∀ (i : ι), ρ i ≤ σ
hτ : ∀ (i : ι), ρ i ≤ τ
carrier_le : σ.carrier ≤ ⨆ (i : ι), (ρ i).carrier
⊢ σ ≤ τ

Tactic:
le_iff.mpr ⟨carrier_le.trans (iSup_le fun i ↦ (hτ i).1), algHom_ext_of_eq_adjoin _
      (carrier_le.antisymm (iSup_le fun i ↦ (hσ i).1)|>.trans <| iSup_eq_adjoin _ _) fun x hx ↦
    have ⟨i, hx⟩ := Set.mem_iUnion.mp hx
    ((hτ i).2 ⟨x, hx⟩).trans ((hσ i).2 ⟨x, hx⟩).symm⟩

Premises used: Iff.mpr, Eq.ge, Set.mem_iUnion, LE.le.antisymm, IntermediateField.subset_adjoin, Subtype.mk, SetLike.coe, IntermediateField.iSup_eq_adjoin, IntermediateField.Lifts.emb, Exists.intro, IntermediateField.Lifts.carrier, Iff.mp, iSup_le, IntermediateField.algHom_ext_of_eq_adjoin, LE.le.trans, IntermediateField.inclusion, AlgHom.comp, Eq.symm, _private.0.IntermediateField.Lifts.le_of_carrier_le_iSup.match_1, Eq, DFunLike.coe, Set.iUnion, IntermediateField.Lifts.le_iff, Eq.trans