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
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:
exact strictMono_filtration (coe_lt_coe.mp h)

Premises used: WithTop.coe_lt_coe, Field.Emb.Cardinal.strictMono_filtration, Iff.mp
-- 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
inst_4 : Algebra.IsSeparable F E
i : (Module.rank F E).ord.ToType
⊢ Algebra.IsSeparable.{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:
have := Algebra.isSeparable_tower_top_of_isSeparable F (E⟮<i⟯) E
  have : IsScalarTower (E⟮<i⟯) (E⟮<i⟯⟮b (φ i)⟯) E := .of_algebraMap_eq' rfl
  Algebra.isSeparable_tower_bot_of_isSeparable _ _ E

Premises used: Function.comp, Membership.mem, Subtype, Algebra.isSeparable_tower_top_of_isSeparable, Field.Emb.Cardinal.wellOrderedBasis, IsScalarTower.of_algebraMap_eq', Algebra.isSeparable_tower_bot_of_isSeparable, IntermediateField.adjoin, Set.image, Singleton.singleton, 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
inst_4 : Algebra.IsSeparable F E
i : (Module.rank F E).ord.ToType
rw :
  1 <
    finrank.{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)⟯
⊢ 2 ≤
    #(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:
rw [← Nat.cast_ofNat, ← toNat_le_iff_le_of_lt_aleph0 natCast_lt_aleph0 (deg_lt_aleph0 i),
    toNat_natCast, ← Nat.card, ← finSepDegree, finSepDegree_eq_finrank_of_isSeparable,
    Nat.succ_le_iff]

Premises used: Nat.cast_ofNat, Field.finSepDegree, Nat.card, Cardinal.natCast_lt_aleph0, Field.finSepDegree_eq_finrank_of_isSeparable, Field.Emb.Cardinal.deg_lt_aleph0, Cardinal.toNat_le_iff_le_of_lt_aleph0, Cardinal.toNat_natCast, Nat.succ_le_iff
-- 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
inst_4 : Algebra.IsSeparable F E
i : (Module.rank F E).ord.ToType
by_contra! :
  ∀
    (this :
      finrank.{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)⟯ ≤
        1),
    False
⊢ 1 <
    finrank.{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:
by_contra!
-- 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
inst_4 : Algebra.IsSeparable F E
i : (Module.rank F E).ord.ToType
this :
  finrank.{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)⟯ ≤
    1
obtain :
  ∀ (x : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i)))
    (hx :
      Eq (α := E)
        ((AlgHom.toRingHom (Algebra.ofId (↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) E) :
              (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) → E)
            x :
          E)
        ((b : (a : (Module.rank F E).ord.ToType) → E) (φ i) : E)),
    False
⊢ False

Tactic:
obtain ⟨x, hx⟩ := finrank_adjoin_simple_eq_one_iff.mp (this.antisymm Module.finrank_pos)

Premises used: LE.le.antisymm, Iff.mp, IntermediateField.finrank_adjoin_simple_eq_one_iff, Module.finrank_pos
-- 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
inst_4 : Algebra.IsSeparable F E
i : (Module.rank F E).ord.ToType
this :
  finrank.{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)⟯ ≤
    1
x : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
hx :
  Eq (α := E)
    ((AlgHom.toRingHom (Algebra.ofId (↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) E) :
          (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) → E)
        x :
      E)
    ((b : (a : (Module.rank F E).ord.ToType) → E) (φ i) : E)
⊢ False

Tactic:
(isLeast_leastExt i).1 (hx ▸ ?_)

Premises used: Field.Emb.Cardinal.isLeast_leastExt, Eq.rec, And.left
-- 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
inst_4 : Algebra.IsSeparable F E
i : (Module.rank F E).ord.ToType
this :
  finrank.{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)⟯ ≤
    1
x : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
hx :
  Eq (α := E)
    ((AlgHom.toRingHom (Algebra.ofId (↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) E) :
          (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) → E)
        x :
      E)
    ((b : (a : (Module.rank F E).ord.ToType) → E) (φ i) : E)
