internlm/Lean-Github huggingface dataset:
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 : (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
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
hmemq : x ∈ q
⊢ (x.1, x.2) ∈ q ∧ 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
hmemq : x ∈ q
⊢ x ∈ q
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
hmemq : x ∈ q
⊢ 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) }
hf : Function.Injective f
⊢ ↑(𝒫 Set.univ) → ↑(𝒫 Set.univ)
Tactic:
intro a_set_of_n
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) }
hf : Function.Injective f
a_set_of_n : ↑(𝒫 Set.univ)
⊢ ↑(𝒫 Set.univ)
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) }
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
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) }
hf : Function.Injective f
a_set_of_n : ↑(𝒫 Set.univ)
a_set_of_nxn : Set (ℕ × ℕ)
⊢ ↑(𝒫 Set.univ)
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) }
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 }
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) }
hf : Function.Injective f
a_set_of_n : ↑(𝒫 Set.univ)
a_set_of_nxn : Set (ℕ × ℕ)
⊢ a_set_of_nxn ∈ 𝒫 Set.univ
Tactic:
simp
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) }
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
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) }
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
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) }
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
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) }
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
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) }
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⟩)
Proof 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
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof 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
Proof state after:
no goals
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof 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
Proof 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
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof 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
Proof 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
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof 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
Proof 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
Theorem: power_nat_nat_card_eq_power_nat_csb
Proof 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
Proof state after:
no goals
Theorem: every_nonzero_nat_successor
Proof state before:
n : ↑N0
⊢ n ≠ z → ∃ m, n = S m
Tactic:
intro hne
Proof state after:
n : ↑N0
hne : n ≠ z
⊢ ∃ m, n = S m
Theorem: every_nonzero_nat_successor
Proof state before:
n : ↑N0
hne : n ≠ z
⊢ ∃ m, n = S m
Tactic:
let A := {n : N0 | n ≠ z → ∃ m : N0, n = S m}
Proof state after:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
⊢ ∃ m, n = S m
Theorem: every_nonzero_nat_successor
Proof state before:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
⊢ ∃ m, n = S m
Tactic:
have hzmem : z ∈ A := by
  simp only [ne_eq, Subtype.exists, Set.mem_setOf_eq, not_true_eq_false, IsEmpty.forall_iff]
Proof state after:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
⊢ ∃ m, n = S m
Theorem: every_nonzero_nat_successor
Proof state before:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
⊢ ∃ m, n = S m
Tactic:
have hind : (∀ n : N0, n ∈ A → (S n) ∈ A) := by
  intros n _
  simp only [ne_eq, Subtype.exists, Set.mem_setOf_eq]
  intro _
  use n
  simp only [Subtype.coe_eta, Subtype.coe_prop, exists_const]
Proof state after:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ ∃ m, n = S m
Theorem: every_nonzero_nat_successor
Proof state before:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ ∃ m, n = S m
Tactic:
have heq := p3 A ⟨hzmem, hind⟩
Proof state after:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ ∃ m, n = S m
Theorem: every_nonzero_nat_successor
Proof state before:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ ∃ m, n = S m
Tactic:
simp [A, Set.ext_iff] at heq
Proof state after:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  ∀ (x : α),
    (∃ (x_1 : x ∈ N0),
        ¬{ val := x, property := (_ : x ∈ N0) } = z →
          ∃ a, ∃ (b : a ∈ N0), { val := x, property := (_ : x ∈ N0) } = S { val := a, property := b }) ↔
      x ∈ N0
⊢ ∃ m, n = S m
Theorem: every_nonzero_nat_successor
Proof state before:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  ∀ (x : α),
    (∃ (x_1 : x ∈ N0),
        ¬{ val := x, property := (_ : x ∈ N0) } = z →
          ∃ a, ∃ (b : a ∈ N0), { val := x, property := (_ : x ∈ N0) } = S { val := a, property := b }) ↔
      x ∈ N0
