awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    Eq (α := N)
      (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod) → N)
          (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) →
                  ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x
                h) :
            ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
        N)
      ((g.cod.subtype : (a : ↥g.cod) → N)
          ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x ⋯) : ↥g.cod) :
        N)
refl : { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } ≤ g
refl₁ : g ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f }
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } = g

Tactic:
apply le_antisymm

Premises used: _private.0.FirstOrder.Language.PartialEquiv.le_antisymm
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    Eq (α := N)
      (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod) → N)
          (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) →
                  ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x
                h) :
            ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
        N)
      ((g.cod.subtype : (a : ↥g.cod) → N)
          ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x ⋯) : ↥g.cod) :
        N)
h₁ :
  g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) =
    { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
      { dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding
⊢ ∃ (h : { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom ≤ g.dom),
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion h)) =
      { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
        { dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding

Tactic:
use le_rfl

Premises used: le_rfl
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    Eq (α := N)
      (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod) → N)
          (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) →
                  ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x
                h) :
            ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
        N)
      ((g.cod.subtype : (a : ↥g.cod) → N)
          ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x ⋯) : ↥g.cod) :
        N)
h₁ :
  ∀ (x : M) (hx : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    Eq.{w' + 1} (α := N)
      ((g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) :
            (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) → N)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x hx) :
        N)
      (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
              { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv.toEmbedding :
            (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) → N)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x hx) :
        N)
⊢ g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) =
    { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
      { dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    Eq (α := N)
      (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod) → N)
          (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) →
                  ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x
                h) :
            ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
        N)
      ((g.cod.subtype : (a : ↥g.cod) → N)
          ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x ⋯) : ↥g.cod) :
        N)
h₁ :
  { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
      ({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv.toEmbedding.comp (inclusion ⋯)) =
    g.cod.subtype.comp g.toEquiv.toEmbedding
⊢ ∃ (h : g.dom ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv.toEmbedding.comp (inclusion h)) =
      g.cod.subtype.comp g.toEquiv.toEmbedding

Tactic:
use le_rfl

Premises used: le_rfl
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    Eq (α := N)
      (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod) → N)
          (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) →
                  ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x
                h) :
            ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
        N)
      ((g.cod.subtype : (a : ↥g.cod) → N)
          ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x ⋯) : ↥g.cod) :
        N)
h₁ :
  ∀ (x : M) (hx : x ∈ g.dom),
    Eq.{w' + 1} (α := N)
      (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
              ({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv.toEmbedding.comp (inclusion ⋯)) :
            (a : ↥g.dom) → N)
          (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x hx) :
        N)
      ((g.cod.subtype.comp g.toEquiv.toEmbedding : (a : ↥g.dom) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x hx) :
        N)
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
      ({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv.toEmbedding.comp (inclusion ⋯)) =
    g.cod.subtype.comp g.toEquiv.toEmbedding

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    Eq (α := N)
      (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod) → N)
          (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) →
                  ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x
                h) :
            ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
        N)
      ((g.cod.subtype : (a : ↥g.cod) → N)
          ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x ⋯) : ↥g.cod) :
        N)
x : M
hx : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom
⊢ Eq.{w' + 1} (α := N)
    ((g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) :
          (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) → N)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x hx) :
      N)
    (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
            { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv.toEmbedding :
          (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) → N)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x hx) :
      N)

Tactic:
(h x hx).symm

Premises used: Eq.symm
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    Eq (α := N)
      (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod) → N)
          (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) →
                  ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x
                h) :
            ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
        N)
      ((g.cod.subtype : (a : ↥g.cod) → N)
          ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x ⋯) : ↥g.cod) :
        N)
x : M
hx : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom
⊢ Eq.{w' + 1} (α := N)
    ((g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) :
          (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) → N)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x hx) :
      N)
    (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
            { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv.toEmbedding :
          (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) → N)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x hx) :
      N)

Tactic:
exact (h x hx).symm

Premises used: Eq.symm
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    Eq (α := N)
      (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod) → N)
          (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) →
                  ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x
                h) :
            ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
        N)
      ((g.cod.subtype : (a : ↥g.cod) → N)
          ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x ⋯) : ↥g.cod) :
        N)
x : M
hx : x ∈ g.dom
⊢ Eq.{w' + 1} (α := N)
    (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
            ({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv.toEmbedding.comp (inclusion ⋯)) :
          (a : ↥g.dom) → N)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x hx) :
      N)
    ((g.cod.subtype.comp g.toEquiv.toEmbedding : (a : ↥g.dom) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x hx) : N)

Tactic:
h x hx
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥g.1 ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    Eq (α := N)
      (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
            (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod) → N)
          (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                (a : ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom) →
                  ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod)
              (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x
                h) :
            ↥{ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
        N)
      ((g.cod.subtype : (a : ↥g.cod) → N)
          ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x ⋯) : ↥g.cod) :
        N)
