exact (h ⟨x, hy⟩).elim
case pos
α✝ : 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 : β
hf : Injective f
a : α
h : b ∉ range f
x y : α
h_1 : ¬x = a
h✝ : y = a
hy : f x = b
⊢ x = y
no goals