simp only [or_self] at hb
case inr.intro
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) }
a b : ↑(𝒫 Set.univ)
hb : ↑b = ∅ ∨ ↑b = ∅
ha : ↑a = ∅
⊢ a = b
case inr.intro
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) }
a b : ↑(𝒫 Set.univ)
ha : ↑a = ∅
hb : ↑b = ∅
⊢ a = b