x : M
hx : x ∈ g.dom
⊢ Eq.{w' + 1} (α := N)
    (({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype.comp
            ({ dom := g.1, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv.toEmbedding.comp (inclusion ⋯)) :
          (a : ↥g.dom) → N)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x hx) :
      N)
    ((g.cod.subtype.comp g.toEquiv.toEmbedding : (a : ↥g.dom) → N) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x hx) : N)

Tactic:
exact h x hx
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f g : M ≃ₚ[L] N
mp :
  f = g →
    ∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : x ∈ f.dom),
        Eq (α := N)
          ((f.cod.subtype : (a : ↥f.cod) → N)
              ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.dom) x h) : ↥f.cod) :
            N)
          ((g.cod.subtype : (a : ↥g.cod) → N)
              ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x ⋯) : ↥g.cod) :
            N)
mpr :
  (∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : x ∈ f.dom),
        Eq (α := N)
          ((f.cod.subtype : (a : ↥f.cod) → N)
              ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.dom) x h) : ↥f.cod) :
            N)
          ((g.cod.subtype : (a : ↥g.cod) → N)
              ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x ⋯) : ↥g.cod) :
            N)) →
    f = g
⊢ f = g ↔
    ∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : x ∈ f.dom),
        Eq (α := N)
          ((f.cod.subtype : (a : ↥f.cod) → N)
              ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.dom) x h) : ↥f.cod) :
            N)
          ((g.cod.subtype : (a : ↥g.cod) → N)
              ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x ⋯) : ↥g.cod) :
            N)

Tactic:
constructor
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
f g : M ≃ₚ[L] N
h_eq : f = g
mp :
  ∀ (dom_f : L.Substructure M) (cod_f : L.Substructure N) (equiv_f : Equiv.{u, v, w, w'} L ↥dom_f ↥cod_f)
    (h_eq : { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } = g),
    ∃ (h_dom : { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom = g.dom),
      ∀ (x : M) (h : x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
        Eq (α := N)
          (({ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
                (a : ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod) → N)
              (({ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                    (a : ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom) →
                      ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod)
                  (Subtype.mk (p := fun (x : M) ↦
                    x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom) x h) :
                ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
            N)
          ((g.cod.subtype : (a : ↥g.cod) → N)
              ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x ⋯) : ↥g.cod) :
            N)
⊢ ∃ (h_dom : f.dom = g.dom),
    ∀ (x : M) (h : x ∈ f.dom),
      Eq (α := N)
        ((f.cod.subtype : (a : ↥f.cod) → N)
            ((f.toEquiv : (a : ↥f.dom) → ↥f.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ f.dom) x h) : ↥f.cod) :
          N)
        ((g.cod.subtype : (a : ↥g.cod) → N)
            ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x ⋯) : ↥g.cod) :
          N)

Tactic:
rcases f with ⟨dom_f, cod_f, equiv_f⟩
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
g : M ≃ₚ[L] N
dom_f : L.Substructure M
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥dom_f ↥cod_f
h_eq : { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N } = g
mp :
  ∃ (h_dom :
    { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom =
      { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    ∀ (x : M) (h : x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
      Eq (α := N)
        (({ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
              (a : ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod) → N)
            (({ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                  (a : ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom) →
                    ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod)
                (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom)
                  x h) :
              ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
          N)
        (({ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
              (a : ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod) → N)
            (({ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                  (a : ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom) →
                    ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod)
                (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom)
                  x ⋯) :
              ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
          N)
⊢ ∃ (h_dom : { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom = g.dom),
    ∀ (x : M) (h : x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
      Eq (α := N)
        (({ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
              (a : ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod) → N)
            (({ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                  (a : ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom) →
                    ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod)
                (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom)
                  x h) :
              ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
          N)
        ((g.cod.subtype : (a : ↥g.cod) → N)
            ((g.toEquiv : (a : ↥g.dom) → ↥g.cod) (Subtype.mk (p := fun (x : M) ↦ x ∈ g.dom) x ⋯) : ↥g.cod) :
          N)

Tactic:
cases h_eq
-- Module: Mathlib.ModelTheory.PartialEquiv
Goal:
L : Language
M : Type w
N : Type w'
inst : L.Structure M
inst_1 : L.Structure N
dom_f : L.Substructure M
cod_f : L.Substructure N
equiv_f : Equiv.{u, v, w, w'} L ↥dom_f ↥cod_f
⊢ ∃ (h_dom :
    { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom =
      { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
    ∀ (x : M) (h : x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom),
      Eq (α := N)
        (({ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
              (a : ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod) → N)
            (({ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                  (a : ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom) →
                    ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod)
                (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom)
                  x h) :
              ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
          N)
        (({ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod.subtype :
              (a : ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod) → N)
            (({ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.toEquiv :
                  (a : ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom) →
                    ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod)
                (Subtype.mk (p := fun (x : M) ↦ x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.dom)
                  x ⋯) :
              ↥{ dom := dom_f, cod := cod_f, toEquiv := equiv_f : M ≃ₚ[L] N }.cod) :
          N)

Tactic:
⟨rfl, fun _ _ ↦ rfl⟩

Premises used: Exists.intro, rfl