1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16

import Mathlib

#synth Uncountable Cardinal

example : Uncountable (Type u) := by
  by_contra! h
  obtain ⟨f, hf⟩ := countable_iff_exists_surjective.mp h
  let g (t : Type u) := Cardinal.mk t
  let T := g '' Set.range f
  obtain ⟨k, hk⟩ : ∃ k, k ∉ T := by
    by_contra
    have : T.Countable := Set.countable_range f |>.image g
    have : T = .univ := by grind
    grind [Set.not_countable_univ]
  obtain ⟨t, ht⟩ : ∃ t, g t = k := ⟨_, k.mk_out⟩
  exact hk <| ht ▸ Set.mem_image_of_mem g (hf t)