-- Module: Mathlib.ModelTheory.PartialEquiv
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 : ι
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' := ⋯ :
                    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 (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 ⋯)
        (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)) ⋯))
        (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' := ⋯ :
                      OrderHom.{u_1, w} ι (L.Substructure M) } :
                    (a : ι) → L.Substructure M)
                  x :
                L.Substructure M))
          (fun (x x_1 : ι) (h : x ≤ x_1) ↦ inclusion ⋯) i)) =
    Embedding.comp (inclusion ⋯) (Equiv.toEmbedding (toEquiv ((S : (a : ι) → 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)))

Tactic:
rw [Equiv_isup_symm_inclusion]

Premises used: FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion