awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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))
        ⊤)
⊢ 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)
have 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))
Tactic: cases j
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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 < ⊤
⊢ 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))
      ⊤)
have 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))
      ⊤)
Tactic: obtain ⟨i, rfl⟩ := ne_top_iff_exists.mp h.ne
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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)
⊢ 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))
have 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))
Tactic: obtain ⟨i, rfl⟩ := ne_top_iff_exists.mp (h.trans <| coe_lt_top _).ne
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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
⊢ 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)⟯)
have 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)⟯
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]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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
⊢ 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)⟯
have 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
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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
⊢ False
have 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
Tactic: obtain ⟨x, hx⟩ := finrank_adjoin_simple_eq_one_iff.mp (this.antisymm Module.finrank_pos)
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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
have 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)
Tactic: refine (isLeast_leastExt i).1 (hx ▸ ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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
⊢ 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)
have 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)
Tactic: rw [succ_top]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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]
    Ē
⊢ ((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
have 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 sorry f
Tactic: cases i
Cleared hypotheses: i, f
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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
⊢ ((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
have 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 sorry f
Tactic: cases i
Cleared hypotheses: i, f
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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
⊢ 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)
have 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)
Tactic: cases i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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)
⊢ 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)
have 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)
Tactic: cases i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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)
    (⨆ (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)
have 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)
Tactic: rw [← range_coe, iSup_range']
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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)
have 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)
Tactic: refine (iSup_le fun j ↦ filtration.monotone (mem_Iio.1 j.2).le).antisymm (adjoin_le_iff.2 ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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)
have coe : Membership.mem (γ := Set E) ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio (j⁺))
  (((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ) j)
Tactic: refine le_iSup (α := IntermediateField F E) _ ⟨j⁺, ?_⟩ (subset_adjoin F _ ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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
coe :
  Membership.mem (γ := Set E) ((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ '' Iio (j⁺))
    (((⇑b : (a : (Module.rank F E).ord.ToType) → E) ∘ φ) j)
⊢ ((⇑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)
have coe₁ : (↑j : WithTop (Module.rank F E).ord.ToType)⁺ ∈ Iio (↑a : WithTop (Module.rank F E).ord.ToType)
Tactic: refine le_iSup (α := IntermediateField F E) _ ⟨j⁺, ?_⟩ (subset_adjoin F _ ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
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_1 : IsSuccPrelimit i
hi : ¬Nonempty.{v + 1} (↑(Iio i) : Type v)
⊢ Eq (α := IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i : IntermediateField F E)
    (⊥ : IntermediateField F E)
have top : ∀ (hi : IsSuccPrelimit.{v} (α := WithTop (Module.rank F E).ord.ToType) ⊤) (hi : ¬Nonempty.{v + 1} (↑(Iio ⊤) : Type v)),
  Eq.{v + 1} (α := IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤ : IntermediateField F E)
    (⊥ : IntermediateField F E)
Tactic: cases i
Cleared hypotheses: i, hi_1, hi