simpa [dif_pos hx, dif_pos hy, Subtype.coe_inj] using hxy
case h.refine_2
α : Type u_1
β : Type u_2
s✝ s₁ s₂ t✝ t' : Set α
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
e : ↑s ≃ ↑t
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy :
  (if hx : x ∈ s then ↑(e ⟨x, hx⟩) else Classical.arbitrary β) =
    if hx : y ∈ s then ↑(e ⟨y, hx⟩) else Classical.arbitrary β
⊢ x = y
no goals