simp_rw
  [Set.union_prod,
   Set.countable_union,
   Set.countable_iff_exists_injective] at hcnt
hcnt : Set.Countable (({0} ∪ {1}) ×ˢ Set.univ)
hun : {0, 1} = {0} ∪ {1}
⊢ False
hun : {0, 1} = {0} ∪ {1}
hcnt : (∃ f, Function.Injective f) ∧ ∃ f, Function.Injective f
⊢ False