awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
refine_1 : φ '' Iio i ⊆ Iio (φ i)
⊢ Subset (α := Set E) ((⇑b : (a : (Module.rank F E).ord.ToType) → E) '' φ '' Iio i)
    ((⇑b : (a : (Module.rank F E).ord.ToType) → E) '' Iio (φ i))

Tactic:
apply image_mono

Premises used: Set.image_mono
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
hj : j ∈ Iio i
⊢ φ j ∈ Iio (φ i)

Tactic:
strictMono_leastExt hj

Premises used: Set.Mem, setOf, Field.Emb.Cardinal.strictMono_leastExt, Set.Iio
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
hj : j ∈ Iio i
⊢ φ j ∈ Iio (φ i)

Tactic:
exact strictMono_leastExt hj

Premises used: Field.Emb.Cardinal.strictMono_leastExt
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
hj : j ∈ Iio (φ i)
refine_2 :
  ∀
    (hj :
      ((b : (a : (Module.rank F E).ord.ToType) → E) j : E) ∉
        (↑(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)) : Set E)),
    j ∉ Iio (φ i)
⊢ Membership.mem (α := E) (↑(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)) : Set E)
    ((b : (a : (Module.rank F E).ord.ToType) → E) j : E)

Tactic:
contrapose hj
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
hj :
  ((b : (a : (Module.rank F E).ord.ToType) → E) j : E) ∉
    (↑(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)) : Set E)
⊢ j ∉ Iio (φ i)

Tactic:
((isLeast_leastExt i).2 hj).not_gt

Premises used: Set.Mem, Field.Emb.Cardinal.isLeast_leastExt, setOf, And.right, LE.le.not_gt, Set.Iio
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i j : (Module.rank F E).ord.ToType
hj :
  ((b : (a : (Module.rank F E).ord.ToType) → E) j : E) ∉
    (↑(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)) : Set E)
⊢ j ∉ Iio (φ i)

Tactic:
exact ((isLeast_leastExt i).2 hj).not_gt

Premises used: Field.Emb.Cardinal.isLeast_leastExt, And.right, LE.le.not_gt
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
simp_rw :
  range («ι» := (Module.rank F E).ord.ToType) (⇑b : (a : (Module.rank F E).ord.ToType) → E) ⊆
    (↑(⨆ (i : (Module.rank F E).ord.ToType), adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) '' Iio (φ i))) :
      Set E)
⊢ Eq.{v + 1} (α := IntermediateField F E)
    (⨆ (i : (Module.rank F E).ord.ToType), adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)) ⊤

Tactic:
simp_rw [adjoin_image_leastExt, eq_top_iff, ← adjoin_basis_eq_top, adjoin_le_iff]

Premises used: eq_top_iff, IntermediateField.adjoin_le_iff, Field.Emb.Cardinal.adjoin_image_leastExt, Field.Emb.Cardinal.adjoin_basis_eq_top
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ Membership.mem (α := E)
    (↑(⨆ (i : (Module.rank F E).ord.ToType), adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) '' Iio (φ i))) :
      Set E)
    ((b : (a : (Module.rank F E).ord.ToType) → E) i : E)

Tactic:
le_iSup (α := IntermediateField F E) _ (i⁺) (subset_adjoin _ _ ⟨i, ?_, rfl⟩)

Premises used: Order.succ, Set.Mem, le_iSup, IntermediateField.subset_adjoin, And.intro, Exists.intro, rfl
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
refine : i ∈ Iio (φ (i⁺))
⊢ Membership.mem (α := E)
    (↑(⨆ (i : (Module.rank F E).ord.ToType), adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) '' Iio (φ i))) :
      Set E)
    ((b : (a : (Module.rank F E).ord.ToType) → E) i : E)

Tactic:
refine le_iSup (α := IntermediateField F E) _ (i⁺) (subset_adjoin _ _ ⟨i, ?_, rfl⟩)
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ i ∈ Iio (φ (i⁺))

Tactic:
(lt_succ i).trans_le strictMono_leastExt.le_apply

