have hucnt
  : ¬(Set.Countable (({0, 1} : Set ℕ) ×ˢ (Set.univ : Set ℝ))) := by
  intro hcnt
  have hun : ({0, 1} : Set ℕ) = {0} ∪ {1} := by
    rw [Set.union_comm, Set.union_singleton]
  rw [hun] at hcnt
  simp_rw
    [Set.union_prod,
     Set.countable_union,
     Set.countable_iff_exists_injective] at hcnt
  rcases hcnt with ⟨⟨f, finj⟩⟩
  let g : ↑(Set.univ : Set ℝ) → ({0} ×ˢ (Set.univ : Set ℝ))
    := λ r => ⟨((0 : ℕ), r), by simp⟩
  have ginj : Function.Injective g := by
    intro a b heq
    simp only [Subtype.mk.injEq, Prod.mk.injEq, true_and] at heq
    exact SetCoe.ext heq
  let fg : ↑(Set.univ : Set ℝ) → ℕ := f ∘ g
  have fginj := Function.Injective.comp finj ginj
  exact Cardinal.not_countable_real (Set.countable_iff_exists_injective.mpr ⟨fg, fginj⟩)
⊢ Uncountable ({0, 1} ×ˢ Set.univ)
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
⊢ Uncountable ({0, 1} ×ˢ Set.univ)