exact φ'.map_target (target_subset h hi)
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
no goals