⊢ ∃ m, n = S m
Tactic:
specialize heq n
Proof state after:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  (∃ (x : ↑n ∈ N0),
      ¬{ val := ↑n, property := (_ : ↑n ∈ N0) } = z →
        ∃ a, ∃ (b : a ∈ N0), { val := ↑n, property := (_ : ↑n ∈ N0) } = S { val := a, property := b }) ↔
    ↑n ∈ N0
⊢ ∃ m, n = S m
Theorem: every_nonzero_nat_successor
Proof state before:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  (∃ (x : ↑n ∈ N0),
      ¬{ val := ↑n, property := (_ : ↑n ∈ N0) } = z →
        ∃ a, ∃ (b : a ∈ N0), { val := ↑n, property := (_ : ↑n ∈ N0) } = S { val := a, property := b }) ↔
    ↑n ∈ N0
⊢ ∃ m, n = S m
Tactic:
simp only [Subtype.coe_eta, Subtype.coe_prop, exists_const, iff_true] at heq
Proof state after:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : ¬n = z → ∃ a, ∃ (h : a ∈ N0), n = S { val := a, property := (_ : a ∈ N0) }
⊢ ∃ m, n = S m
Theorem: every_nonzero_nat_successor
Proof state before:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : ¬n = z → ∃ a, ∃ (h : a ∈ N0), n = S { val := a, property := (_ : a ∈ N0) }
⊢ ∃ m, n = S m
Tactic:
rcases heq hne with ⟨a, ⟨h, heq⟩⟩
Proof state after:
case intro.intro
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq✝ : ¬n = z → ∃ a, ∃ (h : a ∈ N0), n = S { val := a, property := (_ : a ∈ N0) }
a : α
h : a ∈ N0
heq : n = S { val := a, property := (_ : a ∈ N0) }
⊢ ∃ m, n = S m
Theorem: every_nonzero_nat_successor
Proof state before:
case intro.intro
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq✝ : ¬n = z → ∃ a, ∃ (h : a ∈ N0), n = S { val := a, property := (_ : a ∈ N0) }
a : α
h : a ∈ N0
heq : n = S { val := a, property := (_ : a ∈ N0) }
⊢ ∃ m, n = S m
Tactic:
use { val := a, property := h }
Proof state after:
no goals
Theorem: every_nonzero_nat_successor
Proof state before:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
⊢ z ∈ A
Tactic:
simp only [ne_eq, Subtype.exists, Set.mem_setOf_eq, not_true_eq_false, IsEmpty.forall_iff]
Proof state after:
no goals
Theorem: every_nonzero_nat_successor
Proof state before:
n : ↑N0
hne : n ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
⊢ ∀ n ∈ A, S n ∈ A
Tactic:
intros n _
Proof state after:
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝ : n ∈ A
⊢ S n ∈ A
Theorem: every_nonzero_nat_successor
Proof state before:
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝ : n ∈ A
⊢ S n ∈ A
Tactic:
simp only [ne_eq, Subtype.exists, Set.mem_setOf_eq]
Proof state after:
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝ : n ∈ A
⊢ ¬S n = z → ∃ a, ∃ (b : a ∈ N0), S n = S { val := a, property := b }
Theorem: every_nonzero_nat_successor
Proof state before:
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝ : n ∈ A
⊢ ¬S n = z → ∃ a, ∃ (b : a ∈ N0), S n = S { val := a, property := b }
Tactic:
intro _
Proof state after:
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝¹ : n ∈ A
a✝ : ¬S n = z
⊢ ∃ a, ∃ (b : a ∈ N0), S n = S { val := a, property := b }
Theorem: every_nonzero_nat_successor
Proof state before:
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝¹ : n ∈ A
a✝ : ¬S n = z
⊢ ∃ a, ∃ (b : a ∈ N0), S n = S { val := a, property := b }
Tactic:
use n
Proof state after:
case h
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝¹ : n ∈ A
a✝ : ¬S n = z
⊢ ∃ (b : ↑n ∈ N0), S n = S { val := ↑n, property := b }
Theorem: every_nonzero_nat_successor
Proof state before:
case h
n✝ : ↑N0
hne : n✝ ≠ z
A : Set ↑N0 := {n | n ≠ z → ∃ m, n = S m}
hzmem : z ∈ A
n : ↑N0
a✝¹ : n ∈ A
a✝ : ¬S n = z
⊢ ∃ (b : ↑n ∈ N0), S n = S { val := ↑n, property := b }
Tactic:
simp only [Subtype.coe_eta, Subtype.coe_prop, exists_const]
Proof state after:
no goals
Theorem: zero_plus_x_eq_eq
Proof state before:
x : ↑N0
⊢ plus (z, x) = x
Tactic:
let A := {b : N0 | plus (z, b) = b}
Proof state after:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
⊢ plus (z, x) = x
Theorem: zero_plus_x_eq_eq
Proof state before:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
⊢ plus (z, x) = x
Tactic:
have hzmem : z ∈ A := by
  simp only [Set.mem_setOf_eq]
  exact zplus z
