let g : (𝒫 (Set.univ : Set ℕ)) → (𝒫 (Set.univ : Set (ℕ × ℕ))) := by
  intro a_set_of_n
  have a_set_of_nxn : Set (ℕ × ℕ) := a_set_of_n.val ×ˢ a_set_of_n.val
  exact { val := a_set_of_nxn, property := by simp }
f : ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ) :=
  fun a_set_of_nxn =>
    { val := {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x},
      property := (_ : {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x} ∈ 𝒫 Set.univ) }
hf : Function.Injective f
⊢ ∃ fg, Function.Bijective fg
f : ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ) :=
  fun a_set_of_nxn =>
    { val := {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x},
      property := (_ : {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x} ∈ 𝒫 Set.univ) }
hf : Function.Injective f
g : ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ) :=
  fun a_set_of_n =>
    let_fun a_set_of_nxn := ↑a_set_of_n ×ˢ ↑a_set_of_n;
    { val := a_set_of_nxn, property := (_ : a_set_of_nxn ∈ 𝒫 Set.univ) }
⊢ ∃ fg, Function.Bijective fg