rw [eq_comm, h.2 (φ.map_target hi), φ.right_inv hi, φ'.right_inv (target_subset h hi)]
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)
no goals