refine ⟨target_subset h, fun {i} hi ↦ φ'.injOn ?_ ?_ ?_⟩
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
⊢ φ.symm ≤ φ'.symm
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
i : β
hi : i ∈ φ.symm.source
⊢ ↑φ'.symm i ∈ φ'.source

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
i : β
hi : i ∈ φ.symm.source
⊢ ↑φ.symm i ∈ φ'.source

case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
i : β
hi : i ∈ φ.symm.source
⊢ ↑φ' (↑φ'.symm i) = ↑φ' (↑φ.symm i)