Simpler variant of Cantor's diagonal argument

[thielema]

I find the proof sketch presented in C04_Sets_and_Functions.S02_Functions.Cantor rather cumbersome. I have come up with a shorter and more symmetrical proof:

theorem Cantor : ∀ f : α → Set α, ¬Surjective f := by
  intro f surjf
  set S := { i | i ∉ f i } with Sdef
  have ⟨j,h⟩ := surjf S
  if p : j ∈ f j
    then have q := Sdef ▸ h ▸ p; simp at q; apply q p
    else have q := Sdef ▸ h ▸ p; simp at q; apply p q

I guess, set and the triangle operator are not introduced at this point, but one could write it using rw tactic.

I am working with leanprover-community/mathematics_in_lean@45b50b9 .