-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (goal)
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
ι : Type u_1
inst_2 : Preorder ι
inst_3 : Nonempty ι
inst_4 : IsDirectedOrder ι
S : ι →o M ≃ₚ[L] N
i : ι
⊢ Embedding.comp (N :=
      DirectLimit.{u_1, w', u, v} (L := L)
        (fun (i : ι) ↦
          ↥(({ toFun := fun (i : ι) ↦ cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) i), monotone' := ⋯ :
                    OrderHom.{u_1, w'} ι (L.Substructure N) } :
                  (a : ι) → L.Substructure N)
                i :
              L.Substructure N))
        fun (x x_1 : ι) (h : x ≤ x_1) ↦ inclusion ⋯)
      (Equiv.toEmbedding
        (Equiv_iSup
          { toFun := fun (i : ι) ↦ cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) i), monotone' := ⋯ :
            OrderHom.{u_1, w'} ι (L.Substructure N) }))
      (Embedding.comp
        (Equiv.toEmbedding
          (equiv_lift L ι (fun (i : ι) ↦ ↥(dom.{u, v, w, w'} (N := N) ((S : (a : ι) → M ≃ₚ[L] N) i)))
            (fun (x x_1 : ι) (hij : x ≤ x_1) ↦ inclusion ⋯)
            (fun (i : ι) ↦ ↥(cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) i)))
            (fun (x x_1 : ι) (hij : x ≤ x_1) ↦ inclusion ⋯) (fun (i : ι) ↦ toEquiv ((S : (a : ι) → M ≃ₚ[L] N) i)) ⋯))
        (Embedding.comp
          (Equiv.toEmbedding
            (Equiv.symm
              (Equiv_iSup
                { toFun := fun (i : ι) ↦ dom.{u, v, w, w'} (N := N) ((S : (a : ι) → M ≃ₚ[L] N) i), monotone' := ⋯ :
                  OrderHom.{u_1, w} ι (L.Substructure M) })))
          (inclusion ⋯))) =
    Embedding.comp (inclusion ⋯) (Equiv.toEmbedding (toEquiv ((S : (a : ι) → M ≃ₚ[L] N) i)))
have rw : Embedding.comp (N :=
    DirectLimit.{u_1, w', u, v} (L := L)
      (fun (i : ι) ↦
        ↥(({ toFun := fun (i : ι) ↦ cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) i), monotone' := sorry :
                  OrderHom.{u_1, w'} ι (L.Substructure N) } :
                (a : ι) → L.Substructure N)
              i :
            L.Substructure N))
      fun (x x_1 : ι) (h : x ≤ x_1) ↦ inclusion sorry)
    (Equiv.toEmbedding
      (Equiv_iSup
        { toFun := fun (i : ι) ↦ cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) i), monotone' := sorry :
          OrderHom.{u_1, w'} ι (L.Substructure N) }))
    (Embedding.comp (N :=
      DirectLimit.{u_1, w, u, v} (L := L) (fun (i : ι) ↦ ↥(dom.{u, v, w, w'} (N := N) ((S : (a : ι) → M ≃ₚ[L] N) i)))
        fun (x x_1 : ι) (hij : x ≤ x_1) ↦ inclusion sorry)
      (Equiv.toEmbedding
        (equiv_lift L ι (fun (i : ι) ↦ ↥(dom.{u, v, w, w'} (N := N) ((S : (a : ι) → M ≃ₚ[L] N) i)))
          (fun (x x_1 : ι) (hij : x ≤ x_1) ↦ inclusion sorry)
          (fun (i : ι) ↦ ↥(cod.{u, v, w, w'} (M := M) ((S : (a : ι) → M ≃ₚ[L] N) i)))
          (fun (x x_1 : ι) (hij : x ≤ x_1) ↦ inclusion sorry) (fun (i : ι) ↦ toEquiv ((S : (a : ι) → M ≃ₚ[L] N) i)) sorry))
      (of.{u_1, w, u, v} L ι
        (fun (x : ι) ↦
          ↥(({ toFun := fun (i : ι) ↦ dom.{u, v, w, w'} (N := N) ((S : (a : ι) → M ≃ₚ[L] N) i), monotone' := sorry :
                    OrderHom.{u_1, w} ι (L.Substructure M) } :
                  (a : ι) → L.Substructure M)
                x :
              L.Substructure M))
        (fun (x x_1 : ι) (h : x ≤ x_1) ↦ inclusion sorry) i)) =
  Embedding.comp (inclusion sorry) (Equiv.toEmbedding (toEquiv ((S : (a : ι) → M ≃ₚ[L] N) i)))
Tactic: rw [Equiv_isup_symm_inclusion]