internlm/Lean-Github huggingface dataset:
Theorem: inter_rectangles
Proof state before:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)
h1 : 0 ≤ 0 → 0 ≤ 1 → (0, 0) ≤ x ∧ x ≤ (1, 0)
⊢ x ∈ Set.singleton (1, 0)
Tactic:
have h2 := imp 1
Proof state after:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)
h1 : 0 ≤ 0 → 0 ≤ 1 → (0, 0) ≤ x ∧ x ≤ (1, 0)
h2 : 0 ≤ 1 → 1 ≤ 1 → (1, 0) ≤ x ∧ x ≤ (1, 1)
⊢ x ∈ Set.singleton (1, 0)
Theorem: inter_rectangles
Proof state before:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)
h1 : 0 ≤ 0 → 0 ≤ 1 → (0, 0) ≤ x ∧ x ≤ (1, 0)
h2 : 0 ≤ 1 → 1 ≤ 1 → (1, 0) ≤ x ∧ x ≤ (1, 1)
⊢ x ∈ Set.singleton (1, 0)
Tactic:
simp [Prod.le_def] at *
Proof state after:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ i
h1 : (0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 0
h2 : (1 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 1
⊢ x ∈ Set.singleton (1, 0)
Theorem: inter_rectangles
Proof state before:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ i
h1 : (0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 0
h2 : (1 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 1
⊢ x ∈ Set.singleton (1, 0)
Tactic:
have hx1 : x.1 = 1 := by
  linarith
Proof state after:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ i
h1 : (0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 0
h2 : (1 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 1
hx1 : x.1 = 1
⊢ x ∈ Set.singleton (1, 0)
Theorem: inter_rectangles
Proof state before:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ i
h1 : (0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 0
h2 : (1 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 1
hx1 : x.1 = 1
⊢ x ∈ Set.singleton (1, 0)
Tactic:
have hx2 : x.2 = 0 := by
  linarith
Proof state after:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ i
h1 : (0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 0
h2 : (1 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 1
hx1 : x.1 = 1
hx2 : x.2 = 0
⊢ x ∈ Set.singleton (1, 0)
Theorem: inter_rectangles
Proof state before:
case mp
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ i
h1 : (0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 0
h2 : (1 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 1
hx1 : x.1 = 1
hx2 : x.2 = 0
⊢ x ∈ Set.singleton (1, 0)
Tactic:
exact Set.mem_singleton_of_eq (Prod.ext hx1 hx2)
Proof state after:
no goals
Theorem: inter_rectangles
Proof state before:
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ i
h1 : (0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 0
h2 : (1 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 1
⊢ x.1 = 1
Tactic:
linarith
Proof state after:
no goals
Theorem: inter_rectangles
Proof state before:
x : ℝ × ℝ
imp : ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ i
h1 : (0 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 0
h2 : (1 ≤ x.1 ∧ 0 ≤ x.2) ∧ x.1 ≤ 1 ∧ x.2 ≤ 1
hx1 : x.1 = 1
⊢ x.2 = 0
Tactic:
linarith
Proof state after:
no goals
Theorem: inter_rectangles
Proof state before:
case mpr
x : ℝ × ℝ
⊢ x ∈ Set.singleton (1, 0) → ∀ (i : ℝ), 0 ≤ i → i ≤ 1 → (i, 0) ≤ x ∧ x ≤ (1, i)
Tactic:
intros mem i hle0i hlei1
Proof state after:
case mpr
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
⊢ (i, 0) ≤ x ∧ x ≤ (1, i)
Theorem: inter_rectangles
Proof state before:
case mpr
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
⊢ (i, 0) ≤ x ∧ x ≤ (1, i)
Tactic:
have mem' := Set.eq_of_mem_singleton mem
Proof state after:
case mpr
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (i, 0) ≤ x ∧ x ≤ (1, i)
Theorem: inter_rectangles
Proof state before:
case mpr
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (i, 0) ≤ x ∧ x ≤ (1, i)
Tactic:
constructor
Proof state after:
case mpr.left
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (i, 0) ≤ x

case mpr.right
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ x ≤ (1, i)
Theorem: inter_rectangles
Proof state before:
case mpr.left
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (i, 0) ≤ x
Tactic:
rw [mem']
Proof state after:
case mpr.left
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (i, 0) ≤ (1, 0)
Theorem: inter_rectangles
Proof state before:
case mpr.left
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (i, 0) ≤ (1, 0)
Tactic:
simp [Prod.le_def]
Proof state after:
case mpr.left
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ i ≤ 1
Theorem: inter_rectangles
Proof state before:
case mpr.left
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ i ≤ 1
Tactic:
exact hlei1
Proof state after:
no goals
Theorem: inter_rectangles
Proof state before:
case mpr.right
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ x ≤ (1, i)
Tactic:
rw [mem']
Proof state after:
case mpr.right
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (1, 0) ≤ (1, i)
Theorem: inter_rectangles
Proof state before:
case mpr.right
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ (1, 0) ≤ (1, i)
Tactic:
simp
Proof state after:
case mpr.right
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ 0 ≤ i
Theorem: inter_rectangles
Proof state before:
case mpr.right
x : ℝ × ℝ
mem : x ∈ Set.singleton (1, 0)
i : ℝ
hle0i : 0 ≤ i
hlei1 : i ≤ 1
mem' : x = (1, 0)
⊢ 0 ≤ i
Tactic:
exact hle0i
Proof state after:
no goals
Theorem: prod_bin_real_uncountable
Proof state before:
⊢ Uncountable ({0, 1} ×ˢ Set.univ)
Tactic:
have hucnt
  : ¬(Set.Countable (({0, 1} : Set ℕ) ×ˢ (Set.univ : Set ℝ))) := by
  intro hcnt
  have hun : ({0, 1} : Set ℕ) = {0} ∪ {1} := by
    rw [Set.union_comm, Set.union_singleton]
  rw [hun] at hcnt
  simp_rw
    [Set.union_prod,
     Set.countable_union,
     Set.countable_iff_exists_injective] at hcnt
  rcases hcnt with ⟨⟨f, finj⟩⟩
  let g : ↑(Set.univ : Set ℝ) → ({0} ×ˢ (Set.univ : Set ℝ))
    := λ r => ⟨((0 : ℕ), r), by simp⟩
  have ginj : Function.Injective g := by
    intro a b heq
    simp only [Subtype.mk.injEq, Prod.mk.injEq, true_and] at heq
    exact SetCoe.ext heq
  let fg : ↑(Set.univ : Set ℝ) → ℕ := f ∘ g
  have fginj := Function.Injective.comp finj ginj
  exact Cardinal.not_countable_real (Set.countable_iff_exists_injective.mpr ⟨fg, fginj⟩)
Proof state after:
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
⊢ Uncountable ({0, 1} ×ˢ Set.univ)
Theorem: prod_bin_real_uncountable
Proof state before:
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
⊢ Uncountable ({0, 1} ×ˢ Set.univ)
Tactic:
constructor
Proof state after:
case left
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
⊢ ¬Set.Countable ({0, 1} ×ˢ Set.univ)

case right
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
⊢ Set.Infinite ({0, 1} ×ˢ Set.univ)
Theorem: prod_bin_real_uncountable
Proof state before:
⊢ ¬Set.Countable ({0, 1} ×ˢ Set.univ)
Tactic:
intro hcnt
Proof state after:
hcnt : Set.Countable ({0, 1} ×ˢ Set.univ)
⊢ False
Theorem: prod_bin_real_uncountable
Proof state before:
hcnt : Set.Countable ({0, 1} ×ˢ Set.univ)
⊢ False
Tactic:
have hun : ({0, 1} : Set ℕ) = {0} ∪ {1} := by
  rw [Set.union_comm, Set.union_singleton]
Proof state after:
hcnt : Set.Countable ({0, 1} ×ˢ Set.univ)
hun : {0, 1} = {0} ∪ {1}
⊢ False
Theorem: prod_bin_real_uncountable
Proof state before:
hcnt : Set.Countable ({0, 1} ×ˢ Set.univ)
hun : {0, 1} = {0} ∪ {1}
⊢ False
Tactic:
rw [hun] at hcnt
Proof state after:
hcnt : Set.Countable (({0} ∪ {1}) ×ˢ Set.univ)
hun : {0, 1} = {0} ∪ {1}
⊢ False
Theorem: prod_bin_real_uncountable
Proof state before:
hcnt : Set.Countable (({0} ∪ {1}) ×ˢ Set.univ)
hun : {0, 1} = {0} ∪ {1}
⊢ False
Tactic:
simp_rw
  [Set.union_prod,
   Set.countable_union,
   Set.countable_iff_exists_injective] at hcnt
Proof state after:
hun : {0, 1} = {0} ∪ {1}
hcnt : (∃ f, Function.Injective f) ∧ ∃ f, Function.Injective f
⊢ False
Theorem: prod_bin_real_uncountable
Proof state before:
hun : {0, 1} = {0} ∪ {1}
hcnt : (∃ f, Function.Injective f) ∧ ∃ f, Function.Injective f
⊢ False
Tactic:
rcases hcnt with ⟨⟨f, finj⟩⟩
Proof state after:
case intro.intro
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
⊢ False
Theorem: prod_bin_real_uncountable
Proof state before:
case intro.intro
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
⊢ False
Tactic:
let g : ↑(Set.univ : Set ℝ) → ({0} ×ˢ (Set.univ : Set ℝ))
  := λ r => ⟨((0 : ℕ), r), by simp⟩
Proof state after:
case intro.intro
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
g : ↑Set.univ → ↑({0} ×ˢ Set.univ) := fun r => { val := (0, ↑r), property := (_ : (0, ↑r) ∈ {0} ×ˢ Set.univ) }
⊢ False
Theorem: prod_bin_real_uncountable
Proof state before:
case intro.intro
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
g : ↑Set.univ → ↑({0} ×ˢ Set.univ) := fun r => { val := (0, ↑r), property := (_ : (0, ↑r) ∈ {0} ×ˢ Set.univ) }
⊢ False
Tactic:
have ginj : Function.Injective g := by
  intro a b heq
  simp only [Subtype.mk.injEq, Prod.mk.injEq, true_and] at heq
  exact SetCoe.ext heq
Proof state after:
case intro.intro
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
g : ↑Set.univ → ↑({0} ×ˢ Set.univ) := fun r => { val := (0, ↑r), property := (_ : (0, ↑r) ∈ {0} ×ˢ Set.univ) }
ginj : Function.Injective g
⊢ False
Theorem: prod_bin_real_uncountable
Proof state before:
case intro.intro
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
g : ↑Set.univ → ↑({0} ×ˢ Set.univ) := fun r => { val := (0, ↑r), property := (_ : (0, ↑r) ∈ {0} ×ˢ Set.univ) }
ginj : Function.Injective g
⊢ False
Tactic:
let fg : ↑(Set.univ : Set ℝ) → ℕ := f ∘ g
Proof state after:
case intro.intro
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
g : ↑Set.univ → ↑({0} ×ˢ Set.univ) := fun r => { val := (0, ↑r), property := (_ : (0, ↑r) ∈ {0} ×ˢ Set.univ) }
ginj : Function.Injective g
fg : ↑Set.univ → ℕ := f ∘ g
⊢ False
Theorem: prod_bin_real_uncountable
Proof state before:
case intro.intro
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
g : ↑Set.univ → ↑({0} ×ˢ Set.univ) := fun r => { val := (0, ↑r), property := (_ : (0, ↑r) ∈ {0} ×ˢ Set.univ) }
ginj : Function.Injective g
fg : ↑Set.univ → ℕ := f ∘ g
⊢ False
Tactic:
have fginj := Function.Injective.comp finj ginj
Proof state after:
case intro.intro
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
g : ↑Set.univ → ↑({0} ×ˢ Set.univ) := fun r => { val := (0, ↑r), property := (_ : (0, ↑r) ∈ {0} ×ˢ Set.univ) }
ginj : Function.Injective g
fg : ↑Set.univ → ℕ := f ∘ g
fginj : Function.Injective (f ∘ g)
⊢ False
Theorem: prod_bin_real_uncountable
Proof state before:
case intro.intro
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
g : ↑Set.univ → ↑({0} ×ˢ Set.univ) := fun r => { val := (0, ↑r), property := (_ : (0, ↑r) ∈ {0} ×ˢ Set.univ) }
ginj : Function.Injective g
fg : ↑Set.univ → ℕ := f ∘ g
fginj : Function.Injective (f ∘ g)
⊢ False
Tactic:
exact Cardinal.not_countable_real (Set.countable_iff_exists_injective.mpr ⟨fg, fginj⟩)
Proof state after:
no goals
Theorem: prod_bin_real_uncountable
Proof state before:
hcnt : Set.Countable ({0, 1} ×ˢ Set.univ)
⊢ {0, 1} = {0} ∪ {1}
Tactic:
rw [Set.union_comm, Set.union_singleton]
Proof state after:
no goals
Theorem: prod_bin_real_uncountable
Proof state before:
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
r : ↑Set.univ
⊢ (0, ↑r) ∈ {0} ×ˢ Set.univ
Tactic:
simp
Proof state after:
no goals
Theorem: prod_bin_real_uncountable
Proof state before:
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
g : ↑Set.univ → ↑({0} ×ˢ Set.univ) := fun r => { val := (0, ↑r), property := (_ : (0, ↑r) ∈ {0} ×ˢ Set.univ) }
⊢ Function.Injective g
Tactic:
intro a b heq
Proof state after:
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
g : ↑Set.univ → ↑({0} ×ˢ Set.univ) := fun r => { val := (0, ↑r), property := (_ : (0, ↑r) ∈ {0} ×ˢ Set.univ) }
a b : ↑Set.univ
heq : g a = g b
⊢ a = b
Theorem: prod_bin_real_uncountable
Proof state before:
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
g : ↑Set.univ → ↑({0} ×ˢ Set.univ) := fun r => { val := (0, ↑r), property := (_ : (0, ↑r) ∈ {0} ×ˢ Set.univ) }
a b : ↑Set.univ
heq : g a = g b
⊢ a = b
Tactic:
simp only [Subtype.mk.injEq, Prod.mk.injEq, true_and] at heq
Proof state after:
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
g : ↑Set.univ → ↑({0} ×ˢ Set.univ) := fun r => { val := (0, ↑r), property := (_ : (0, ↑r) ∈ {0} ×ˢ Set.univ) }
a b : ↑Set.univ
heq : ↑a = ↑b
⊢ a = b
Theorem: prod_bin_real_uncountable
Proof state before:
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
g : ↑Set.univ → ↑({0} ×ˢ Set.univ) := fun r => { val := (0, ↑r), property := (_ : (0, ↑r) ∈ {0} ×ˢ Set.univ) }
a b : ↑Set.univ
heq : ↑a = ↑b
⊢ a = b
Tactic:
exact SetCoe.ext heq
Proof state after:
no goals
Theorem: prod_bin_real_uncountable
Proof state before:
case left
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
⊢ ¬Set.Countable ({0, 1} ×ˢ Set.univ)
Tactic:
exact hucnt
Proof state after:
no goals
Theorem: prod_bin_real_uncountable
Proof state before:
case right
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
⊢ Set.Infinite ({0, 1} ×ˢ Set.univ)
Tactic:
have hncnt {α : Type} {s : Set α}
  : ¬Set.Countable s → Set.Infinite s := by
  contrapose
  simp only [Set.mem_singleton_iff, Set.not_infinite, not_not, Set.Finite.countable]
  exact Set.Finite.countable
Proof state after:
case right
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
hncnt : ∀ {α : Type} {s : Set α}, ¬Set.Countable s → Set.Infinite s
⊢ Set.Infinite ({0, 1} ×ˢ Set.univ)
Theorem: prod_bin_real_uncountable
Proof state before:
case right
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
hncnt : ∀ {α : Type} {s : Set α}, ¬Set.Countable s → Set.Infinite s
⊢ Set.Infinite ({0, 1} ×ˢ Set.univ)
Tactic:
exact hncnt hucnt
Proof state after:
no goals
Theorem: prod_bin_real_uncountable
Proof state before:
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
α : Type
s : Set α
⊢ ¬Set.Countable s → Set.Infinite s
Tactic:
contrapose
Proof state after:
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
α : Type
s : Set α
⊢ ¬Set.Infinite s → ¬¬Set.Countable s
Theorem: prod_bin_real_uncountable
Proof state before:
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
α : Type
s : Set α
⊢ ¬Set.Infinite s → ¬¬Set.Countable s
Tactic:
simp only [Set.mem_singleton_iff, Set.not_infinite, not_not, Set.Finite.countable]
Proof state after:
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
α : Type
s : Set α
⊢ Set.Finite s → Set.Countable s
Theorem: prod_bin_real_uncountable
Proof state before:
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
α : Type
s : Set α
⊢ Set.Finite s → Set.Countable s
Tactic:
exact Set.Finite.countable
Proof state after:
no goals
Theorem: uncountable_minus_countably_infinite_uncountable
Proof state before:
α : Type
A B : Set α
hsub : A ⊆ B
hcntiA : Countably_Infinite A
hucnt : Uncountable B
⊢ Uncountable (B \ A)
Tactic:
rcases hcntiA with ⟨hcntA, _⟩
Proof state after:
case intro
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
⊢ Uncountable (B \ A)
Theorem: uncountable_minus_countably_infinite_uncountable
Proof state before:
case intro
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
⊢ Uncountable (B \ A)
Tactic:
constructor
Proof state after:
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
⊢ ¬Set.Countable (B \ A)

case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
⊢ Set.Infinite (B \ A)
Theorem: uncountable_minus_countably_infinite_uncountable
Proof state before:
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
⊢ ¬Set.Countable (B \ A)
Tactic:
intro hcntmin
Proof state after:
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hcntmin : Set.Countable (B \ A)
⊢ False
Theorem: uncountable_minus_countably_infinite_uncountable
Proof state before:
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hcntmin : Set.Countable (B \ A)
⊢ False
Tactic:
have hcntB := Set.Countable.union hcntA hcntmin
Proof state after:
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hcntmin : Set.Countable (B \ A)
hcntB : Set.Countable (A ∪ B \ A)
⊢ False
Theorem: uncountable_minus_countably_infinite_uncountable
Proof state before:
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hcntmin : Set.Countable (B \ A)
hcntB : Set.Countable (A ∪ B \ A)
⊢ False
Tactic:
rw [Set.union_diff_cancel hsub] at hcntB
Proof state after:
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hcntmin : Set.Countable (B \ A)
hcntB : Set.Countable B
⊢ False
Theorem: uncountable_minus_countably_infinite_uncountable
Proof state before:
case intro.left
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hcntmin : Set.Countable (B \ A)
hcntB : Set.Countable B
⊢ False
Tactic:
exact hucnt.1 hcntB
Proof state after:
no goals
Theorem: uncountable_minus_countably_infinite_uncountable
Proof state before:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
⊢ Set.Infinite (B \ A)
Tactic:
intro hfin
Proof state after:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hfin : Set.Finite (B \ A)
⊢ False
Theorem: uncountable_minus_countably_infinite_uncountable
Proof state before:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hfin : Set.Finite (B \ A)
⊢ False
Tactic:
have hcnt := Set.Finite.countable hfin
Proof state after:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hfin : Set.Finite (B \ A)
hcnt : Set.Countable (B \ A)
⊢ False
Theorem: uncountable_minus_countably_infinite_uncountable
Proof state before:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hfin : Set.Finite (B \ A)
hcnt : Set.Countable (B \ A)
⊢ False
Tactic:
have hcntB := Set.Countable.union hcntA hcnt
Proof state after:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hfin : Set.Finite (B \ A)
hcnt : Set.Countable (B \ A)
hcntB : Set.Countable (A ∪ B \ A)
⊢ False
Theorem: uncountable_minus_countably_infinite_uncountable
Proof state before:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hfin : Set.Finite (B \ A)
hcnt : Set.Countable (B \ A)
hcntB : Set.Countable (A ∪ B \ A)
⊢ False
Tactic:
rw [Set.union_diff_cancel hsub] at hcntB
Proof state after:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hfin : Set.Finite (B \ A)
hcnt : Set.Countable (B \ A)
hcntB : Set.Countable B
⊢ False
Theorem: uncountable_minus_countably_infinite_uncountable
Proof state before:
case intro.right
α : Type
A B : Set α
hsub : A ⊆ B
hucnt : Uncountable B
hcntA : Set.Countable A
right✝ : Set.Infinite A
hfin : Set.Finite (B \ A)
hcnt : Set.Countable (B \ A)
hcntB : Set.Countable B
⊢ False
Tactic:
exact hucnt.1 hcntB
Proof state after:
no goals
Theorem: indicator_card_gt_real_card
Proof state before:
⊢ Cardinal.mk ↑indicator > Cardinal.mk ↑Set.univ
Tactic:
simp only [Cardinal.mk_univ, indicator]
Proof state after:
⊢ Cardinal.mk (ℝ → ↑binary') > Cardinal.mk ℝ
Theorem: indicator_card_gt_real_card
Proof state before:
⊢ Cardinal.mk (ℝ → ↑binary') > Cardinal.mk ℝ
Tactic:
rw [binary', ←Cardinal.power_def, Cardinal.mk_insert (by simp), Cardinal.mk_singleton]
Proof state after:
⊢ (1 + 1) ^ Cardinal.mk ℝ > Cardinal.mk ℝ
Theorem: indicator_card_gt_real_card
Proof state before:
⊢ (1 + 1) ^ Cardinal.mk ℝ > Cardinal.mk ℝ
Tactic:
ring_nf
Proof state after:
⊢ 2 ^ Cardinal.mk ℝ > Cardinal.mk ℝ
Theorem: indicator_card_gt_real_card
Proof state before:
⊢ 2 ^ Cardinal.mk ℝ > Cardinal.mk ℝ
Tactic:
exact Cardinal.cantor (Cardinal.mk ℝ)
Proof state after:
no goals
Theorem: indicator_card_gt_real_card
Proof state before:
⊢ 0 ∉ {1}
Tactic:
simp
Proof state after:
no goals
Theorem: binary'_zero_eq_iff_one_eq
Proof state before:
b : ↑binary'
hb : ¬↑b = 1
⊢ ↑b = 0
Tactic:
rcases b with ⟨hv, hp⟩
Proof state after:
case mk
hv : ℕ
hp : hv ∈ binary'
hb : ¬↑{ val := hv, property := hp } = 1
⊢ ↑{ val := hv, property := hp } = 0
Theorem: binary'_zero_eq_iff_one_eq
Proof state before:
case mk
hv : ℕ
hp : hv ∈ binary'
hb : ¬↑{ val := hv, property := hp } = 1
⊢ ↑{ val := hv, property := hp } = 0
Tactic:
dsimp only at *
Proof state after:
case mk
hv : ℕ
hp : hv ∈ binary'
hb : ¬hv = 1
⊢ hv = 0
Theorem: binary'_zero_eq_iff_one_eq
Proof state before:
case mk
hv : ℕ
hp : hv ∈ binary'
hb : ¬hv = 1
⊢ hv = 0
Tactic:
rw [binary'] at hp
Proof state after:
case mk
hv : ℕ
hp : hv ∈ {0, 1}
hb : ¬hv = 1
⊢ hv = 0
Theorem: binary'_zero_eq_iff_one_eq
Proof state before:
case mk
hv : ℕ
hp : hv ∈ {0, 1}
hb : ¬hv = 1
⊢ hv = 0
Tactic:
simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at hp
Proof state after:
case mk
hv : ℕ
hb : ¬hv = 1
hp : hv = 0 ∨ hv = 1
⊢ hv = 0
Theorem: binary'_zero_eq_iff_one_eq
Proof state before:
case mk
hv : ℕ
hb : ¬hv = 1
hp : hv = 0 ∨ hv = 1
⊢ hv = 0
Tactic:
rcases hp with (h0 | h1)
Proof state after:
case mk.inl
hv : ℕ
hb : ¬hv = 1
h0 : hv = 0
⊢ hv = 0

case mk.inr
hv : ℕ
hb : ¬hv = 1
h1 : hv = 1
⊢ hv = 0
Theorem: binary'_zero_eq_iff_one_eq
Proof state before:
case mk.inl
hv : ℕ
hb : ¬hv = 1
h0 : hv = 0
⊢ hv = 0
Tactic:
exact h0
Proof state after:
no goals
Theorem: binary'_zero_eq_iff_one_eq
Proof state before:
case mk.inr
hv : ℕ
hb : ¬hv = 1
h1 : hv = 1
⊢ hv = 0
Tactic:
exfalso
Proof state after:
case mk.inr.h
hv : ℕ
hb : ¬hv = 1
h1 : hv = 1
⊢ False
Theorem: binary'_zero_eq_iff_one_eq
Proof state before:
case mk.inr.h
hv : ℕ
hb : ¬hv = 1
h1 : hv = 1
⊢ False
Tactic:
exact hb h1
Proof state after:
no goals
Theorem: binary_zero_eq_iff_one_eq
Proof state before:
a b : binary
hb : b = binary.one ↔ a = binary.one
⊢ b = binary.zero ↔ a = binary.zero
Tactic:
cases b
Proof state after:
case zero
a : binary
hb : binary.zero = binary.one ↔ a = binary.one
⊢ binary.zero = binary.zero ↔ a = binary.zero

case one
a : binary
hb : binary.one = binary.one ↔ a = binary.one
⊢ binary.one = binary.zero ↔ a = binary.zero
Theorem: binary_zero_eq_iff_one_eq
Proof state before:
case zero
a : binary
hb : binary.zero = binary.one ↔ a = binary.one
⊢ binary.zero = binary.zero ↔ a = binary.zero
Tactic:
simp only [false_iff, forall_true_left] at *
Proof state after:
case zero
a : binary
hb : ¬a = binary.one
⊢ True ↔ a = binary.zero