Theorem: prod_bin_real_uncountable (meetings/ex5.lean)

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⟩)
State after:
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
⊢ Uncountable ({0, 1} ×ˢ Set.univ)

State before:
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
⊢ Uncountable ({0, 1} ×ˢ Set.univ)
Tactic:
constructor
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)

State before:
⊢ ¬Set.Countable ({0, 1} ×ˢ Set.univ)
Tactic:
intro hcnt
State after:
hcnt : Set.Countable ({0, 1} ×ˢ Set.univ)
⊢ False

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]
State after:
hcnt : Set.Countable ({0, 1} ×ˢ Set.univ)
hun : {0, 1} = {0} ∪ {1}
⊢ False

State before:
hcnt : Set.Countable ({0, 1} ×ˢ Set.univ)
hun : {0, 1} = {0} ∪ {1}
⊢ False
Tactic:
rw [hun] at hcnt
State after:
hcnt : Set.Countable (({0} ∪ {1}) ×ˢ Set.univ)
hun : {0, 1} = {0} ∪ {1}
⊢ False

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
State after:
hun : {0, 1} = {0} ∪ {1}
hcnt : (∃ f, Function.Injective f) ∧ ∃ f, Function.Injective f
⊢ False

State before:
hun : {0, 1} = {0} ∪ {1}
hcnt : (∃ f, Function.Injective f) ∧ ∃ f, Function.Injective f
⊢ False
Tactic:
rcases hcnt with ⟨⟨f, finj⟩⟩
State after:
case intro.intro
hun : {0, 1} = {0} ∪ {1}
right✝ : ∃ f, Function.Injective f
f : ↑({0} ×ˢ Set.univ) → ℕ
finj : Function.Injective f
⊢ False

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

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

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

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

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

State before:
hcnt : Set.Countable ({0, 1} ×ˢ Set.univ)
⊢ {0, 1} = {0} ∪ {1}
Tactic:
rw [Set.union_comm, Set.union_singleton]
State after:
no goals

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

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

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

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

State before:
case left
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
⊢ ¬Set.Countable ({0, 1} ×ˢ Set.univ)
Tactic:
exact hucnt
State after:
no goals

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

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

State before:
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
α : Type
s : Set α
⊢ ¬Set.Countable s → Set.Infinite s
Tactic:
contrapose
State after:
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
α : Type
s : Set α
⊢ ¬Set.Infinite s → ¬¬Set.Countable s

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]
State after:
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
α : Type
s : Set α
⊢ Set.Finite s → Set.Countable s

State before:
hucnt : ¬Set.Countable ({0, 1} ×ˢ Set.univ)
α : Type
s : Set α
⊢ Set.Finite s → Set.Countable s
Tactic:
exact Set.Finite.countable
State after:
no goals