Theorem: HTPI.Theorem_8_2_1_1 (HTPILib/Chap8Part2.lean)

State before:
U V : Type
A : Set U
B : Set V
h1 : ctble A
h2 : ctble B
⊢ ctble (A ×ₛ B)
Tactic:
rewrite [ctble_iff_equinum_set_nat] at h1
State after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ctble B
⊢ ctble (A ×ₛ B)

State before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ctble B
⊢ ctble (A ×ₛ B)
Tactic:
rewrite [ctble_iff_equinum_set_nat] at h2
State after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
⊢ ctble (A ×ₛ B)

State before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
⊢ ctble (A ×ₛ B)
Tactic:
obtain (I : Set Nat) (h3 : I ∼ A) from h1
State after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
⊢ ctble (A ×ₛ B)

State before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
⊢ ctble (A ×ₛ B)
Tactic:
obtain (J : Set Nat) (h4 : J ∼ B) from h2
State after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
⊢ ctble (A ×ₛ B)

State before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
⊢ ctble (A ×ₛ B)
Tactic:
have h5 : I ×ₛ J ∼ A ×ₛ B := Theorem_8_1_2_1 h3 h4
State after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
⊢ ctble (A ×ₛ B)

State before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
⊢ ctble (A ×ₛ B)
Tactic:
have h6 : I ×ₛ J ⊆ Univ (Nat × Nat) := by
  fix p : Nat × Nat
  assume h6 : p ∈ I ×ₛ J
  show p ∈ Univ (Nat × Nat) from elt_Univ p
  done
State after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ ctble (A ×ₛ B)

State before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ ctble (A ×ₛ B)
Tactic:
have h7 : ctble (Univ (Nat × Nat)) := by
  define   apply Or.inr
  rewrite [denum_def]
  show Univ Nat ∼ Univ (Nat × Nat) from Theorem_8_1_3_2 NxN_equinum_N
  done
State after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
h7 : ctble (Univ (ℕ × ℕ))
⊢ ctble (A ×ₛ B)

State before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
h7 : ctble (Univ (ℕ × ℕ))
⊢ ctble (A ×ₛ B)
Tactic:
have h8 : ctble (I ×ₛ J) := Exercise_8_1_17 h6 h7
State after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
h7 : ctble (Univ (ℕ × ℕ))
h8 : ctble (I ×ₛ J)
⊢ ctble (A ×ₛ B)

State before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
h7 : ctble (Univ (ℕ × ℕ))
h8 : ctble (I ×ₛ J)
⊢ ctble (A ×ₛ B)
Tactic:
show ctble (A ×ₛ B) from ctble_of_equinum_ctble h5 h8
State after:
no goals

State before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
⊢ I ×ₛ J ⊆ Univ (ℕ × ℕ)
Tactic:
fix p : Nat × Nat
State after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
p : ℕ × ℕ
⊢ p ∈ I ×ₛ J → p ∈ Univ (ℕ × ℕ)

State before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
p : ℕ × ℕ
⊢ p ∈ I ×ₛ J → p ∈ Univ (ℕ × ℕ)
Tactic:
assume h6 : p ∈ I ×ₛ J
State after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
p : ℕ × ℕ
h6 : p ∈ I ×ₛ J
⊢ p ∈ Univ (ℕ × ℕ)

State before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
p : ℕ × ℕ
h6 : p ∈ I ×ₛ J
⊢ p ∈ Univ (ℕ × ℕ)
Tactic:
show p ∈ Univ (Nat × Nat) from elt_Univ p
State after:
no goals

State before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ ctble (Univ (ℕ × ℕ))
Tactic:
define
State after:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ finite (Univ (ℕ × ℕ)) ∨ denum (Univ (ℕ × ℕ))

State before:
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ finite (Univ (ℕ × ℕ)) ∨ denum (Univ (ℕ × ℕ))
Tactic:
apply Or.inr
State after:
case h
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ denum (Univ (ℕ × ℕ))

State before:
case h
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ denum (Univ (ℕ × ℕ))
Tactic:
rewrite [denum_def]
State after:
case h
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ Univ ℕ ∼ Univ (ℕ × ℕ)

State before:
case h
U V : Type
A : Set U
B : Set V
h1 : ∃ I, I ∼ A
h2 : ∃ I, I ∼ B
I : Set ℕ
h3 : I ∼ A
J : Set ℕ
h4 : J ∼ B
h5 : I ×ₛ J ∼ A ×ₛ B
h6 : I ×ₛ J ⊆ Univ (ℕ × ℕ)
⊢ Univ ℕ ∼ Univ (ℕ × ℕ)
Tactic:
show Univ Nat ∼ Univ (Nat × Nat) from Theorem_8_1_3_2 NxN_equinum_N
State after:
no goals