-- Lean 4 proof step from Mathlib.ModelTheory.DirectLimit (goal)
Goal:
L : Language
ι : Type v
inst : Preorder ι
G : ι → Type w
inst_1 : (i : ι) → Structure.{u_2, u_3, w} L (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst_2 : Nonempty ι
inst_3 : IsDirectedOrder ι
M : Type u_1
inst_4 : L.Structure M
S : OrderHom.{v, u_1} ι (L.Substructure M)
liftInclusion_in_sup :
  ∀
    (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 ⋯),
    Membership.mem.{u_1, u_1} (α := M) (γ := L.Substructure M) (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i)
      ((liftInclusion S :
            (a :
                DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                  Substructure.inclusion ⋯) →
              M)
          x :
        M)
F : (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 ⋯) ↪[L]
  ↥(⨆ (i : ι), (S : (a : ι) → L.Substructure M) i) :=
  Embedding.codRestrict (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i) (liftInclusion S) liftInclusion_in_sup
m : M
hm_1 : Membership.mem (γ := L.Substructure M) (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i) m
hm :
  ∃ (y :
    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 ⋯),
    (Embedding.toHom (liftInclusion S) :
          (a :
              DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion ⋯) →
            M)
        y =
      m
⊢ ∃ (a :
    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 ⋯),
    (F :
          (a :
              DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion ⋯) →
            ↥(⨆ (i : ι), (S : (a : ι) → L.Substructure M) i))
        a =
      Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := L.Substructure M) (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i) x) m hm_1
have rcases : ∀
  (a :
    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 sorry),
  (Embedding.toHom (liftInclusion S) :
          (a :
              DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                Substructure.inclusion sorry) →
            M)
        a =
      m →
    ∃ (a :
      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 sorry),
      (F :
            (a :
                DirectLimit (fun (i : ι) ↦ ↥((S : (a : ι) → L.Substructure M) i)) fun (x x_1 : ι) (h : x ≤ x_1) ↦
                  Substructure.inclusion sorry) →
              ↥(⨆ (i : ι), (S : (a : ι) → L.Substructure M) i))
          a =
        Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := L.Substructure M) (⨆ (i : ι), (S : (a : ι) → L.Substructure M) i) x) m hm_1
Tactic: rcases hm with ⟨a, _⟩
Cleared hypotheses: hm