Simple proof of Cantor's theorem.

cantor.lean

import set_theory.cardinal

-- https://www.youtube.com/watch?v=3ZHacSgSj0Q

variable {α : Type}

lemma not_exists_surj : ¬ ∃ f : α → set α, function.surjective f :=
begin
  intro h,
  cases h with f hf,
  let s := {x | x ∉ f x},
  have hs : ∃ x, _ := hf s,
  cases hs with x hx,
  have : x ∈ s ↔ x ∈ f x, by rw hx,
  simp only [set.mem_set_of_eq] at this,
  simpa
end

prefix # := cardinal.mk

theorem cantor : #α < #(set α) :=
begin
  split,
  { let f : α → set α := λ x, {x},
    refine ⟨⟨f, _⟩⟩,
    intros x₁ x₂ hx,
    simpa using hx },
  { rintro ⟨⟨f, hf⟩⟩,
    refine not_exists_surj ⟨function.inv_fun f, _⟩,
    exact function.inv_fun_surjective hf }
end