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

State before:
U : Type
A : Set U
h1 : ctble A
⊢ ctble (seq A)
Tactic:
set F : Set (Set (List U)) := sbl_set A
State after:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
⊢ ctble (seq A)

State before:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
⊢ ctble (seq A)
Tactic:
have h2 : ctble F := Lemma_8_2_4_4 A
State after:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
h2 : ctble F
⊢ ctble (seq A)

State before:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
h2 : ctble F
⊢ ctble (seq A)
Tactic:
have h3 : ∀ S ∈ F, ctble S := by
  fix S : Set (List U)
  assume h3 : S ∈ F
  define at h3
  obtain (n : Nat) (h4 : seq_by_length A n = S) from h3
  rewrite [←h4]
  show ctble (seq_by_length A n) from Lemma_8_2_4_2 h1 n
  done
State after:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
h2 : ctble F
h3 : ∀ S ∈ F, ctble S
⊢ ctble (seq A)

State before:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
h2 : ctble F
h3 : ∀ S ∈ F, ctble S
⊢ ctble (seq A)
Tactic:
rewrite [←Lemma_8_2_4_3 A]
State after:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
h2 : ctble F
h3 : ∀ S ∈ F, ctble S
⊢ ctble (⋃₀ sbl_set A)

State before:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
h2 : ctble F
h3 : ∀ S ∈ F, ctble S
⊢ ctble (⋃₀ sbl_set A)
Tactic:
show ctble (⋃₀ sbl_set A) from Theorem_8_2_2 h2 h3
State after:
no goals

State before:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
h2 : ctble F
⊢ ∀ S ∈ F, ctble S
Tactic:
fix S : Set (List U)
State after:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
h2 : ctble F
S : Set (List U)
⊢ S ∈ F → ctble S

State before:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
h2 : ctble F
S : Set (List U)
⊢ S ∈ F → ctble S
Tactic:
assume h3 : S ∈ F
State after:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
h2 : ctble F
S : Set (List U)
h3 : S ∈ F
⊢ ctble S

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

State before:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
h2 : ctble F
S : Set (List U)
h3 : ∃ n, seq_by_length A n = S
⊢ ctble S
Tactic:
obtain (n : Nat) (h4 : seq_by_length A n = S) from h3
State after:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
h2 : ctble F
S : Set (List U)
h3 : ∃ n, seq_by_length A n = S
n : ℕ
h4 : seq_by_length A n = S
⊢ ctble S

State before:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
h2 : ctble F
S : Set (List U)
h3 : ∃ n, seq_by_length A n = S
n : ℕ
h4 : seq_by_length A n = S
⊢ ctble S
Tactic:
rewrite [←h4]
State after:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
h2 : ctble F
S : Set (List U)
h3 : ∃ n, seq_by_length A n = S
n : ℕ
h4 : seq_by_length A n = S
⊢ ctble (seq_by_length A n)

State before:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
h2 : ctble F
S : Set (List U)
h3 : ∃ n, seq_by_length A n = S
n : ℕ
h4 : seq_by_length A n = S
⊢ ctble (seq_by_length A n)
Tactic:
show ctble (seq_by_length A n) from Lemma_8_2_4_2 h1 n
State after:
no goals