refine :
  Membership.mem (α := E) (γ := IntermediateField F E)
    (adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
    ((AlgHom.toRingHom (Algebra.ofId (↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) E) :
          (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) → E)
        x :
      E)
⊢ False

Tactic:
refine (isLeast_leastExt i).1 (hx ▸ ?_)

Premises used: Field.Emb.Cardinal.isLeast_leastExt, Eq.rec, And.left
-- 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
inst_4 : Algebra.IsSeparable F E
i : (Module.rank F E).ord.ToType
this :
  finrank.{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)⟯ ≤
    1
x : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
hx :
  Eq (α := E)
    ((AlgHom.toRingHom (Algebra.ofId (↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) E) :
          (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) → E)
        x :
      E)
    ((b : (a : (Module.rank F E).ord.ToType) → E) (φ i) : E)
⊢ Membership.mem (α := E) (γ := IntermediateField F E)
    (adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
    ((AlgHom.toRingHom (Algebra.ofId (↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) E) :
          (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) → E)
        x :
      E)

Tactic:
x.2

Premises used: Set.Mem, Subtype.property
-- 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
inst_4 : Algebra.IsSeparable F E
i : (Module.rank F E).ord.ToType
this :
  finrank.{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)⟯ ≤
    1
x : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
hx :
  Eq (α := E)
    ((AlgHom.toRingHom (Algebra.ofId (↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) E) :
          (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) → E)
        x :
      E)
    ((b : (a : (Module.rank F E).ord.ToType) → E) (φ i) : E)
⊢ Membership.mem (α := E) (γ := IntermediateField F E)
    (adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))
    ((AlgHom.toRingHom (Algebra.ofId (↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) E) :
          (a : ↥(adjoin F ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio i))) → E)
        x :
      E)

Tactic:
exact x.2

Premises used: Subtype.property
-- 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
rw rw₁ :
  Eq.{v + 1} (α := IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤ : IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤ : IntermediateField F E)
⊢ Eq.{v + 1} (α := IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) (⊤⁺) : IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤ : IntermediateField F E)

Tactic:
rw [succ_top]

Premises used: Order.succ_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 : WithTop (Module.rank F E).ord.ToType
f :
  ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) (i⁺) :
        IntermediateField F E) →ₐ[F]
    Ē
top :
  ∀
    (f :
      ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) (⊤⁺) :
            IntermediateField F E) →ₐ[F]
        Ē),
    ((equivSucc ⊤ :
            (a : ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) (⊤⁺)) →ₐ[F] Ē) →
              (↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤) →ₐ[F] Ē) ×
                factor ⊤)
          f).1 =
      embFunctor F E ⋯ f
coe :
  ∀ (a : (Module.rank F E).ord.ToType)
    (f :
      ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
              ((↑a : WithTop (Module.rank F E).ord.ToType)⁺) :
            IntermediateField F E) →ₐ[F]
        Ē),
    ((equivSucc (↑a : WithTop (Module.rank F E).ord.ToType) :
            (a_1 :
                ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                      ((↑a : WithTop (Module.rank F E).ord.ToType)⁺)) →ₐ[F]
                  Ē) →
              (↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                      (↑a : WithTop (Module.rank F E).ord.ToType)) →ₐ[F]
                  Ē) ×
                factor (↑a : WithTop (Module.rank F E).ord.ToType))
          f).1 =
      embFunctor F E ⋯ f
⊢ ((equivSucc i :
          (a : ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) (i⁺)) →ₐ[F] Ē) →
            (↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i) →ₐ[F] Ē) × factor i)
        f).1 =
    embFunctor F E ⋯ f

Tactic:
cases i
-- 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
f :
  ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) (⊤⁺) :
        IntermediateField F E) →ₐ[F]
    Ē
⊢ ((equivSucc ⊤ :
          (a : ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) (⊤⁺)) →ₐ[F] Ē) →
            (↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤) →ₐ[F] Ē) × factor ⊤)
        f).1 =
    embFunctor F E ⋯ f

