internlm/Lean-Github huggingface dataset:
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
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✝ }
Tactic:
rw [Subtype.mk.injEq, Set.ext_iff]
Proof state after:
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
⊢ ∀ (x : ℕ × ℕ), x ∈ p ↔ x ∈ q
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
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
⊢ ∀ (x : ℕ × ℕ), x ∈ p ↔ x ∈ q
Tactic:
intro x
Proof state after:
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
x : ℕ × ℕ
⊢ x ∈ p ↔ x ∈ q
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
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
x : ℕ × ℕ
⊢ x ∈ p ↔ x ∈ q
Tactic:
let uniq := 2^x.1 * 3^x.2
Proof state after:
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
⊢ x ∈ p ↔ x ∈ q
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
⊢ x ∈ p ↔ x ∈ q
Tactic:
specialize heq uniq
Proof state after:
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
heq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) ↔ ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
⊢ x ∈ p ↔ x ∈ q
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
heq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) ↔ ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
⊢ x ∈ p ↔ x ∈ q
Tactic:
rcases heq with ⟨pimpq, qimpp⟩
Proof state after:
case mk.mk.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) }
p : Set (ℕ × ℕ)
property✝¹ : p ∈ 𝒫 Set.univ
q : Set (ℕ × ℕ)
property✝ : q ∈ 𝒫 Set.univ
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
⊢ x ∈ p ↔ x ∈ q
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
case mk.mk.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) }
p : Set (ℕ × ℕ)
property✝¹ : p ∈ 𝒫 Set.univ
q : Set (ℕ × ℕ)
property✝ : q ∈ 𝒫 Set.univ
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
⊢ x ∈ p ↔ x ∈ q
Tactic:
constructor
Proof state after:
case mk.mk.intro.mp
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
⊢ x ∈ p → x ∈ q

case mk.mk.intro.mpr
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
⊢ x ∈ q → x ∈ p
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
case mk.mk.intro.mp
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
⊢ x ∈ p → x ∈ q
Tactic:
intro hmemp
Proof state after:
case mk.mk.intro.mp
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemp : x ∈ p
⊢ x ∈ q
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
case mk.mk.intro.mp
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemp : x ∈ p
⊢ x ∈ q
Tactic:
have ⟨a, ⟨b, ⟨hmemq, heqfac⟩⟩⟩
  := pimpq ⟨x.1, ⟨x.2, by simp only [Prod.mk.eta,and_true]; exact hmemp⟩⟩
Proof state after:
case mk.mk.intro.mp
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemp : x ∈ p
a b : ℕ
hmemq : (a, b) ∈ q
heqfac : 2 ^ a * 3 ^ b = uniq
⊢ x ∈ q
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
case mk.mk.intro.mp
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemp : x ∈ p
a b : ℕ
hmemq : (a, b) ∈ q
heqfac : 2 ^ a * 3 ^ b = uniq
⊢ x ∈ q
Tactic:
simp_rw [uniq] at heqfac
Proof state after:
case mk.mk.intro.mp
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemp : x ∈ p
a b : ℕ
hmemq : (a, b) ∈ q
heqfac : 2 ^ a * 3 ^ b = 2 ^ x.1 * 3 ^ x.2
⊢ x ∈ q
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
case mk.mk.intro.mp
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemp : x ∈ p
a b : ℕ
hmemq : (a, b) ∈ q
heqfac : 2 ^ a * 3 ^ b = 2 ^ x.1 * 3 ^ x.2
⊢ x ∈ q
Tactic:
have ⟨heq1, heq2⟩ := two_pow_three_pow_unique_factorization heqfac
Proof state after:
case mk.mk.intro.mp
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemp : x ∈ p
a b : ℕ
hmemq : (a, b) ∈ q
heqfac : 2 ^ a * 3 ^ b = 2 ^ x.1 * 3 ^ x.2
heq1 : a = x.1
heq2 : b = x.2
⊢ x ∈ q
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
case mk.mk.intro.mp
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemp : x ∈ p
a b : ℕ
hmemq : (a, b) ∈ q
heqfac : 2 ^ a * 3 ^ b = 2 ^ x.1 * 3 ^ x.2
heq1 : a = x.1
heq2 : b = x.2
⊢ x ∈ q
Tactic:
rw [heq1, heq2] at hmemq
Proof state after:
case mk.mk.intro.mp
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemp : x ∈ p
a b : ℕ
hmemq : (x.1, x.2) ∈ q
heqfac : 2 ^ a * 3 ^ b = 2 ^ x.1 * 3 ^ x.2
heq1 : a = x.1
heq2 : b = x.2
⊢ x ∈ q
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
case mk.mk.intro.mp
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemp : x ∈ p
a b : ℕ
hmemq : (x.1, x.2) ∈ q
heqfac : 2 ^ a * 3 ^ b = 2 ^ x.1 * 3 ^ x.2
heq1 : a = x.1
heq2 : b = x.2
⊢ x ∈ q
Tactic:
exact hmemq
Proof state after:
no goals
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemp : x ∈ p
⊢ (x.1, x.2) ∈ p ∧ 2 ^ x.1 * 3 ^ x.2 = uniq
Tactic:
simp only [Prod.mk.eta,and_true]
Proof state after:
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemp : x ∈ p
⊢ x ∈ p
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemp : x ∈ p
⊢ x ∈ p
Tactic:
exact hmemp
Proof state after:
no goals
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
case mk.mk.intro.mpr
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
⊢ x ∈ q → x ∈ p
Tactic:
intro hmemq
Proof state after:
case mk.mk.intro.mpr
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemq : x ∈ q
⊢ x ∈ p
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
case mk.mk.intro.mpr
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemq : x ∈ q
⊢ x ∈ p
Tactic:
have ⟨a, ⟨b, ⟨hmemp, heqfac⟩⟩⟩
  := qimpp ⟨x.1, ⟨x.2, by simp only [Prod.mk.eta,and_true]; exact hmemq⟩⟩
