Theorem: HTPI.Cantor's_theorem (HTPILib/Chap8Part2.lean)

State before:
⊢ ¬ctble (𝒫 Univ ℕ)
Tactic:
by_contra h1
State after:
h1 : ctble (𝒫 Univ ℕ)
⊢ False

State before:
h1 : ctble (𝒫 Univ ℕ)
⊢ False
Tactic:
rewrite [Theorem_8_1_5_2] at h1
State after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
⊢ False

State before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
⊢ False
Tactic:
obtain (R : Rel Nat (Set Nat))
  (h2 : fcnl_onto_from_nat R (𝒫 (Univ Nat))) from h1
State after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : fcnl_onto_from_nat R (𝒫 Univ ℕ)
⊢ False

State before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : fcnl_onto_from_nat R (𝒫 Univ ℕ)
⊢ False
Tactic:
define at h2
State after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
⊢ False

State before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
⊢ False
Tactic:
have h3 : unique_val_on_N R := h2.left
State after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
⊢ False

State before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
⊢ False
Tactic:
have h4 : nat_rel_onto R (𝒫 (Univ Nat)) := h2.right
State after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : nat_rel_onto R (𝒫 Univ ℕ)
⊢ False

State before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : nat_rel_onto R (𝒫 Univ ℕ)
⊢ False
Tactic:
set D : Set Nat := {n : Nat | ∃ (X : Set Nat), R n X ∧ n ∉ X}
State after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : nat_rel_onto R (𝒫 Univ ℕ)
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
⊢ False

State before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : nat_rel_onto R (𝒫 Univ ℕ)
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
⊢ False
Tactic:
have h5 : D ∈ 𝒫 (Univ Nat) := set_elt_powerset_univ D
State after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : nat_rel_onto R (𝒫 Univ ℕ)
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
⊢ False

State before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : nat_rel_onto R (𝒫 Univ ℕ)
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
⊢ False
Tactic:
define at h4
State after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
⊢ False

State before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
⊢ False
Tactic:
obtain (n : Nat) (h6 : R n D) from h4 h5
State after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
⊢ False

State before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
⊢ False
Tactic:
by_cases h7 : n ∈ D
State after:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∈ D
⊢ False

case neg
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∉ D
⊢ False

State before:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∈ D
⊢ False
Tactic:
contradict h7
State after:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∈ D
⊢ n ∉ D

State before:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∈ D
⊢ n ∉ D
Tactic:
define at h7
State after:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
⊢ n ∉ D

State before:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
⊢ n ∉ D
Tactic:
obtain (X : Set Nat) (h8 : R n X ∧ n ∉ X) from h7
State after:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
X : Set ℕ
h8 : R n X ∧ n ∉ X
⊢ n ∉ D

State before:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
X : Set ℕ
h8 : R n X ∧ n ∉ X
⊢ n ∉ D
Tactic:
define at h3
State after:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set ℕ⦄, R n x1 → R n x2 → x1 = x2
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
X : Set ℕ
h8 : R n X ∧ n ∉ X
⊢ n ∉ D

State before:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set ℕ⦄, R n x1 → R n x2 → x1 = x2
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
X : Set ℕ
h8 : R n X ∧ n ∉ X
⊢ n ∉ D
Tactic:
have h9 : D = X := h3 h6 h8.left
State after:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set ℕ⦄, R n x1 → R n x2 → x1 = x2
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
X : Set ℕ
h8 : R n X ∧ n ∉ X
h9 : D = X
⊢ n ∉ D

State before:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set ℕ⦄, R n x1 → R n x2 → x1 = x2
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
X : Set ℕ
h8 : R n X ∧ n ∉ X
h9 : D = X
⊢ n ∉ D
Tactic:
rewrite [h9]
State after:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set ℕ⦄, R n x1 → R n x2 → x1 = x2
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
X : Set ℕ
h8 : R n X ∧ n ∉ X
h9 : D = X
⊢ n ∉ X

State before:
case pos
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : ∀ ⦃n : ℕ⦄ ⦃x1 x2 : Set ℕ⦄, R n x1 → R n x2 → x1 = x2
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : ∃ X, R n X ∧ n ∉ X
X : Set ℕ
h8 : R n X ∧ n ∉ X
h9 : D = X
⊢ n ∉ X
Tactic:
show n ∉ X from h8.right
State after:
no goals

State before:
case neg
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∉ D
⊢ False
Tactic:
contradict h7
State after:
case neg
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∉ D
⊢ n ∈ D

State before:
case neg
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∉ D
⊢ n ∈ D
Tactic:
define
State after:
case neg
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∉ D
⊢ ∃ X, R n X ∧ n ∉ X

State before:
case neg
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
h3 : unique_val_on_N R
h4 : ∀ ⦃x : Set ℕ⦄, x ∈ 𝒫 Univ ℕ → ∃ n, R n x
D : Set ℕ := {n | ∃ X, R n X ∧ n ∉ X}
h5 : D ∈ 𝒫 Univ ℕ
n : ℕ
h6 : R n D
h7 : n ∉ D
⊢ ∃ X, R n X ∧ n ∉ X
Tactic:
show ∃ (X : Set Nat), R n X ∧ n ∉ X from
  Exists.intro D (And.intro h6 h7)
State after:
no goals