Tactic:
rfl

Premises used: IntermediateField.copy, AlgEquiv.toAlgHom, Set.Mem, Subalgebra.inclusion, Field.Emb.Cardinal.embFunctor, AlgHom.comp, WithTop.recTopCoe, Subalgebra.copy, 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
a : (Module.rank F E).ord.ToType
f :
  ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
          ((↑a : WithTop (Module.rank F E).ord.ToType)⁺) :
        IntermediateField F E) →ₐ[F]
    Ē
⊢ ((equivSucc (↑a : WithTop (Module.rank F E).ord.ToType) :
          (a_1 :
              ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                    ((↑a : WithTop (Module.rank F E).ord.ToType)⁺)) →ₐ[F]
                Ē) →
            (↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                    (↑a : WithTop (Module.rank F E).ord.ToType)) →ₐ[F]
                Ē) ×
              factor (↑a : WithTop (Module.rank F E).ord.ToType))
        f).1 =
    embFunctor F E ⋯ f

Tactic:
succEquiv_coherence _ f

Premises used: Set.Mem, Field.Emb.Cardinal.succEquiv_coherence, IntermediateField.adjoin, Field.Emb.Cardinal.embFunctor, WithTop.recTopCoe
-- 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
f :
  ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) (⊤⁺) :
        IntermediateField F E) →ₐ[F]
    Ē
⊢ ((equivSucc ⊤ :
          (a : ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) (⊤⁺)) →ₐ[F] Ē) →
            (↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤) →ₐ[F] Ē) × factor ⊤)
        f).1 =
    embFunctor F E ⋯ f

Tactic:
exacts [rfl, succEquiv_coherence _ f]

