rw [← φ.image_source_eq_target, ← φ'.image_source_eq_target]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
⊢ φ.target ⊆ φ'.target
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
φ φ' : PartialEquiv α β
a : α
b : β
h : φ ≤ φ'
⊢ ↑φ '' φ.source ⊆ ↑φ' '' φ'.source