simp
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
y : β
hy : y ∈ t
⊢ ↑(e.symm ⟨y, hy⟩) ∈ s ∧ (fun x => if hx : x ∈ s then ↑(e ⟨x, hx⟩) else Classical.arbitrary β) ↑(e.symm ⟨y, hy⟩) = y
no goals