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

State before:
A : Set ℕ
⊢ ctble A
Tactic:
define
State after:
A : Set ℕ
⊢ finite A ∨ denum A

State before:
A : Set ℕ
⊢ finite A ∨ denum A
Tactic:
by_cases h1 : ∃ (m : Nat), ∀ n ∈ A, n < m
State after:
case pos
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
⊢ finite A ∨ denum A

case neg
A : Set ℕ
h1 : ¬∃ m, ∀ n ∈ A, n < m
⊢ finite A ∨ denum A

State before:
case pos
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
⊢ finite A ∨ denum A
Tactic:
apply Or.inl
State after:
case pos.h
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
⊢ finite A

State before:
case pos.h
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
⊢ finite A
Tactic:
obtain (m : Nat) (h2 : ∀ n ∈ A, n < m) from h1
State after:
case pos.h
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
m : ℕ
h2 : ∀ n ∈ A, n < m
⊢ finite A

State before:
case pos.h
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
m : ℕ
h2 : ∀ n ∈ A, n < m
⊢ finite A
Tactic:
obtain (s : Nat) (h3 : num_elts_below A m s) from neb_exists A m
State after:
case pos.h
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
m : ℕ
h2 : ∀ n ∈ A, n < m
s : ℕ
h3 : num_elts_below A m s
⊢ finite A

State before:
case pos.h
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
m : ℕ
h2 : ∀ n ∈ A, n < m
s : ℕ
h3 : num_elts_below A m s
⊢ finite A
Tactic:
apply Exists.intro s
State after:
case pos.h
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
m : ℕ
h2 : ∀ n ∈ A, n < m
s : ℕ
h3 : num_elts_below A m s
⊢ I s ∼ A

State before:
case pos.h
A : Set ℕ
h1 : ∃ m, ∀ n ∈ A, n < m
m : ℕ
h2 : ∀ n ∈ A, n < m
s : ℕ
h3 : num_elts_below A m s
⊢ I s ∼ A
Tactic:
show I s ∼ A from bdd_subset_nat h2 h3
State after:
no goals

State before:
case neg
A : Set ℕ
h1 : ¬∃ m, ∀ n ∈ A, n < m
⊢ finite A ∨ denum A
Tactic:
apply Or.inr
State after:
case neg.h
A : Set ℕ
h1 : ¬∃ m, ∀ n ∈ A, n < m
⊢ denum A

State before:
case neg.h
A : Set ℕ
h1 : ¬∃ m, ∀ n ∈ A, n < m
⊢ denum A
Tactic:
push_neg at h1
State after:
case neg.h
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, m ≤ n
⊢ denum A

State before:
case neg.h
A : Set ℕ
h1 : ∀ (m : ℕ), ∃ n ∈ A, m ≤ n
⊢ denum A
Tactic:
show denum A from unbdd_subset_nat h1
State after:
no goals