-- Mathlib/ModelTheory/PartialEquiv.lean
theorem ext_iff {f g : M ≃ₚ[L] N} : f = g ↔ ∃ h_dom : f.dom = g.dom,
    ∀ x : M, ∀ h : x ∈ f.dom,
    subtype _ (f.toEquiv ⟨x, h⟩) = subtype _ (g.toEquiv ⟨x, (h_dom ▸ h)⟩)

Proof state:
case mp.mk
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
dom_f : L.Substructure M
cod_f : L.Substructure N
equiv_f : ↥dom_f ≃[L] ↥cod_f
h_eq : { dom := dom_f, cod := cod_f, toEquiv := equiv_f } = g
⊢ ∃ (h_dom : { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom = g.dom),
    ∀ (x : M) (h : x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom),
      { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod.subtype
          ({ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
        g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)

Tactic:
cases h_eq

Result:
case mp.mk.refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
dom_f : L.Substructure M
cod_f : L.Substructure N
equiv_f : ↥dom_f ≃[L] ↥cod_f
⊢ ∃ (h_dom :
    { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom = { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom),
    ∀ (x : M) (h : x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom),
      { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod.subtype
          ({ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
        { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod.subtype
          ({ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, ⋯⟩)

Proof state:
case mp
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h_eq : f = g
⊢ ∃ (h_dom : f.dom = g.dom),
    ∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)

Tactic:
rcases f with ⟨dom_f, cod_f, equiv_f⟩

Result:
case mp.mk
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
dom_f : L.Substructure M
cod_f : L.Substructure N
equiv_f : ↥dom_f ≃[L] ↥cod_f
h_eq : { dom := dom_f, cod := cod_f, toEquiv := equiv_f } = g
⊢ ∃ (h_dom : { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom = g.dom),
    ∀ (x : M) (h : x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom),
      { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod.subtype
          ({ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
        g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)

Proof state:
case mpr.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f.dom = g.dom
H : ∀ (x : M) (h_1 : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h_1⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ f = g

Tactic:
exact ext h H

Result:
no goals

Proof state:
case mp.mk.refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
dom_f : L.Substructure M
cod_f : L.Substructure N
equiv_f : ↥dom_f ≃[L] ↥cod_f
⊢ ∃ (h_dom :
    { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom = { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom),
    ∀ (x : M) (h : x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom),
      { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod.subtype
          ({ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
        { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod.subtype
          ({ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, ⋯⟩)

Tactic:
exact ⟨rfl, fun _ _ ↦ rfl⟩

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
⊢ f = g ↔
    ∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)

Tactic:
constructor

Result:
case mp
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
⊢ f = g →
    ∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)

case mpr
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
⊢ (∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)) →
    f = g

Proof state:
case mpr
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
⊢ (∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)) →
    f = g

Tactic:
rintro ⟨h, H⟩

Result:
case mpr.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f.dom = g.dom
H : ∀ (x : M) (h_1 : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h_1⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ f = g

Proof state:
case mp
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
⊢ f = g →
    ∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)

Tactic:
intro h_eq

Result:
case mp
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h_eq : f = g
⊢ ∃ (h_dom : f.dom = g.dom),
    ∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)