Premises used: StrictMono.le_apply, Set.Mem, setOf, Field.Emb.Cardinal.strictMono_leastExt, Order.lt_succ, LT.lt.trans_le, Set.Iio
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ i ∈ Iio (φ (i⁺))

Tactic:
exact (lt_succ i).trans_le strictMono_leastExt.le_apply

Premises used: StrictMono.le_apply, Field.Emb.Cardinal.strictMono_leastExt, Order.lt_succ, LT.lt.trans_le
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
⊢ StrictMono (β := IntermediateField F E) fun (x : (Module.rank F E).ord.ToType) ↦
    adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x)

Tactic:
fun i _ h ↦ ⟨adjoin.mono _ _ _ (image_mono <| Iio_subset_Iio h.le),
    fun incl ↦ (isLeast_leastExt i).1 (incl <| subset_adjoin _ _ ⟨i, h, rfl⟩)⟩

Premises used: StrictMono, IntermediateField.adjoin.mono, Field.Emb.Cardinal.isLeast_leastExt, Set.image_mono, Function.comp, LT.lt.le, Field.Emb.Cardinal.wellOrderedBasis, IntermediateField.subset_adjoin, Set.Iio_subset_Iio, And.left, And.intro, Exists.intro, Set.image, Set.Iio, DFunLike.coe, rfl, Field.Emb.Cardinal.leastExt
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
rw :
  Eq (α := IntermediateField F E)
    (adjoin F
      ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i ∪
        {((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ) i}))
    (adjoin F
      ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i ∪
        singleton (α := E) ((b : (a : (Module.rank F E).ord.ToType) → E) (φ i) : E)))
⊢ Eq (α := IntermediateField F E) (adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio (i⁺)))
    (IntermediateField.restrictScalars F (L' :=
      ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)))
      (↥(adjoin F
            ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ ''
              Iio i)))⟮((b : (a : (Module.rank F E).ord.ToType) → E) (φ i) : E)⟯)

Tactic:
rw [Iio_succ, ← Iio_insert, image_insert_eq, ← union_singleton, adjoin_adjoin_left]

Premises used: Order.Iio_succ, Set.image_insert_eq, Set.Iio_insert, IntermediateField.adjoin_adjoin_left, Set.union_singleton
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ Eq (α := IntermediateField F E)
    (adjoin F
      ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i ∪
        {((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ) i}))
    (adjoin F
      ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i ∪
        singleton (α := E) ((b : (a : (Module.rank F E).ord.ToType) → E) (φ i) : E)))

Tactic:
rfl
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
f : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio (i⁺))) →ₐ[F] Ē
H :
  ∀ (x : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))),
    Eq (α := Ē)
      ((((succEquiv i :
                  (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio (i⁺))) →ₐ[F] Ē) →
                    (↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)) →ₐ[F] Ē) ×
                      Emb ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
                        ↥(↥(adjoin F
                                ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ ''
                                  Iio i)))⟮(b : (a : (Module.rank F E).ord.ToType) → E) (φ i)⟯)
                f).1 :
            (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) → Ē)
          x :
        Ē)
      ((f.comp (Subalgebra.inclusion ⋯) :
            (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) → Ē)
          x :
        Ē)
⊢ ((succEquiv i :
          (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio (i⁺))) →ₐ[F] Ē) →
            (↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)) →ₐ[F] Ē) ×
              Emb ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
                ↥(↥(adjoin F
                        ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ ''
                          Iio i)))⟮(b : (a : (Module.rank F E).ord.ToType) → E) (φ i)⟯)
        f).1 =
    f.comp (Subalgebra.inclusion ⋯)

Tactic:
ext
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
f : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio (i⁺))) →ₐ[F] Ē
x : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
⊢ Eq (α := Ē)
    ((((succEquiv i :
                (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio (i⁺))) →ₐ[F] Ē) →
                  (↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)) →ₐ[F] Ē) ×
                    Emb ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
                      ↥(↥(adjoin F
                              ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ ''
                                Iio i)))⟮(b : (a : (Module.rank F E).ord.ToType) → E) (φ i)⟯)
              f).1 :
          (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) → Ē)
        x :
      Ē)
    ((f.comp (Subalgebra.inclusion ⋯) :
          (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) → Ē)
        x :
      Ē)

