-- 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
f :
  ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i : IntermediateField F E) →ₐ[F] Ē
h : Nonempty.{v + 1} (↑(Iio i) : Type v)
x : E
hx_1 :
  Membership.mem (γ := Subalgebra F E)
    (toSubalgebra ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i)) x
hx :
  ∃ (i_1 : (↑(Iio i) : Type v)),
    x ∈
      (↑((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
              (↑i_1 : WithTop (Module.rank F E).ord.ToType) :
            IntermediateField F E) :
        Set E)
⊢ Eq (α := Ē)
    (((fun
                (f :
                  (↑(limit (F := fun (j : WithTop (Module.rank F E).ord.ToType) ↦
                        ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) j :
                              IntermediateField F E) →ₐ[F]
                          Ē)
                        (embFunctor F E) i) :
                    Type v)) ↦
              Subalgebra.iSupLift
                (fun (x : (↑(Iio i) : Type v)) ↦
                  toSubalgebra
                    ((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) :
                          IntermediateField F E))
                      x))
                ⋯
                (↑f :
                  (l : (↑(Iio i) : Type v)) →
                    ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                          (↑l : WithTop (Module.rank F E).ord.ToType)) →ₐ[F]
                      Ē)
                ⋯ (toSubalgebra ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i))
                ⋯)
            ((fun
                  (f :
                    ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i :
                          IntermediateField F E) →ₐ[F]
                      Ē) ↦
                (Subtype.mk (p :=
                    fun
                      (x :
                        (l : (↑(Iio i) : Type v)) →
                          ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                                  (↑l : WithTop (Module.rank F E).ord.ToType) :
                                IntermediateField F E) →ₐ[F]
                            Ē) ↦
                    Membership.mem (γ :=
                      Set
                        ((l : (↑(Iio i) : Type v)) →
                          ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                                  (↑l : WithTop (Module.rank F E).ord.ToType) :
                                IntermediateField F E) →ₐ[F]
                            Ē))
                      (limit (F := fun (j : WithTop (Module.rank F E).ord.ToType) ↦
                        ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) j :
                              IntermediateField F E) →ₐ[F]
                          Ē)
                        (embFunctor F E) i)
                      x)
                    (fun (j : (↑(Iio i) : Type v)) ↦ embFunctor F E ⋯ f) ⋯ :
                  { x :
                    (l : (↑(Iio i) : Type v)) →
                      ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                              (↑l : WithTop (Module.rank F E).ord.ToType) :
                            IntermediateField F E) →ₐ[F]
                        Ē //
                    Membership.mem (γ :=
                      Set
                        ((l : (↑(Iio i) : Type v)) →
                          ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                                  (↑l : WithTop (Module.rank F E).ord.ToType) :
                                IntermediateField F E) →ₐ[F]
                            Ē))
                      (limit (F := fun (j : WithTop (Module.rank F E).ord.ToType) ↦
                        ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) j :
                              IntermediateField F E) →ₐ[F]
                          Ē)
                        (embFunctor F E) i)
                      x }))
              f) :
          (a : ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i).toSubalgebra) → Ē)
        (Subtype.mk (p := fun (x : E) ↦
          Membership.mem (γ := Subalgebra F E)
            (toSubalgebra ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i)) x)
          x hx_1) :
      Ē)
    ((f : (a : ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i).toSubalgebra) → Ē)
        (Subtype.mk (p := fun (x : E) ↦
          Membership.mem (γ := Subalgebra F E)
            (toSubalgebra ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i)) x)
          x hx_1) :
      Ē)
have pos : Eq (α := Ē)
  (((↑((fun
                    (f :
                      ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i :
                            IntermediateField F E) →ₐ[F]
                        Ē) ↦
                  (Subtype.mk (p :=
                      fun
                        (x :
                          (l : (↑(Iio i) : Type v)) →
                            ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                                    (↑l : WithTop (Module.rank F E).ord.ToType) :
                                  IntermediateField F E) →ₐ[F]
                              Ē) ↦
                      Membership.mem (γ :=
                        Set
                          ((l : (↑(Iio i) : Type v)) →
                            ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                                    (↑l : WithTop (Module.rank F E).ord.ToType) :
                                  IntermediateField F E) →ₐ[F]
                              Ē))
                        (limit (F := fun (j : WithTop (Module.rank F E).ord.ToType) ↦
                          ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) j :
                                IntermediateField F E) →ₐ[F]
                            Ē)
                          (embFunctor F E) i)
                        x)
                      (fun (j : (↑(Iio i) : Type v)) ↦ embFunctor F E sorry f) sorry :
                    { x :
                      (l : (↑(Iio i) : Type v)) →
                        ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                                (↑l : WithTop (Module.rank F E).ord.ToType) :
                              IntermediateField F E) →ₐ[F]
                          Ē //
                      Membership.mem (γ :=
                        Set
                          ((l : (↑(Iio i) : Type v)) →
                            ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                                    (↑l : WithTop (Module.rank F E).ord.ToType) :
                                  IntermediateField F E) →ₐ[F]
                              Ē))
                        (limit (F := fun (j : WithTop (Module.rank F E).ord.ToType) ↦
                          ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) j :
                                IntermediateField F E) →ₐ[F]
                            Ē)
                          (embFunctor F E) i)
                        x }))
                f) :
            (l : (↑(Iio i) : Type v)) →
              ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                    (↑l : WithTop (Module.rank F E).ord.ToType)) →ₐ[F]
                Ē)
          (hx.choose (p := fun (i_1 : (↑(Iio i) : Type v)) ↦
            x ∈
              (↑((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                      (↑i_1 : WithTop (Module.rank F E).ord.ToType) :
                    IntermediateField F E) :
                Set E))) :
        (a :
            ↥((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))
                  hx.choose).toSubalgebra) →
          Ē)
      (Subtype.mk (p := fun (x_1 : E) ↦
        Membership.mem (γ := Subalgebra F E)
          (toSubalgebra
            ((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) :
                  IntermediateField F E))
              (hx.choose (p := fun (i_1 : (↑(Iio i) : Type v)) ↦
                x ∈
                  (↑((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                          (↑i_1 : WithTop (Module.rank F E).ord.ToType) :
                        IntermediateField F E) :
                    Set E)))))
          x_1)
        (↑(Subtype.mk (p := fun (x : E) ↦
              Membership.mem (γ := Subalgebra F E)
                (toSubalgebra ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i)) x)
              x hx_1) :
          E)
        sorry) :
    Ē)
  ((f : (a : ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i).toSubalgebra) → Ē)
      (Subtype.mk (p := fun (x : E) ↦
        Membership.mem (γ := Subalgebra F E)
          (toSubalgebra ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i)) x)
        x hx_1) :
    Ē)
Tactic: rw [Subalgebra.iSupLift_of_mem _ _ (by exact hx.choose_spec)]