-- Mathlib/ModelTheory/PartialEquiv.lean
theorem toPartialEquiv_injective :
    Function.Injective (fun f : M ↪[L] N ↦ f.toPartialEquiv)

Proof state:
case h.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ↪[L] N
x✝ : M
w✝ : ((fun f => f.toPartialEquiv) a₁✝).dom = ((fun f => f.toPartialEquiv) a₂✝).dom
H :
  ∀ (x : M) (h : x ∈ ((fun f => f.toPartialEquiv) a₁✝).dom),
    ((fun f => f.toPartialEquiv) a₁✝).cod.subtype (((fun f => f.toPartialEquiv) a₁✝).toEquiv ⟨x, h⟩) =
      ((fun f => f.toPartialEquiv) a₂✝).cod.subtype (((fun f => f.toPartialEquiv) a₂✝).toEquiv ⟨x, ⋯⟩)
⊢ a₁✝ x✝ = a₂✝ x✝

Tactic:
exact H _ (Substructure.mem_top _)

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ↪[L] N
h : (fun f => f.toPartialEquiv) a₁✝ = (fun f => f.toPartialEquiv) a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext

Result:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ↪[L] N
h : (fun f => f.toPartialEquiv) a₁✝ = (fun f => f.toPartialEquiv) a₂✝
x✝ : M
⊢ a₁✝ x✝ = a₂✝ x✝

Proof state:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ↪[L] N
h : (fun f => f.toPartialEquiv) a₁✝ = (fun f => f.toPartialEquiv) a₂✝
x✝ : M
⊢ a₁✝ x✝ = a₂✝ x✝

Tactic:
rw [PartialEquiv.ext_iff] at h

Result:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ↪[L] N
h :
  ∃ (h_dom : ((fun f => f.toPartialEquiv) a₁✝).dom = ((fun f => f.toPartialEquiv) a₂✝).dom),
    ∀ (x : M) (h : x ∈ ((fun f => f.toPartialEquiv) a₁✝).dom),
      ((fun f => f.toPartialEquiv) a₁✝).cod.subtype (((fun f => f.toPartialEquiv) a₁✝).toEquiv ⟨x, h⟩) =
        ((fun f => f.toPartialEquiv) a₂✝).cod.subtype (((fun f => f.toPartialEquiv) a₂✝).toEquiv ⟨x, ⋯⟩)
x✝ : M
⊢ a₁✝ x✝ = a₂✝ x✝

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
⊢ Function.Injective fun f => f.toPartialEquiv

Tactic:
intro _ _ h

Result:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ↪[L] N
h : (fun f => f.toPartialEquiv) a₁✝ = (fun f => f.toPartialEquiv) a₂✝
⊢ a₁✝ = a₂✝

Proof state:
case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ↪[L] N
h :
  ∃ (h_dom : ((fun f => f.toPartialEquiv) a₁✝).dom = ((fun f => f.toPartialEquiv) a₂✝).dom),
    ∀ (x : M) (h : x ∈ ((fun f => f.toPartialEquiv) a₁✝).dom),
      ((fun f => f.toPartialEquiv) a₁✝).cod.subtype (((fun f => f.toPartialEquiv) a₁✝).toEquiv ⟨x, h⟩) =
        ((fun f => f.toPartialEquiv) a₂✝).cod.subtype (((fun f => f.toPartialEquiv) a₂✝).toEquiv ⟨x, ⋯⟩)
x✝ : M
⊢ a₁✝ x✝ = a₂✝ x✝

Tactic:
rcases h with ⟨_, H⟩

Result:
case h.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ↪[L] N
x✝ : M
w✝ : ((fun f => f.toPartialEquiv) a₁✝).dom = ((fun f => f.toPartialEquiv) a₂✝).dom
H :
  ∀ (x : M) (h : x ∈ ((fun f => f.toPartialEquiv) a₁✝).dom),
    ((fun f => f.toPartialEquiv) a₁✝).cod.subtype (((fun f => f.toPartialEquiv) a₁✝).toEquiv ⟨x, h⟩) =
      ((fun f => f.toPartialEquiv) a₂✝).cod.subtype (((fun f => f.toPartialEquiv) a₂✝).toEquiv ⟨x, ⋯⟩)
⊢ a₁✝ x✝ = a₂✝ x✝