chore(logic/function/basic): don't unfold set in cantor (#13822)

This uses `set_of` and `mem` consistently instead of using application everywhere, since `f` has type `A -> set A` instead of `A -> A -> Prop`. (Arguably, it could just be stated for `A -> A -> Prop` instead though.)

src/logic/function/basic.lean

@@ -206,14 +206,13 @@ and_congr (injective.of_comp_iff hf.injective _) (surjective.of_comp_iff' hf _)
 /-- **Cantor's diagonal argument** implies that there are no surjective functions from `α`
 to `set α`. -/
 theorem cantor_surjective {α} (f : α → set α) : ¬ function.surjective f | h :=
-let ⟨D, e⟩ := h (λ a, ¬ f a a) in
-(iff_not_self (f D D)).1 $ iff_of_eq (congr_fun e D)
+let ⟨D, e⟩ := h {a | ¬ a ∈ f a} in
+(iff_not_self (D ∈ f D)).1 $ iff_of_eq (congr_arg ((∈) D) e)
 
 /-- **Cantor's diagonal argument** implies that there are no injective functions from `set α`
 to `α`. -/
-theorem cantor_injective {α : Type*} (f : (set α) → α) :
-  ¬ function.injective f | i :=
-cantor_surjective (λ a b, ∀ U, a = f U → U b) $
+theorem cantor_injective {α : Type*} (f : set α → α) : ¬ function.injective f | i :=
+cantor_surjective (λ a, {b | ∀ U, a = f U → b ∈ U}) $
 right_inverse.surjective (λ U, funext $ λ a, propext ⟨λ h, h U rfl, λ h' U' e, i e ▸ h'⟩)
 
 /-- There is no surjection from `α : Type u` into `Type u`. This theorem