-- Module: Mathlib.ModelTheory.DirectLimit
Goal:
L : Language
ι : Type v
inst : Preorder ι
inst_1 : Nonempty ι
inst_2 : IsDirectedOrder ι
M : Type u_1
inst_3 : L.Structure M
S : OrderHom.{v, u_1} ι (L.Substructure M)
i : ι
x : ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M)
a :
  Eq.{u_1 + 1} (α := ↥(iSup.{u_1, v + 1} (ι := ι) (⇑S : (a : ι) → L.Substructure M)))
    ((Equiv_iSup S :
          (a :
              DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion ⋯) →
            ↥(iSup (⇑S : (a : ι) → L.Substructure M)))
        ((Equiv.symm (Equiv_iSup S) :
            (a : ↥(iSup (⇑S : (a : ι) → L.Substructure M))) →
              DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion ⋯)
          ((Substructure.inclusion ⋯ :
              (a : ↥((S : (a : ι) → L.Substructure M) i)) → ↥(iSup (⇑S : (a : ι) → L.Substructure M)))
            x)) :
      ↥(iSup.{u_1, v + 1} (ι := ι) (⇑S : (a : ι) → L.Substructure M)))
    ((Equiv_iSup S :
          (a :
              DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion ⋯) →
            ↥(iSup (⇑S : (a : ι) → L.Substructure M)))
        (((of.{v, u_1, u_2, u_3} L ι (fun (x : ι) ↦ ↥((S : (a : ι) → L.Substructure M) x : L.Substructure M))
                (fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯) i :
              ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M) ↪[L]
                DirectLimit.{v, u_1, u_2, u_3} (L := L)
                  (fun (x : ι) ↦ ↥((S : (a : ι) → L.Substructure M) x : L.Substructure M))
                  fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯) :
            (a : ↥((S : (a : ι) → L.Substructure M) i)) →
              DirectLimit (fun (x : ι) ↦ ↥((S : (a : ι) → L.Substructure M) x)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion ⋯)
          x) :
      ↥(iSup.{u_1, v + 1} (ι := ι) (⇑S : (a : ι) → L.Substructure M)))
⊢ Eq (α :=
    DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
      fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯)
    ((Equiv.symm (Equiv_iSup S) :
          (a : ↥(iSup (⇑S : (a : ι) → L.Substructure M))) →
            DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
              Substructure.inclusion ⋯)
        ((Substructure.inclusion ⋯ :
            (a : ↥((S : (a : ι) → L.Substructure M) i)) → ↥(iSup (⇑S : (a : ι) → L.Substructure M)))
          x) :
      DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M))
        fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯)
    (((of.{v, u_1, u_2, u_3} L ι (fun (x : ι) ↦ ↥((S : (a : ι) → L.Substructure M) x : L.Substructure M))
              (fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯) i :
            ↥((S : (a : ι) → L.Substructure M) i : L.Substructure M) ↪[L]
              DirectLimit.{v, u_1, u_2, u_3} (L := L)
                (fun (x : ι) ↦ ↥((S : (a : ι) → L.Substructure M) x : L.Substructure M)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion ⋯) :
          (a : ↥((S : (a : ι) → L.Substructure M) i)) →
            DirectLimit (fun (x : ι) ↦ ↥((S : (a : ι) → L.Substructure M) x)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
              Substructure.inclusion ⋯)
        x :
      DirectLimit.{v, u_1, u_2, u_3} (L := L) (fun (x : ι) ↦ ↥((S : (a : ι) → L.Substructure M) x : L.Substructure M))
        fun (x x_1 : ι) (h : x ≤ x_1) ↦ Substructure.inclusion ⋯)

Tactic:
apply (Equiv_iSup S).injective

Premises used: FirstOrder.Language.Equiv.injective, FirstOrder.Language.DirectLimit.Equiv_iSup