-- 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] Ē
pos :
  ∀ (h : Nonempty.{v + 1} (↑(Iio i) : Type v)),
    (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) =
      f
⊢ (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)) ↦
        (if h : Nonempty.{v + 1} (↑(Iio i) : Type v) then
            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)) ⋯
          else
            AlgHom.comp (Algebra.ofId F Ē)
              (↑(AlgEquiv.trans (equivOfEq ⋯) (botEquiv F E)) :
                ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i) →ₐ[F] F) :
          ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i :
                IntermediateField F E) →ₐ[F]
            Ē))
      ((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) =
    f
have neg : ∀ (h : ¬Nonempty.{v + 1} (↑(Iio i) : Type v)),
  (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)) ↦
        (AlgHom.comp (Algebra.ofId F Ē)
            (↑(AlgEquiv.trans (equivOfEq sorry) (botEquiv F E)) :
              ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i) →ₐ[F] F) :
          ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i :
                IntermediateField F E) →ₐ[F]
            Ē))
      ((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) =
    f
Tactic: split_ifs with h