Tactic:
simp [succEquiv, embEquivOfIsAlgClosed, embEquivOfAdjoinSplits, Equiv.sigmaEquivProdOfEquiv,
    algHomEquivSigma, AlgHom.restrictDomain, Subalgebra.inclusion, Set.inclusion, equivOfEq,
    Subalgebra.equivOfEq]

Premises used: algHomEquivSigma, Subalgebra.equivOfEq, Field.Emb.Cardinal.succEquiv, IntermediateField.equivOfEq, Subalgebra.inclusion, Field.embEquivOfIsAlgClosed, Equiv.sigmaEquivProdOfEquiv, AlgHom.restrictDomain, Set.inclusion, Field.embEquivOfAdjoinSplits
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ FiniteDimensional.{v, v} ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
    ↥(↥(adjoin F
            ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ ''
              Iio i)))⟮((b : (a : (Module.rank F E).ord.ToType) → E) (φ i) : E)⟯

Tactic:
adjoin.finiteDimensional ((Algebra.IsAlgebraic.tower_top (K := F) _).isAlgebraic _).isIntegral

Premises used: Algebra.IsAlgebraic.isAlgebraic, Set.Mem, IntermediateField.adjoin, IsAlgebraic.isIntegral, IntermediateField.adjoin.finiteDimensional
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ #(Emb ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
        ↥(↥(adjoin F
                ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ ''
                  Iio i)))⟮((b : (a : (Module.rank F E).ord.ToType) → E) (φ i) : E)⟯) <
    ℵ₀

Tactic:
lt_aleph0_of_finite _

Premises used: Cardinal.lt_aleph0_of_finite
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i j : WithTop (Module.rank F E).ord.ToType
h : i < j
top :
  ∀ (h : i < ⊤),
    LT.lt.{v} (α := IntermediateField F E)
      ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
          (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
              (fun (x : (Module.rank F E).ord.ToType) ↦
                adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
              i :
            IntermediateField F E))
        i)
      ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
          (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
              (fun (x : (Module.rank F E).ord.ToType) ↦
                adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
              i :
            IntermediateField F E))
        ⊤)
coe :
  ∀ (a : (Module.rank F E).ord.ToType) (h : i < (↑a : WithTop (Module.rank F E).ord.ToType)),
    LT.lt.{v} (α := IntermediateField F E)
      ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
          (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
              (fun (x : (Module.rank F E).ord.ToType) ↦
                adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
              i :
            IntermediateField F E))
        i)
      ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
          (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
              (fun (x : (Module.rank F E).ord.ToType) ↦
                adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
              i :
            IntermediateField F E))
        (↑a : WithTop (Module.rank F E).ord.ToType))
⊢ LT.lt.{v} (α := IntermediateField F E)
    ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
        (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
            (fun (x : (Module.rank F E).ord.ToType) ↦
              adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
            i :
          IntermediateField F E))
      i)
    ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
        (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
            (fun (x : (Module.rank F E).ord.ToType) ↦
              adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
            i :
          IntermediateField F E))
      j)

Tactic:
cases j
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
h : i < ⊤
top :
  ∀ (i : (Module.rank F E).ord.ToType) (h : (↑i : WithTop (Module.rank F E).ord.ToType) < ⊤),
    LT.lt.{v} (α := IntermediateField F E)
      ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
          (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
              (fun (x : (Module.rank F E).ord.ToType) ↦
                adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
              i :
            IntermediateField F E))
        (↑i : WithTop (Module.rank F E).ord.ToType))
      ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
          (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
              (fun (x : (Module.rank F E).ord.ToType) ↦
                adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
              i :
            IntermediateField F E))
        ⊤)
⊢ LT.lt.{v} (α := IntermediateField F E)
    ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
        (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
            (fun (x : (Module.rank F E).ord.ToType) ↦
              adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
            i :
          IntermediateField F E))
      i)
    ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
        (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
            (fun (x : (Module.rank F E).ord.ToType) ↦
              adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
            i :
          IntermediateField F E))
      ⊤)

Tactic:
obtain ⟨i, rfl⟩ := ne_top_iff_exists.mp h.ne

