-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
cod : L.Substructure N
toEquiv : Equiv.{u, v, w, w'} L ↥{ carrier := Set.univ, fun_mem := ⋯ } ↥cod
x : M
refl :
  ∀ (h : x ∈ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom),
    Eq (α := N)
      (((PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod.subtype :
            (a : ↥(PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod) → N)
          (((PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.toEquiv :
                (a : ↥(PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom) →
                  ↥(PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom) x h) :
            ↥(PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod) :
        N)
      (({ dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                  M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := toEquiv }.cod) → N)
          (({ dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                    M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := toEquiv }.dom) →
                  ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := toEquiv }.cod)
              (Subtype.mk (p := fun (x : M) ↦
                x ∈
                  { dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                      M ≃ₚ[L] N }.dom)
                x ⋯) :
            ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                  M ≃ₚ[L] N }.cod) :
        N)
⊢ ∀ (h : x ∈ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom),
    Eq (α := N)
      (((PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod.subtype :
            (a : ↥(PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod) → N)
          (((PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.toEquiv :
                (a : ↥(PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom) →
                  ↥(PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom) x h) :
            ↥(PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod) :
        N)
      (({ dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                  M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := toEquiv }.cod) → N)
          (({ dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                    M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := toEquiv }.dom) →
                  ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod, toEquiv := toEquiv }.cod)
              (Subtype.mk (p := fun (x : M) ↦
                x ∈
                  { dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                      M ≃ₚ[L] N }.dom)
                x ⋯) :
            ↥{ dom := { carrier := Set.univ, fun_mem := ⋯ : L.Substructure M }, cod := cod, toEquiv := toEquiv :
                  M ≃ₚ[L] N }.cod) :
        N)

Tactic:
_