simp only [f, Prod.exists, Subtype.mk.injEq, Set.ext_iff, Set.mem_setOf_eq] at heq
case mk.mk
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) }
p : Set (ℕ × ℕ)
property✝¹ : p ∈ 𝒫 Set.univ
q : Set (ℕ × ℕ)
property✝ : q ∈ 𝒫 Set.univ
heq : f { val := p, property := property✝¹ } = f { val := q, property := property✝ }
⊢ { val := p, property := property✝¹ } = { val := q, property := property✝ }
case mk.mk
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) }
p : Set (ℕ × ℕ)
property✝¹ : p ∈ 𝒫 Set.univ
q : Set (ℕ × ℕ)
property✝ : q ∈ 𝒫 Set.univ
heq : ∀ (x : ℕ), (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = x) ↔ ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = x
⊢ { val := p, property := property✝¹ } = { val := q, property := property✝ }