Premises used: Field.Emb.Cardinal.succEquiv_coherence, 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 : WithTop (Module.rank F E).ord.ToType
⊢ Directed (fun (x1 x2 : IntermediateField F E) ↦ x1 ≤ x2) fun (j : (↑(Iio i) : Type v)) ↦
    (filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
      (↑j : WithTop (Module.rank F E).ord.ToType)

Tactic:
(filtration.monotone.comp <| Subtype.mono_coe _).directed_le

Premises used: OrderEmbedding.monotone, Monotone.comp, Subtype.mono_coe, Field.Emb.Cardinal.filtration, Monotone.directed_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
i : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
top :
  ∀ (hi : IsSuccPrelimit.{v} (α := WithTop (Module.rank F E).ord.ToType) ⊤),
    Eq.{v + 1} (α := IntermediateField F E)
      (⨆ (j : (↑(Iio ⊤) : Type v)),
          (filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
            (↑j : WithTop (Module.rank F E).ord.ToType) :
        IntermediateField F E)
      ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤ : IntermediateField F E)
coe :
  ∀ (a : (Module.rank F E).ord.ToType) (hi : IsSuccPrelimit (↑a : WithTop (Module.rank F E).ord.ToType)),
    Eq (α := IntermediateField F E)
      (⨆ (j : (↑(Iio (↑a : WithTop (Module.rank F E).ord.ToType)) : Type v)),
          (filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
            (↑j : WithTop (Module.rank F E).ord.ToType) :
        IntermediateField F E)
      ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
          (↑a : WithTop (Module.rank F E).ord.ToType) :
        IntermediateField F E)
⊢ Eq (α := IntermediateField F E)
    (⨆ (j : (↑(Iio i) : Type v)),
        (filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
          (↑j : WithTop (Module.rank F E).ord.ToType) :
      IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i : IntermediateField F E)

Tactic:
cases i
-- 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
hi : IsSuccPrelimit.{v} (α := WithTop (Module.rank F E).ord.ToType) ⊤
top :
  Eq.{v + 1} (α := IntermediateField F E)
    (⨆ (i : (Module.rank F E).ord.ToType),
        (filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
          (↑i : WithTop (Module.rank F E).ord.ToType) :
      IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤ : IntermediateField F E)
⊢ Eq.{v + 1} (α := IntermediateField F E)
    (⨆ (j : (↑(Iio ⊤) : Type v)),
        (filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
          (↑j : WithTop (Module.rank F E).ord.ToType) :
      IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤ : IntermediateField F E)

Tactic:
rw [← range_coe, iSup_range']

Premises used: iSup_range', WithTop.range_coe
-- 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
hi : IsSuccPrelimit.{v} (α := WithTop (Module.rank F E).ord.ToType) ⊤
⊢ Eq.{v + 1} (α := IntermediateField F E)
    (⨆ (i : (Module.rank F E).ord.ToType),
        (filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
          (↑i : WithTop (Module.rank F E).ord.ToType) :
      IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤ : IntermediateField F E)

Tactic:
iSup_adjoin_eq_top

Premises used: IntermediateField.copy, IntermediateField.adjoin, Field.Emb.Cardinal.iSup_adjoin_eq_top, WithTop.recTopCoe
-- 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
hi : IsSuccPrelimit.{v} (α := WithTop (Module.rank F E).ord.ToType) ⊤
⊢ Eq.{v + 1} (α := IntermediateField F E)
    (⨆ (i : (Module.rank F E).ord.ToType),
        (filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
          (↑i : WithTop (Module.rank F E).ord.ToType) :
      IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤ : IntermediateField F E)

Tactic:
exact iSup_adjoin_eq_top

Premises used: Field.Emb.Cardinal.iSup_adjoin_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
a : (Module.rank F E).ord.ToType
hi : IsSuccPrelimit (↑a : WithTop (Module.rank F E).ord.ToType)
⊢ Eq (α := IntermediateField F E)
    (⨆ (j : (↑(Iio (↑a : WithTop (Module.rank F E).ord.ToType)) : Type v)),
        (filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
          (↑j : WithTop (Module.rank F E).ord.ToType) :
      IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
        (↑a : WithTop (Module.rank F E).ord.ToType) :
      IntermediateField F E)

Tactic:
(iSup_le fun j ↦ filtration.monotone (mem_Iio.1 j.2).le).antisymm (adjoin_le_iff.2 ?_)

Premises used: Iff.mpr, OrderEmbedding.monotone, Set.mem_Iio, IntermediateField.adjoin_le_iff, LE.le.antisymm, LT.lt.le, Iff.mp, iSup_le, Field.Emb.Cardinal.filtration
-- 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 : (Module.rank F E).ord.ToType
hi : IsSuccPrelimit (↑a : WithTop (Module.rank F E).ord.ToType)
coe :
  (⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio a ⊆
    (↑(⨆ (j : (↑(Iio (↑a : WithTop (Module.rank F E).ord.ToType)) : Type v)),
          (filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
            (↑j : WithTop (Module.rank F E).ord.ToType)) :
      Set E)
⊢ Eq (α := IntermediateField F E)
    (⨆ (j : (↑(Iio (↑a : WithTop (Module.rank F E).ord.ToType)) : Type v)),
        (filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
          (↑j : WithTop (Module.rank F E).ord.ToType) :
      IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
        (↑a : WithTop (Module.rank F E).ord.ToType) :
      IntermediateField F E)

Tactic:
refine (iSup_le fun j ↦ filtration.monotone (mem_Iio.1 j.2).le).antisymm (adjoin_le_iff.2 ?_)

Premises used: OrderEmbedding.monotone, Set.mem_Iio, LE.le.antisymm, LT.lt.le, Iff.mp, iSup_le, Field.Emb.Cardinal.filtration
-- 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 : (Module.rank F E).ord.ToType
hi : IsSuccPrelimit (↑a : WithTop (Module.rank F E).ord.ToType)
j : (Module.rank F E).ord.ToType
hj : j ∈ Iio a
⊢ ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ) j ∈
    (↑(⨆ (j : (↑(Iio (↑a : WithTop (Module.rank F E).ord.ToType)) : Type v)),
          (filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
            (↑j : WithTop (Module.rank F E).ord.ToType)) :
      Set E)

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

Premises used: le_iSup