Theorem: power_nat_nat_card_eq_power_nat_csb (meetings/ex5.lean)

State before:
⊢ ∃ fg, Function.Bijective fg
Tactic:
let f : (𝒫 (Set.univ : Set (ℕ × ℕ))) → (𝒫 (Set.univ : Set ℕ)) := by
  intro a_set_of_nxn
  exact {
    val := {2^x.1 * 3^x.2 | x ∈ a_set_of_nxn.val}
    property := by simp only [Set.powerset_univ, Set.mem_univ]
  }
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) }
⊢ ∃ fg, Function.Bijective fg

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) }
hf : Function.Injective f
⊢ ∃ fg, Function.Bijective fg
Tactic:
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 }
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) }
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

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) }
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) }
hg : Function.Injective g
⊢ ∃ fg, Function.Bijective fg
Tactic:
exact Function.Embedding.schroeder_bernstein hf hg
State after:
no goals

State before:
⊢ ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ)
Tactic:
intro a_set_of_nxn
State after:
a_set_of_nxn : ↑(𝒫 Set.univ)
⊢ ↑(𝒫 Set.univ)

State before:
a_set_of_nxn : ↑(𝒫 Set.univ)
⊢ ↑(𝒫 Set.univ)
Tactic:
exact {
  val := {2^x.1 * 3^x.2 | x ∈ a_set_of_nxn.val}
  property := by simp only [Set.powerset_univ, Set.mem_univ]
}
State after:
no goals

State before:
a_set_of_nxn : ↑(𝒫 Set.univ)
⊢ {x | ∃ x_1 ∈ ↑a_set_of_nxn, 2 ^ x_1.1 * 3 ^ x_1.2 = x} ∈ 𝒫 Set.univ
Tactic:
simp only [Set.powerset_univ, Set.mem_univ]
State after:
no goals

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) }
⊢ Function.Injective f
Tactic:
rintro ⟨p, _⟩ ⟨q, _⟩ heq
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 : f { val := p, property := property✝¹ } = f { val := q, property := property✝ }
⊢ { val := p, property := property✝¹ } = { val := q, property := property✝ }

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 : f { val := p, property := property✝¹ } = f { val := q, property := property✝ }
⊢ { val := p, property := property✝¹ } = { val := q, property := property✝ }
Tactic:
simp only [f, Prod.exists, Subtype.mk.injEq, Set.ext_iff, Set.mem_setOf_eq] at heq
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
⊢ { val := p, property := property✝¹ } = { val := q, property := property✝ }

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]
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

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
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

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
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

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
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

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⟩
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

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
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

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
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

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⟩⟩
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

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
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

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
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

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
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

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
State after:
no goals

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]
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

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
State after:
no goals

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
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

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⟩⟩
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

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
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

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
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

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
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

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 : (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
Tactic:
exact hmemp
State after:
no goals

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
hmemq : x ∈ q
⊢ (x.1, x.2) ∈ q ∧ 2 ^ x.1 * 3 ^ x.2 = uniq
Tactic:
simp only [Prod.mk.eta,and_true]
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
hmemq : x ∈ q
⊢ x ∈ q

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
hmemq : x ∈ q
⊢ x ∈ q
Tactic:
exact hmemq
State after:
no goals

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) }
hf : Function.Injective f
⊢ ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ)
Tactic:
intro a_set_of_n
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) }
hf : Function.Injective f
a_set_of_n : ↑(𝒫 Set.univ)
⊢ ↑(𝒫 Set.univ)

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) }
hf : Function.Injective f
a_set_of_n : ↑(𝒫 Set.univ)
⊢ ↑(𝒫 Set.univ)
Tactic:
have a_set_of_nxn : Set (ℕ × ℕ) := a_set_of_n.val ×ˢ a_set_of_n.val
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) }
hf : Function.Injective f
a_set_of_n : ↑(𝒫 Set.univ)
a_set_of_nxn : Set (ℕ × ℕ)
⊢ ↑(𝒫 Set.univ)

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) }
hf : Function.Injective f
a_set_of_n : ↑(𝒫 Set.univ)
a_set_of_nxn : Set (ℕ × ℕ)
⊢ ↑(𝒫 Set.univ)
Tactic:
exact { val := a_set_of_nxn, property := by simp }
State after:
no goals

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) }
hf : Function.Injective f
a_set_of_n : ↑(𝒫 Set.univ)
a_set_of_nxn : Set (ℕ × ℕ)
⊢ a_set_of_nxn ∈ 𝒫 Set.univ
Tactic:
simp
State after:
no goals

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) }
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) }
⊢ Function.Injective g
Tactic:
intros a b heq
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) }
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)
heq : g a = g b
⊢ a = b

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) }
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)
heq : g a = g b
⊢ a = b
Tactic:
simp only [g, Subtype.mk.injEq, Set.prod_eq_prod_iff] at heq
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) }
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)
heq : ↑a = ↑b ∧ ↑a = ↑b ∨ (↑a = ∅ ∨ ↑a = ∅) ∧ (↑b = ∅ ∨ ↑b = ∅)
⊢ a = b

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) }
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)
heq : ↑a = ↑b ∧ ↑a = ↑b ∨ (↑a = ∅ ∨ ↑a = ∅) ∧ (↑b = ∅ ∨ ↑b = ∅)
⊢ a = b
Tactic:
rcases heq with (coe_eq | ⟨ha, hb⟩)
State after:
case inl
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)
coe_eq : ↑a = ↑b ∧ ↑a = ↑b
⊢ 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 = ∅ ∨ ↑a = ∅
hb : ↑b = ∅ ∨ ↑b = ∅
⊢ a = b

State before:
case inl
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)
coe_eq : ↑a = ↑b ∧ ↑a = ↑b
⊢ a = b
Tactic:
exact SetCoe.ext coe_eq.1
State after:
no goals

State before:
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 = ∅ ∨ ↑a = ∅
hb : ↑b = ∅ ∨ ↑b = ∅
⊢ a = b
Tactic:
simp only [or_self] at ha
State after:
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

State before:
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
Tactic:
simp only [or_self] at hb
State after:
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

State before:
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
Tactic:
rw [←hb] at ha
State after:
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 = ↑b
hb : ↑b = ∅
⊢ a = b

State before:
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 = ↑b
hb : ↑b = ∅
⊢ a = b
Tactic:
exact SetCoe.ext ha
State after:
no goals