exact ⟨hf.toPartialEquiv, rfl, hf.toPartialEquiv_target⟩
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Nonempty α
inst✝ : Nonempty β
s : Set α
t : Set β
hfin : s.Finite
h : s.encard = t.encard
f : α → β
hf : BijOn f s t
⊢ ∃ e, e.source = s ∧ e.target = t
no goals