-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
a₁ a₂ : M ↪[L] N
h :
  ∃ (h_dom :
    Eq.{w + 1} (α := L.Substructure M)
      (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁))
      (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂))),
    ∀ (x : M)
      (h :
        Membership.mem (γ := L.Substructure M)
          (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) x),
      Eq.{w' + 1} (α := N)
        ((subtype (PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) :
              (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).cod) → N)
            ((PartialEquiv.toEquiv ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁) :
                  (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).dom) →
                    ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).cod)
                (Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := L.Substructure M)
                    (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) x)
                  x h) :
              ↥(PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁))) :
          N)
        ((subtype (PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂)) :
              (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).cod) → N)
            ((PartialEquiv.toEquiv ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂) :
                  (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).dom) →
                    ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).cod)
                (Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := L.Substructure M)
                    (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂)) x)
                  x ⋯) :
              ↥(PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂))) :
          N)
x : M
w :
  Eq.{w + 1} (α := L.Substructure M)
    (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁))
    (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂))
⊢ ∀ (x : M)
    (h :
      Membership.mem (γ := L.Substructure M)
        (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) x),
    Eq.{w' + 1} (α := N)
      ((subtype (PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) :
            (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).cod) → N)
          ((PartialEquiv.toEquiv ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁) :
                (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).dom) →
                  ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁).cod)
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := L.Substructure M)
                  (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁)) x)
                x h) :
            ↥(PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₁))) :
        N)
      ((subtype (PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂)) :
            (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).cod) → N)
          ((PartialEquiv.toEquiv ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂) :
                (a : ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).dom) →
                  ↥((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂).cod)
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := L.Substructure M)
                  (PartialEquiv.dom.{u, v, w, w'} (N := N) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂)) x)
                x ⋯) :
            ↥(PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂))) :
        N)

Tactic:
rcases h with ⟨_, H⟩