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
case intro.intro
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
g : ↑Set.univ → ↑({0} ×ˢ Set.univ) := fun r => { val := (0, ↑r), property := (_ : (0, ↑r) ∈ {0} ×ˢ Set.univ) }
⊢ False
case intro.intro
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
g : ↑Set.univ → ↑({0} ×ˢ Set.univ) := fun r => { val := (0, ↑r), property := (_ : (0, ↑r) ∈ {0} ×ˢ Set.univ) }
ginj : Function.Injective g
⊢ False