exact hne.symm <| h.2 hx y hy hxy.symm
case refine_3.inl
α✝ : Type u_1
β✝ : Type u_2
r s✝ s₁ s₂ : Set α✝
t t' t₁ t₂ : Set β✝
f✝¹ : α✝ → β✝
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f✝ : α → β
a : α
b✝ : β
f : α → β
s : Set α
b : β
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : InjOn f (s \ {x}) ∧ (x ∈ s → ∀ x_1 ∈ s, f x_1 = b → x_1 = x)
hxy : b = f y
hne : x ≠ y
⊢ False
no goals