Premises used: WithTop.ne_top_iff_exists, Iff.mp, rfl, LT.lt.ne
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
h : (↑i : WithTop (Module.rank F E).ord.ToType) < ⊤
⊢ LT.lt.{v} (α := IntermediateField F E)
    ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
        (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
            (fun (x : (Module.rank F E).ord.ToType) ↦
              adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
            i :
          IntermediateField F E))
      (↑i : WithTop (Module.rank F E).ord.ToType))
    ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
        (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
            (fun (x : (Module.rank F E).ord.ToType) ↦
              adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
            i :
          IntermediateField F E))
      ⊤)

Tactic:
⟨le_top, fun incl ↦ (isLeast_leastExt i).1 (incl trivial)⟩

Premises used: trivial, Field.Emb.Cardinal.isLeast_leastExt, And.left, le_top, And.intro
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
h : (↑i : WithTop (Module.rank F E).ord.ToType) < ⊤
⊢ LT.lt.{v} (α := IntermediateField F E)
    ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
        (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
            (fun (x : (Module.rank F E).ord.ToType) ↦
              adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
            i :
          IntermediateField F E))
      (↑i : WithTop (Module.rank F E).ord.ToType))
    ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
        (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
            (fun (x : (Module.rank F E).ord.ToType) ↦
              adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
            i :
          IntermediateField F E))
      ⊤)

Tactic:
exact ⟨le_top, fun incl ↦ (isLeast_leastExt i).1 (incl trivial)⟩
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
a : (Module.rank F E).ord.ToType
h : i < (↑a : WithTop (Module.rank F E).ord.ToType)
coe :
  ∀ (i : (Module.rank F E).ord.ToType)
    (h : (↑i : WithTop (Module.rank F E).ord.ToType) < (↑a : WithTop (Module.rank F E).ord.ToType)),
    LT.lt.{v} (α := IntermediateField F E)
      ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
          (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
              (fun (x : (Module.rank F E).ord.ToType) ↦
                adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
              i :
            IntermediateField F E))
        (↑i : WithTop (Module.rank F E).ord.ToType))
      ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
          (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
              (fun (x : (Module.rank F E).ord.ToType) ↦
                adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
              i :
            IntermediateField F E))
        (↑a : WithTop (Module.rank F E).ord.ToType))
⊢ LT.lt.{v} (α := IntermediateField F E)
    ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
        (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
            (fun (x : (Module.rank F E).ord.ToType) ↦
              adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
            i :
          IntermediateField F E))
      i)
    ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
        (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
            (fun (x : (Module.rank F E).ord.ToType) ↦
              adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
            i :
          IntermediateField F E))
      (↑a : WithTop (Module.rank F E).ord.ToType))

Tactic:
obtain ⟨i, rfl⟩ := ne_top_iff_exists.mp (h.trans <| coe_lt_top _).ne

Premises used: WithTop.coe_lt_top, WithTop.ne_top_iff_exists, Iff.mp, LT.lt.trans, rfl, LT.lt.ne
-- Module: Mathlib.FieldTheory.CardinalEmb
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
a i : (Module.rank F E).ord.ToType
h : (↑i : WithTop (Module.rank F E).ord.ToType) < (↑a : WithTop (Module.rank F E).ord.ToType)
⊢ LT.lt.{v} (α := IntermediateField F E)
    ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
        (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
            (fun (x : (Module.rank F E).ord.ToType) ↦
              adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
            i :
          IntermediateField F E))
      (↑i : WithTop (Module.rank F E).ord.ToType))
    ((fun (i : WithTop (Module.rank F E).ord.ToType) ↦
        (recTopCoe (C := fun (x : WithTop (Module.rank F E).ord.ToType) ↦ IntermediateField F E) ⊤
            (fun (x : (Module.rank F E).ord.ToType) ↦
              adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio x))
            i :
          IntermediateField F E))
      (↑a : WithTop (Module.rank F E).ord.ToType))

Tactic:
strictMono_filtration (coe_lt_coe.mp h)

Premises used: WithTop.coe_lt_coe, Field.Emb.Cardinal.strictMono_filtration, Iff.mp