contradiction
case intro
α✝ : Type u_1
β : Type u_2
inst✝ : Inhabited α✝
P : α✝ → Prop
h✝ : ∃ x, P x
α : Type u_3
f : α → Set α
surjf : Surjective f
S : Set α := {i | i ∉ f i}
j : α
h : f j = S
h₁ : j ∉ f j
h₂ : j ∈ S
h₃ : j ∉ S
⊢ False
no goals