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

State before:
U : Type
A : Set U
⊢ ctble (sbl_set A)
Tactic:
have h1 : ∀ S ∈ sbl_set A, ∃ (n : Nat), seq_by_length A n = S := by
  fix S : Set (List U)
  assume h1 : S ∈ sbl_set A
  define at h1
  show ∃ (n : Nat), seq_by_length A n = S from h1
  done
State after:
U : Type
A : Set U
h1 : ∀ S ∈ sbl_set A, ∃ n, seq_by_length A n = S
⊢ ctble (sbl_set A)

State before:
U : Type
A : Set U
h1 : ∀ S ∈ sbl_set A, ∃ n, seq_by_length A n = S
⊢ ctble (sbl_set A)
Tactic:
show ctble (sbl_set A) from ctble_of_onto_func_from_N h1
State after:
no goals

State before:
U : Type
A : Set U
⊢ ∀ S ∈ sbl_set A, ∃ n, seq_by_length A n = S
Tactic:
fix S : Set (List U)
State after:
U : Type
A : Set U
S : Set (List U)
⊢ S ∈ sbl_set A → ∃ n, seq_by_length A n = S

State before:
U : Type
A : Set U
S : Set (List U)
⊢ S ∈ sbl_set A → ∃ n, seq_by_length A n = S
Tactic:
assume h1 : S ∈ sbl_set A
State after:
U : Type
A : Set U
S : Set (List U)
h1 : S ∈ sbl_set A
⊢ ∃ n, seq_by_length A n = S

State before:
U : Type
A : Set U
S : Set (List U)
h1 : S ∈ sbl_set A
⊢ ∃ n, seq_by_length A n = S
Tactic:
define at h1
State after:
U : Type
A : Set U
S : Set (List U)
h1 : ∃ n, seq_by_length A n = S
⊢ ∃ n, seq_by_length A n = S

State before:
U : Type
A : Set U
S : Set (List U)
h1 : ∃ n, seq_by_length A n = S
⊢ ∃ n, seq_by_length A n = S
Tactic:
show ∃ (n : Nat), seq_by_length A n = S from h1
State after:
no goals