use fun x ↦ if hx : x ∈ s then e ⟨x,hx⟩ else Classical.arbitrary β
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
⊢ ∃ f, BijOn f s t ∧ ∀ (x : ↑s), ↑(e x) = f ↑x
case h
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
⊢ BijOn (fun x => if hx : x ∈ s then ↑(e ⟨x, hx⟩) else Classical.arbitrary β) s t ∧
    ∀ (x : ↑s), ↑(e x) = if hx : ↑x ∈ s then ↑(e ⟨↑x, hx⟩) else Classical.arbitrary β