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

State before:
U : Type
A : Set U
h1 : ctble A
⊢ ∀ (n : ℕ), ctble (seq_by_length A n)
Tactic:
by_induc
State after:
case Base_Case
U : Type
A : Set U
h1 : ctble A
⊢ ctble (seq_by_length A 0)

case Induction_Step
U : Type
A : Set U
h1 : ctble A
⊢ ∀ (n : ℕ), ctble (seq_by_length A n) → ctble (seq_by_length A (n + 1))

State before:
case Base_Case
U : Type
A : Set U
h1 : ctble A
⊢ ctble (seq_by_length A 0)
Tactic:
rewrite [sbl_base]
State after:
case Base_Case
U : Type
A : Set U
h1 : ctble A
⊢ ctble {[]}

State before:
case Base_Case
U : Type
A : Set U
h1 : ctble A
⊢ ctble {[]}
Tactic:
define
State after:
case Base_Case
U : Type
A : Set U
h1 : ctble A
⊢ finite {[]} ∨ denum {[]}

State before:
case Base_Case
U : Type
A : Set U
h1 : ctble A
⊢ finite {[]} ∨ denum {[]}
Tactic:
apply Or.inl
State after:
case Base_Case.h
U : Type
A : Set U
h1 : ctble A
⊢ finite {[]}

State before:
case Base_Case.h
U : Type
A : Set U
h1 : ctble A
⊢ finite {[]}
Tactic:
rewrite [finite_def]
State after:
case Base_Case.h
U : Type
A : Set U
h1 : ctble A
⊢ ∃ n, numElts {[]} n

State before:
case Base_Case.h
U : Type
A : Set U
h1 : ctble A
⊢ ∃ n, numElts {[]} n
Tactic:
apply Exists.intro 1
State after:
case Base_Case.h
U : Type
A : Set U
h1 : ctble A
⊢ numElts {[]} 1

State before:
case Base_Case.h
U : Type
A : Set U
h1 : ctble A
⊢ numElts {[]} 1
Tactic:
show numElts {[]} 1 from singleton_one_elt []
State after:
no goals

State before:
case Induction_Step
U : Type
A : Set U
h1 : ctble A
⊢ ∀ (n : ℕ), ctble (seq_by_length A n) → ctble (seq_by_length A (n + 1))
Tactic:
fix n : Nat
State after:
case Induction_Step
U : Type
A : Set U
h1 : ctble A
n : ℕ
⊢ ctble (seq_by_length A n) → ctble (seq_by_length A (n + 1))

State before:
case Induction_Step
U : Type
A : Set U
h1 : ctble A
n : ℕ
⊢ ctble (seq_by_length A n) → ctble (seq_by_length A (n + 1))
Tactic:
assume ih : ctble (seq_by_length A n)
State after:
case Induction_Step
U : Type
A : Set U
h1 : ctble A
n : ℕ
ih : ctble (seq_by_length A n)
⊢ ctble (seq_by_length A (n + 1))

State before:
case Induction_Step
U : Type
A : Set U
h1 : ctble A
n : ℕ
ih : ctble (seq_by_length A n)
⊢ ctble (seq_by_length A (n + 1))
Tactic:
have h2 : A ×ₛ (seq_by_length A n) ∼ seq_by_length A (n + 1) :=
  Lemma_8_2_4_1 A n
State after:
case Induction_Step
U : Type
A : Set U
h1 : ctble A
n : ℕ
ih : ctble (seq_by_length A n)
h2 : A ×ₛ seq_by_length A n ∼ seq_by_length A (n + 1)
⊢ ctble (seq_by_length A (n + 1))

State before:
case Induction_Step
U : Type
A : Set U
h1 : ctble A
n : ℕ
ih : ctble (seq_by_length A n)
h2 : A ×ₛ seq_by_length A n ∼ seq_by_length A (n + 1)
⊢ ctble (seq_by_length A (n + 1))
Tactic:
have h3 : ctble (A ×ₛ (seq_by_length A n)) := Theorem_8_2_1_1 h1 ih
State after:
case Induction_Step
U : Type
A : Set U
h1 : ctble A
n : ℕ
ih : ctble (seq_by_length A n)
h2 : A ×ₛ seq_by_length A n ∼ seq_by_length A (n + 1)
h3 : ctble (A ×ₛ seq_by_length A n)
⊢ ctble (seq_by_length A (n + 1))

State before:
case Induction_Step
U : Type
A : Set U
h1 : ctble A
n : ℕ
ih : ctble (seq_by_length A n)
h2 : A ×ₛ seq_by_length A n ∼ seq_by_length A (n + 1)
h3 : ctble (A ×ₛ seq_by_length A n)
⊢ ctble (seq_by_length A (n + 1))
Tactic:
show ctble (seq_by_length A (n + 1)) from ctble_of_equinum_ctble h2 h3
State after:
no goals