rintro rfl
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f✝ : α → β
f : α
inst✝ : DecidableEq α
S : Set α
hf : f ∉ S
x : α
he : x ∈ S
⊢ x ≠ f
α : Type u_1
β : Type u_2
s s₁ s₂ t t' : Set α
f : α → β
inst✝ : DecidableEq α
S : Set α
x : α
he : x ∈ S
hf : x ∉ S
⊢ False