Proof state after:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
⊢ plus (z, x) = x
Theorem: zero_plus_x_eq_eq
Proof state before:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
⊢ plus (z, x) = x
Tactic:
have hind : (∀ n : N0, n ∈ A → (S n) ∈ A) := by
  intros n hel
  simp only [Set.mem_setOf_eq]
  simp only [Set.mem_setOf_eq] at hel
  rw [splus, hel]
Proof state after:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ plus (z, x) = x
Theorem: zero_plus_x_eq_eq
Proof state before:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ plus (z, x) = x
Tactic:
have heq := p3 A ⟨hzmem, hind⟩
Proof state after:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ plus (z, x) = x
Theorem: zero_plus_x_eq_eq
Proof state before:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ plus (z, x) = x
Tactic:
simp [A, Set.ext_iff] at heq
Proof state after:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  ∀ (x : α),
    (∃ (x_1 : x ∈ N0), plus (z, { val := x, property := (_ : x ∈ N0) }) = { val := x, property := (_ : x ∈ N0) }) ↔
      x ∈ N0
⊢ plus (z, x) = x
Theorem: zero_plus_x_eq_eq
Proof state before:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  ∀ (x : α),
    (∃ (x_1 : x ∈ N0), plus (z, { val := x, property := (_ : x ∈ N0) }) = { val := x, property := (_ : x ∈ N0) }) ↔
      x ∈ N0
⊢ plus (z, x) = x
Tactic:
specialize heq x
Proof state after:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  (∃ (x_1 : ↑x ∈ N0), plus (z, { val := ↑x, property := (_ : ↑x ∈ N0) }) = { val := ↑x, property := (_ : ↑x ∈ N0) }) ↔
    ↑x ∈ N0
⊢ plus (z, x) = x
Theorem: zero_plus_x_eq_eq
Proof state before:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq :
  (∃ (x_1 : ↑x ∈ N0), plus (z, { val := ↑x, property := (_ : ↑x ∈ N0) }) = { val := ↑x, property := (_ : ↑x ∈ N0) }) ↔
    ↑x ∈ N0
⊢ plus (z, x) = x
Tactic:
simp only [Subtype.coe_eta, Subtype.coe_prop, exists_const, iff_true] at heq
Proof state after:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : plus (z, x) = x
⊢ plus (z, x) = x
Theorem: zero_plus_x_eq_eq
Proof state before:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : plus (z, x) = x
⊢ plus (z, x) = x
Tactic:
exact heq
Proof state after:
no goals
Theorem: zero_plus_x_eq_eq
Proof state before:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
⊢ z ∈ A
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
⊢ plus (z, z) = z
Theorem: zero_plus_x_eq_eq
Proof state before:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
⊢ plus (z, z) = z
Tactic:
exact zplus z
Proof state after:
no goals
Theorem: zero_plus_x_eq_eq
Proof state before:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
⊢ ∀ n ∈ A, S n ∈ A
Tactic:
intros n hel
Proof state after:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ S n ∈ A
Theorem: zero_plus_x_eq_eq
Proof state before:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ S n ∈ A
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
x : ↑N0
A : Set ↑N0 := {b | plus (z, b) = b}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ plus (z, S n) = S n