-- Lean 4 proof step from Mathlib.ModelTheory.PartialEquiv (hypothesis)
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₂))
⊢ Eq.{w' + 1} (α := N) ((a₁ : (a : M) → N) x : N) ((a₂ : (a : M) → N) x : N)
have H : ∀ (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 sorry) :
          ↥(PartialEquiv.cod.{u, v, w, w'} (M := M) ((fun (f : M ↪[L] N) ↦ f.toPartialEquiv) a₂))) :
      N)
Tactic: rcases h with ⟨_, H⟩
Cleared hypotheses: h