-- Mathlib/ModelTheory/PartialEquiv.lean
theorem le_antisymm (f g : M ≃ₚ[L] N) (le_fg : f ≤ g) (le_gf : g ≤ f) : f = g

Proof state:
case h.e'_3.h.e'_8.h.h.h.h.h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
equiv_f : ↥g.1 ≃[L] ↥g.2
le_fg : { dom := g.1, cod := g.2, toEquiv := equiv_f } ≤ g
le_gf : g ≤ { dom := g.1, cod := g.2, toEquiv := equiv_f }
he✝¹ : g.dom = g.1
he✝ : g.cod = g.2
⊢ g.toEquiv = equiv_f

Tactic:
exact Equiv.injective_toEmbedding ((subtype _).comp_injective (subtype_toEquiv_inclusion le_fg))

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
le_fg : f ≤ g
le_gf : g ≤ f
⊢ f = g

Tactic:
let ⟨dom_f, cod_f, equiv_f⟩ := f

Result:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_f : L.Substructure M
cod_f : L.Substructure N
equiv_f : ↥dom_f ≃[L] ↥cod_f
le_fg : { dom := dom_f, cod := cod_f, toEquiv := equiv_f } ≤ g
le_gf : g ≤ { dom := dom_f, cod := cod_f, toEquiv := equiv_f }
⊢ { dom := dom_f, cod := cod_f, toEquiv := equiv_f } = g

Proof state:
case refl.refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
equiv_f : ↥g.1 ≃[L] ↥g.2
le_fg : { dom := g.1, cod := g.2, toEquiv := equiv_f } ≤ g
le_gf : g ≤ { dom := g.1, cod := g.2, toEquiv := equiv_f }
⊢ { dom := g.1, cod := g.2, toEquiv := equiv_f } = g

Tactic:
convert rfl

Result:
case h.e'_3.h.e'_8.h.h.h.h.h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
equiv_f : ↥g.1 ≃[L] ↥g.2
le_fg : { dom := g.1, cod := g.2, toEquiv := equiv_f } ≤ g
le_gf : g ≤ { dom := g.1, cod := g.2, toEquiv := equiv_f }
he✝¹ : g.dom = g.1
he✝ : g.cod = g.2
⊢ g.toEquiv = equiv_f

Proof state:
case refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
le_fg : { dom := g.1, cod := cod_f, toEquiv := equiv_f } ≤ g
le_gf : g ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f }
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f } = g

Tactic:
cases _root_.le_antisymm (cod_le_cod le_fg) (cod_le_cod le_gf)

Result:
case refl.refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
equiv_f : ↥g.1 ≃[L] ↥g.2
le_fg : { dom := g.1, cod := g.2, toEquiv := equiv_f } ≤ g
le_gf : g ≤ { dom := g.1, cod := g.2, toEquiv := equiv_f }
⊢ { dom := g.1, cod := g.2, toEquiv := equiv_f } = g

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_f : L.Substructure M
cod_f : L.Substructure N
equiv_f : ↥dom_f ≃[L] ↥cod_f
le_fg : { dom := dom_f, cod := cod_f, toEquiv := equiv_f } ≤ g
le_gf : g ≤ { dom := dom_f, cod := cod_f, toEquiv := equiv_f }
⊢ { dom := dom_f, cod := cod_f, toEquiv := equiv_f } = g

Tactic:
cases _root_.le_antisymm (dom_le_dom le_fg) (dom_le_dom le_gf)

Result:
case refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
le_fg : { dom := g.1, cod := cod_f, toEquiv := equiv_f } ≤ g
le_gf : g ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f }
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f } = g