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

State before:
U : Type
A : Set U
⊢ ctble A ↔ ∃ I, I ∼ A
Tactic:
apply Iff.intro
State after:
case mp
U : Type
A : Set U
⊢ ctble A → ∃ I, I ∼ A

case mpr
U : Type
A : Set U
⊢ (∃ I, I ∼ A) → ctble A

State before:
case mp
U : Type
A : Set U
⊢ ctble A → ∃ I, I ∼ A
Tactic:
assume h1 : ctble A
State after:
case mp
U : Type
A : Set U
h1 : ctble A
⊢ ∃ I, I ∼ A

State before:
case mp
U : Type
A : Set U
h1 : ctble A
⊢ ∃ I, I ∼ A
Tactic:
define at h1
State after:
case mp
U : Type
A : Set U
h1 : finite A ∨ denum A
⊢ ∃ I, I ∼ A

State before:
case mp
U : Type
A : Set U
h1 : finite A ∨ denum A
⊢ ∃ I, I ∼ A
Tactic:
by_cases on h1
State after:
case mp.Case_1
U : Type
A : Set U
h1 : finite A
⊢ ∃ I, I ∼ A

case mp.Case_2
U : Type
A : Set U
h1 : denum A
⊢ ∃ I, I ∼ A

State before:
case mp.Case_1
U : Type
A : Set U
h1 : finite A
⊢ ∃ I, I ∼ A
Tactic:
define at h1
State after:
case mp.Case_1
U : Type
A : Set U
h1 : ∃ n, I n ∼ A
⊢ ∃ I, I ∼ A

State before:
case mp.Case_1
U : Type
A : Set U
h1 : ∃ n, I n ∼ A
⊢ ∃ I, I ∼ A
Tactic:
obtain (n : Nat) (h2 : I n ∼ A) from h1
State after:
case mp.Case_1
U : Type
A : Set U
h1 : ∃ n, I n ∼ A
n : ℕ
h2 : I n ∼ A
⊢ ∃ I, I ∼ A

State before:
case mp.Case_1
U : Type
A : Set U
h1 : ∃ n, I n ∼ A
n : ℕ
h2 : I n ∼ A
⊢ ∃ I, I ∼ A
Tactic:
show ∃ (I : Set Nat), I ∼ A from Exists.intro (I n) h2
State after:
no goals

State before:
case mp.Case_2
U : Type
A : Set U
h1 : denum A
⊢ ∃ I, I ∼ A
Tactic:
rewrite [denum_def] at h1
State after:
case mp.Case_2
U : Type
A : Set U
h1 : Univ ℕ ∼ A
⊢ ∃ I, I ∼ A

State before:
case mp.Case_2
U : Type
A : Set U
h1 : Univ ℕ ∼ A
⊢ ∃ I, I ∼ A
Tactic:
show ∃ (I : Set Nat), I ∼ A from Exists.intro (Univ Nat) h1
State after:
no goals

State before:
case mpr
U : Type
A : Set U
⊢ (∃ I, I ∼ A) → ctble A
Tactic:
assume h1 : ∃ (I : Set Nat), I ∼ A
State after:
case mpr
U : Type
A : Set U
h1 : ∃ I, I ∼ A
⊢ ctble A

State before:
case mpr
U : Type
A : Set U
h1 : ∃ I, I ∼ A
⊢ ctble A
Tactic:
obtain (I : Set Nat) (h2 : I ∼ A) from h1
State after:
case mpr
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
⊢ ctble A

State before:
case mpr
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
⊢ ctble A
Tactic:
have h3 : ctble I := subset_nat_ctble I
State after:
case mpr
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
h3 : ctble I
⊢ ctble A

State before:
case mpr
U : Type
A : Set U
h1 : ∃ I, I ∼ A
I : Set ℕ
h2 : I ∼ A
h3 : ctble I
⊢ ctble A
Tactic:
show ctble A from ctble_of_equinum_ctble h2 h3
State after:
no goals