Proof state after:
case mk.mk.intro.mpr
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemq : x ∈ q
a b : ℕ
hmemp : (a, b) ∈ p
heqfac : 2 ^ a * 3 ^ b = uniq
⊢ x ∈ p
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
case mk.mk.intro.mpr
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemq : x ∈ q
a b : ℕ
hmemp : (a, b) ∈ p
heqfac : 2 ^ a * 3 ^ b = uniq
⊢ x ∈ p
Tactic:
simp_rw [uniq] at heqfac
Proof state after:
case mk.mk.intro.mpr
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemq : x ∈ q
a b : ℕ
hmemp : (a, b) ∈ p
heqfac : 2 ^ a * 3 ^ b = 2 ^ x.1 * 3 ^ x.2
⊢ x ∈ p
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
case mk.mk.intro.mpr
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemq : x ∈ q
a b : ℕ
hmemp : (a, b) ∈ p
heqfac : 2 ^ a * 3 ^ b = 2 ^ x.1 * 3 ^ x.2
⊢ x ∈ p
Tactic:
have ⟨heq1, heq2⟩ := two_pow_three_pow_unique_factorization heqfac
Proof state after:
case mk.mk.intro.mpr
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemq : x ∈ q
a b : ℕ
hmemp : (a, b) ∈ p
heqfac : 2 ^ a * 3 ^ b = 2 ^ x.1 * 3 ^ x.2
heq1 : a = x.1
heq2 : b = x.2
⊢ x ∈ p
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof state before:
case mk.mk.intro.mpr
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemq : x ∈ q
a b : ℕ
hmemp : (a, b) ∈ p
heqfac : 2 ^ a * 3 ^ b = 2 ^ x.1 * 3 ^ x.2
heq1 : a = x.1
heq2 : b = x.2
⊢ x ∈ p
Tactic:
rw [heq1, heq2] at hmemp
Proof state after:
case mk.mk.intro.mpr
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
x : ℕ × ℕ
uniq : ℕ := 2 ^ x.1 * 3 ^ x.2
pimpq : (∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq
qimpp : (∃ a b, (a, b) ∈ q ∧ 2 ^ a * 3 ^ b = uniq) → ∃ a b, (a, b) ∈ p ∧ 2 ^ a * 3 ^ b = uniq
hmemq : x ∈ q
a b : ℕ
hmemp : (x.1, x.2) ∈ p
heqfac : 2 ^ a * 3 ^ b = 2 ^ x.1 * 3 ^ x.2
heq1 : a = x.1
heq2 : b = x.2
⊢ x ∈ p