-- Mathlib/ModelTheory/PartialEquiv.lean
theorem toPartialEquiv_toEmbedding {f :  M ≃ₚ[L] N} (h : f.dom = ⊤) :
    (PartialEquiv.toEmbeddingOfEqTop h).toPartialEquiv = f

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
h : f.dom = ⊤
⊢ (PartialEquiv.toEmbeddingOfEqTop h).toPartialEquiv = f

Tactic:
rcases f with ⟨_, _, _⟩

Result:
case mk
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
dom✝ : L.Substructure M
cod✝ : L.Substructure N
toEquiv✝ : ↥dom✝ ≃[L] ↥cod✝
h : { dom := dom✝, cod := cod✝, toEquiv := toEquiv✝ }.dom = ⊤
⊢ (PartialEquiv.toEmbeddingOfEqTop h).toPartialEquiv = { dom := dom✝, cod := cod✝, toEquiv := toEquiv✝ }

Proof state:
case mk.refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
cod✝ : L.Substructure N
toEquiv✝ : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod✝
⊢ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv =
    { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }

Tactic:
apply PartialEquiv.ext

Result:
case mk.refl.a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
cod✝ : L.Substructure N
toEquiv✝ : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod✝
⊢ ∀ (x : M) (h : x ∈ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom),
    (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod.subtype
        ((PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.toEquiv ⟨x, h⟩) =
      { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.cod.subtype
        ({ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.toEquiv ⟨x, ⋯⟩)

case mk.refl.h_dom
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
cod✝ : L.Substructure N
toEquiv✝ : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod✝
⊢ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom =
    { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.dom

Proof state:
case mk.refl.a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
cod✝ : L.Substructure N
toEquiv✝ : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod✝
⊢ ∀ (x : M) (h : x ∈ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom),
    (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod.subtype
        ((PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.toEquiv ⟨x, h⟩) =
      { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.cod.subtype
        ({ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.toEquiv ⟨x, ⋯⟩)

Tactic:
intro _ _

Result:
case mk.refl.a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
cod✝ : L.Substructure N
toEquiv✝ : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod✝
x✝ : M
h✝ : x✝ ∈ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom
⊢ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod.subtype
      ((PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.toEquiv ⟨x✝, h✝⟩) =
    { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.cod.subtype
      ({ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.toEquiv ⟨x✝, ⋯⟩)

Proof state:
case mk.refl.h_dom
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
cod✝ : L.Substructure N
toEquiv✝ : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod✝
⊢ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom =
    { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.dom

Tactic:
rfl

Result:
no goals

Proof state:
case mk.refl.a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
cod✝ : L.Substructure N
toEquiv✝ : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod✝
x✝ : M
h✝ : x✝ ∈ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom
⊢ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod.subtype
      ((PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.toEquiv ⟨x✝, h✝⟩) =
    { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.cod.subtype
      ({ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.toEquiv ⟨x✝, ⋯⟩)

Tactic:
rfl

Result:
no goals

Proof state:
case mk
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
dom✝ : L.Substructure M
cod✝ : L.Substructure N
toEquiv✝ : ↥dom✝ ≃[L] ↥cod✝
h : { dom := dom✝, cod := cod✝, toEquiv := toEquiv✝ }.dom = ⊤
⊢ (PartialEquiv.toEmbeddingOfEqTop h).toPartialEquiv = { dom := dom✝, cod := cod✝, toEquiv := toEquiv✝ }

Tactic:
cases h

Result:
case mk.refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
cod✝ : L.Substructure N
toEquiv✝ : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod✝
⊢ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv =
    { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }