-- 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 :
  (↑(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)
j : (↑(Iio i) : Type v)
this : Nonempty.{v + 1} (↑(Iio i) : Type v)
⊢ (↑((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 }))
            ((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]
                    Ē))
              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]
            Ē)
      j =
    (↑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]
            Ē)
      j
have simp_rw : embFunctor F E sorry
    (Subalgebra.iSupLift
      (fun (x : (↑(Iio i) : Type v)) ↦
        toSubalgebra
          ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
            (↑x : WithTop (Module.rank F E).ord.ToType)))
      sorry
      (↑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]
            Ē)
      sorry (toSubalgebra ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i)) sorry) =
  (↑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]
          Ē)
    j
Tactic: simp_rw [dif_pos this]