internlm/Lean-Github huggingface dataset:
Theorem: HTPI.sbl_base
Proof state before:
case h.mp
U : Type
A : Set U
l : List U
⊢ l ∈ seq_by_length A 0 → l ∈ {[]}
Tactic:
assume h1 : l ∈ seq_by_length A 0
Proof state after:
case h.mp
U : Type
A : Set U
l : List U
h1 : l ∈ seq_by_length A 0
⊢ l ∈ {[]}
Theorem: HTPI.sbl_base
Proof state before:
case h.mp
U : Type
A : Set U
l : List U
h1 : l ∈ seq_by_length A 0
⊢ l ∈ {[]}
Tactic:
define at h1
Proof state after:
case h.mp
U : Type
A : Set U
l : List U
h1 : l ∈ seq A ∧ List.length l = 0
⊢ l ∈ {[]}
Theorem: HTPI.sbl_base
Proof state before:
case h.mp
U : Type
A : Set U
l : List U
h1 : l ∈ seq A ∧ List.length l = 0
⊢ l ∈ {[]}
Tactic:
rewrite [List.length_eq_zero] at h1
Proof state after:
case h.mp
U : Type
A : Set U
l : List U
h1 : l ∈ seq A ∧ l = []
⊢ l ∈ {[]}
Theorem: HTPI.sbl_base
Proof state before:
case h.mp
U : Type
A : Set U
l : List U
h1 : l ∈ seq A ∧ l = []
⊢ l ∈ {[]}
Tactic:
define
Proof state after:
case h.mp
U : Type
A : Set U
l : List U
h1 : l ∈ seq A ∧ l = []
⊢ l = []
Theorem: HTPI.sbl_base
Proof state before:
case h.mp
U : Type
A : Set U
l : List U
h1 : l ∈ seq A ∧ l = []
⊢ l = []
Tactic:
show l = [] from h1.right
Proof state after:
no goals
Theorem: HTPI.sbl_base
Proof state before:
case h.mpr
U : Type
A : Set U
l : List U
⊢ l ∈ {[]} → l ∈ seq_by_length A 0
Tactic:
assume h1 : l ∈ {[]}
Proof state after:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l ∈ {[]}
⊢ l ∈ seq_by_length A 0
Theorem: HTPI.sbl_base
Proof state before:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l ∈ {[]}
⊢ l ∈ seq_by_length A 0
Tactic:
define at h1
Proof state after:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l = []
⊢ l ∈ seq_by_length A 0
Theorem: HTPI.sbl_base
Proof state before:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l = []
⊢ l ∈ seq_by_length A 0
Tactic:
define
Proof state after:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l = []
⊢ l ∈ seq A ∧ List.length l = 0
Theorem: HTPI.sbl_base
Proof state before:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l = []
⊢ l ∈ seq A ∧ List.length l = 0
Tactic:
apply And.intro _ (List.length_eq_zero.rtl h1)
Proof state after:
U : Type
A : Set U
l : List U
h1 : l = []
⊢ l ∈ seq A
Theorem: HTPI.sbl_base
Proof state before:
U : Type
A : Set U
l : List U
h1 : l = []
⊢ l ∈ seq A
Tactic:
define
Proof state after:
U : Type
A : Set U
l : List U
h1 : l = []
⊢ ∀ x ∈ l, x ∈ A
Theorem: HTPI.sbl_base
Proof state before:
U : Type
A : Set U
l : List U
h1 : l = []
⊢ ∀ x ∈ l, x ∈ A
Tactic:
fix x : U
Proof state after:
U : Type
A : Set U
l : List U
h1 : l = []
x : U
⊢ x ∈ l → x ∈ A
Theorem: HTPI.sbl_base
Proof state before:
U : Type
A : Set U
l : List U
h1 : l = []
x : U
⊢ x ∈ l → x ∈ A
Tactic:
assume h2 : x ∈ l
Proof state after:
U : Type
A : Set U
l : List U
h1 : l = []
x : U
h2 : x ∈ l
⊢ x ∈ A
Theorem: HTPI.sbl_base
Proof state before:
U : Type
A : Set U
l : List U
h1 : l = []
x : U
h2 : x ∈ l
⊢ x ∈ A
Tactic:
contradict h2 with h3
Proof state after:
U : Type
A : Set U
l : List U
h1 : l = []
x : U
h2 : x ∈ l
h3 : ¬x ∈ A
⊢ x ∉ l
Theorem: HTPI.sbl_base
Proof state before:
U : Type
A : Set U
l : List U
h1 : l = []
x : U
h2 : x ∈ l
h3 : ¬x ∈ A
⊢ x ∉ l
Tactic:
rewrite [h1]
Proof state after:
U : Type
A : Set U
l : List U
h1 : l = []
x : U
h2 : x ∈ l
h3 : ¬x ∈ A
⊢ x ∉ []
Theorem: HTPI.sbl_base
Proof state before:
U : Type
A : Set U
l : List U
h1 : l = []
x : U
h2 : x ∈ l
h3 : ¬x ∈ A
⊢ x ∉ []
Tactic:
show x ∉ [] from List.not_mem_nil x
Proof state after:
no goals
Theorem: HTPI.seq_cons_def
Proof state before:
U : Type
x : U
l : List U
⊢ seq_cons U (x, l) = x :: l
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.seq_cons_one_one
Proof state before:
U : Type
⊢ one_to_one (seq_cons U)
Tactic:
fix (a1, l1) : U × List U
Proof state after:
U : Type
a1 : U
l1 : List U
⊢ ∀ (x2 : U × List U), seq_cons U (a1, l1) = seq_cons U x2 → (a1, l1) = x2
Theorem: HTPI.seq_cons_one_one
Proof state before:
U : Type
a1 : U
l1 : List U
⊢ ∀ (x2 : U × List U), seq_cons U (a1, l1) = seq_cons U x2 → (a1, l1) = x2
Tactic:
fix (a2, l2) : U × List U
Proof state after:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
⊢ seq_cons U (a1, l1) = seq_cons U (a2, l2) → (a1, l1) = (a2, l2)
Theorem: HTPI.seq_cons_one_one
Proof state before:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
⊢ seq_cons U (a1, l1) = seq_cons U (a2, l2) → (a1, l1) = (a2, l2)
Tactic:
assume h1 : seq_cons U (a1, l1) = seq_cons U (a2, l2)
Proof state after:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
h1 : seq_cons U (a1, l1) = seq_cons U (a2, l2)
⊢ (a1, l1) = (a2, l2)
Theorem: HTPI.seq_cons_one_one
Proof state before:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
h1 : seq_cons U (a1, l1) = seq_cons U (a2, l2)
⊢ (a1, l1) = (a2, l2)
Tactic:
rewrite [seq_cons_def, seq_cons_def] at h1
Proof state after:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
h1 : a1 :: l1 = a2 :: l2
⊢ (a1, l1) = (a2, l2)
Theorem: HTPI.seq_cons_one_one
Proof state before:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
h1 : a1 :: l1 = a2 :: l2
⊢ (a1, l1) = (a2, l2)
Tactic:
rewrite [List.cons_eq_cons] at h1
Proof state after:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
h1 : a1 = a2 ∧ l1 = l2
⊢ (a1, l1) = (a2, l2)
Theorem: HTPI.seq_cons_one_one
Proof state before:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
h1 : a1 = a2 ∧ l1 = l2
⊢ (a1, l1) = (a2, l2)
Tactic:
rewrite [h1.left, h1.right]
Proof state after:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
h1 : a1 = a2 ∧ l1 = l2
⊢ (a2, l2) = (a2, l2)
Theorem: HTPI.seq_cons_one_one
Proof state before:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
h1 : a1 = a2 ∧ l1 = l2
⊢ (a2, l2) = (a2, l2)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Lemma_8_2_4_2
Proof state before:
U : Type
A : Set U
h1 : ctble A
⊢ ∀ (n : ℕ), ctble (seq_by_length A n)
Tactic:
by_induc
Proof 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))
Theorem: HTPI.Lemma_8_2_4_2
Proof state before:
case Base_Case
U : Type
A : Set U
h1 : ctble A
⊢ ctble (seq_by_length A 0)
Tactic:
rewrite [sbl_base]
Proof state after:
case Base_Case
U : Type
A : Set U
h1 : ctble A
⊢ ctble {[]}
Theorem: HTPI.Lemma_8_2_4_2
Proof state before:
case Base_Case
U : Type
A : Set U
h1 : ctble A
⊢ ctble {[]}
Tactic:
define
Proof state after:
case Base_Case
U : Type
A : Set U
h1 : ctble A
⊢ finite {[]} ∨ denum {[]}
Theorem: HTPI.Lemma_8_2_4_2
Proof state before:
case Base_Case
U : Type
A : Set U
h1 : ctble A
⊢ finite {[]} ∨ denum {[]}
Tactic:
apply Or.inl
Proof state after:
case Base_Case.h
U : Type
A : Set U
h1 : ctble A
⊢ finite {[]}
Theorem: HTPI.Lemma_8_2_4_2
Proof state before:
case Base_Case.h
U : Type
A : Set U
h1 : ctble A
⊢ finite {[]}
Tactic:
rewrite [finite_def]
Proof state after:
case Base_Case.h
U : Type
A : Set U
h1 : ctble A
⊢ ∃ n, numElts {[]} n
Theorem: HTPI.Lemma_8_2_4_2
Proof state before:
case Base_Case.h
U : Type
A : Set U
h1 : ctble A
⊢ ∃ n, numElts {[]} n
Tactic:
apply Exists.intro 1
Proof state after:
case Base_Case.h
U : Type
A : Set U
h1 : ctble A
⊢ numElts {[]} 1
Theorem: HTPI.Lemma_8_2_4_2
Proof state before:
case Base_Case.h
U : Type
A : Set U
h1 : ctble A
⊢ numElts {[]} 1
Tactic:
show numElts {[]} 1 from singleton_one_elt []
Proof state after:
no goals
Theorem: HTPI.Lemma_8_2_4_2
Proof 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
Proof 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))
Theorem: HTPI.Lemma_8_2_4_2
Proof 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)
Proof 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))
Theorem: HTPI.Lemma_8_2_4_2
Proof 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
Proof 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))
Theorem: HTPI.Lemma_8_2_4_2
Proof 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
Proof 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))
Theorem: HTPI.Lemma_8_2_4_2
Proof 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
Proof state after:
no goals
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
U : Type
A : Set U
⊢ ⋃₀ sbl_set A = seq A
Tactic:
apply Set.ext
Proof state after:
case h
U : Type
A : Set U
⊢ ∀ (x : List U), x ∈ ⋃₀ sbl_set A ↔ x ∈ seq A
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h
U : Type
A : Set U
⊢ ∀ (x : List U), x ∈ ⋃₀ sbl_set A ↔ x ∈ seq A
Tactic:
fix l : List U
Proof state after:
case h
U : Type
A : Set U
l : List U
⊢ l ∈ ⋃₀ sbl_set A ↔ l ∈ seq A
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h
U : Type
A : Set U
l : List U
⊢ l ∈ ⋃₀ sbl_set A ↔ l ∈ seq A
Tactic:
apply Iff.intro
Proof state after:
case h.mp
U : Type
A : Set U
l : List U
⊢ l ∈ ⋃₀ sbl_set A → l ∈ seq A

case h.mpr
U : Type
A : Set U
l : List U
⊢ l ∈ seq A → l ∈ ⋃₀ sbl_set A
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mp
U : Type
A : Set U
l : List U
⊢ l ∈ ⋃₀ sbl_set A → l ∈ seq A
Tactic:
assume h1 : l ∈ ⋃₀ (sbl_set A)
Proof state after:
case h.mp
U : Type
A : Set U
l : List U
h1 : l ∈ ⋃₀ sbl_set A
⊢ l ∈ seq A
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mp
U : Type
A : Set U
l : List U
h1 : l ∈ ⋃₀ sbl_set A
⊢ l ∈ seq A
Tactic:
define at h1
Proof state after:
case h.mp
U : Type
A : Set U
l : List U
h1 : ∃ t ∈ sbl_set A, l ∈ t
⊢ l ∈ seq A
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mp
U : Type
A : Set U
l : List U
h1 : ∃ t ∈ sbl_set A, l ∈ t
⊢ l ∈ seq A
Tactic:
obtain (S : Set (List U)) (h2 :  S ∈ sbl_set A ∧ l ∈ S) from h1
Proof state after:
case h.mp
U : Type
A : Set U
l : List U
h1 : ∃ t ∈ sbl_set A, l ∈ t
S : Set (List U)
h2 : S ∈ sbl_set A ∧ l ∈ S
⊢ l ∈ seq A
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mp
U : Type
A : Set U
l : List U
h1 : ∃ t ∈ sbl_set A, l ∈ t
S : Set (List U)
h2 : S ∈ sbl_set A ∧ l ∈ S
⊢ l ∈ seq A
Tactic:
have h3 : S ∈ sbl_set A := h2.left
Proof state after:
case h.mp
U : Type
A : Set U
l : List U
h1 : ∃ t ∈ sbl_set A, l ∈ t
S : Set (List U)
h2 : S ∈ sbl_set A ∧ l ∈ S
h3 : S ∈ sbl_set A
⊢ l ∈ seq A
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mp
U : Type
A : Set U
l : List U
h1 : ∃ t ∈ sbl_set A, l ∈ t
S : Set (List U)
h2 : S ∈ sbl_set A ∧ l ∈ S
h3 : S ∈ sbl_set A
⊢ l ∈ seq A
Tactic:
define at h3
Proof state after:
case h.mp
U : Type
A : Set U
l : List U
h1 : ∃ t ∈ sbl_set A, l ∈ t
S : Set (List U)
h2 : S ∈ sbl_set A ∧ l ∈ S
h3 : ∃ n, seq_by_length A n = S
⊢ l ∈ seq A
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mp
U : Type
A : Set U
l : List U
h1 : ∃ t ∈ sbl_set A, l ∈ t
S : Set (List U)
h2 : S ∈ sbl_set A ∧ l ∈ S
h3 : ∃ n, seq_by_length A n = S
⊢ l ∈ seq A
Tactic:
obtain (n : Nat) (h4 : seq_by_length A n = S) from h3
Proof state after:
case h.mp
U : Type
A : Set U
l : List U
h1 : ∃ t ∈ sbl_set A, l ∈ t
S : Set (List U)
h2 : S ∈ sbl_set A ∧ l ∈ S
h3 : ∃ n, seq_by_length A n = S
n : ℕ
h4 : seq_by_length A n = S
⊢ l ∈ seq A
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mp
U : Type
A : Set U
l : List U
h1 : ∃ t ∈ sbl_set A, l ∈ t
S : Set (List U)
h2 : S ∈ sbl_set A ∧ l ∈ S
h3 : ∃ n, seq_by_length A n = S
n : ℕ
h4 : seq_by_length A n = S
⊢ l ∈ seq A
Tactic:
have h5 : l ∈ S := h2.right
Proof state after:
case h.mp
U : Type
A : Set U
l : List U
h1 : ∃ t ∈ sbl_set A, l ∈ t
S : Set (List U)
h2 : S ∈ sbl_set A ∧ l ∈ S
h3 : ∃ n, seq_by_length A n = S
n : ℕ
h4 : seq_by_length A n = S
h5 : l ∈ S
⊢ l ∈ seq A
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mp
U : Type
A : Set U
l : List U
h1 : ∃ t ∈ sbl_set A, l ∈ t
S : Set (List U)
h2 : S ∈ sbl_set A ∧ l ∈ S
h3 : ∃ n, seq_by_length A n = S
n : ℕ
h4 : seq_by_length A n = S
h5 : l ∈ S
⊢ l ∈ seq A
Tactic:
rewrite [←h4] at h5
Proof state after:
case h.mp
U : Type
A : Set U
l : List U
h1 : ∃ t ∈ sbl_set A, l ∈ t
S : Set (List U)
h2 : S ∈ sbl_set A ∧ l ∈ S
h3 : ∃ n, seq_by_length A n = S
n : ℕ
h4 : seq_by_length A n = S
h5 : l ∈ seq_by_length A n
⊢ l ∈ seq A
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mp
U : Type
A : Set U
l : List U
h1 : ∃ t ∈ sbl_set A, l ∈ t
S : Set (List U)
h2 : S ∈ sbl_set A ∧ l ∈ S
h3 : ∃ n, seq_by_length A n = S
n : ℕ
h4 : seq_by_length A n = S
h5 : l ∈ seq_by_length A n
⊢ l ∈ seq A
Tactic:
define at h5
Proof state after:
case h.mp
U : Type
A : Set U
l : List U
h1 : ∃ t ∈ sbl_set A, l ∈ t
S : Set (List U)
h2 : S ∈ sbl_set A ∧ l ∈ S
h3 : ∃ n, seq_by_length A n = S
n : ℕ
h4 : seq_by_length A n = S
h5 : l ∈ seq A ∧ List.length l = n
⊢ l ∈ seq A
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mp
U : Type
A : Set U
l : List U
h1 : ∃ t ∈ sbl_set A, l ∈ t
S : Set (List U)
h2 : S ∈ sbl_set A ∧ l ∈ S
h3 : ∃ n, seq_by_length A n = S
n : ℕ
h4 : seq_by_length A n = S
h5 : l ∈ seq A ∧ List.length l = n
⊢ l ∈ seq A
Tactic:
show l ∈ seq A from h5.left
Proof state after:
no goals
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mpr
U : Type
A : Set U
l : List U
⊢ l ∈ seq A → l ∈ ⋃₀ sbl_set A
Tactic:
assume h1 : l ∈ seq A
Proof state after:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
⊢ l ∈ ⋃₀ sbl_set A
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
⊢ l ∈ ⋃₀ sbl_set A
Tactic:
define
Proof state after:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
⊢ ∃ t ∈ sbl_set A, l ∈ t
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
⊢ ∃ t ∈ sbl_set A, l ∈ t
Tactic:
set n : Nat := l.length
Proof state after:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
n : ℕ := List.length l
⊢ ∃ t ∈ sbl_set A, l ∈ t
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
n : ℕ := List.length l
⊢ ∃ t ∈ sbl_set A, l ∈ t
Tactic:
apply Exists.intro (seq_by_length A n)
Proof state after:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
n : ℕ := List.length l
⊢ seq_by_length A n ∈ sbl_set A ∧ l ∈ seq_by_length A n
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
n : ℕ := List.length l
⊢ seq_by_length A n ∈ sbl_set A ∧ l ∈ seq_by_length A n
Tactic:
apply And.intro
Proof state after:
case h.mpr.left
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
n : ℕ := List.length l
⊢ seq_by_length A n ∈ sbl_set A

case h.mpr.right
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
n : ℕ := List.length l
⊢ l ∈ seq_by_length A n
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mpr.left
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
n : ℕ := List.length l
⊢ seq_by_length A n ∈ sbl_set A
Tactic:
define
Proof state after:
case h.mpr.left
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
n : ℕ := List.length l
⊢ ∃ n_1, seq_by_length A n_1 = seq_by_length A n
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mpr.left
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
n : ℕ := List.length l
⊢ ∃ n_1, seq_by_length A n_1 = seq_by_length A n
Tactic:
apply Exists.intro n
Proof state after:
case h.mpr.left
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
n : ℕ := List.length l
⊢ seq_by_length A n = seq_by_length A n
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mpr.left
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
n : ℕ := List.length l
⊢ seq_by_length A n = seq_by_length A n
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mpr.right
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
n : ℕ := List.length l
⊢ l ∈ seq_by_length A n
Tactic:
define
Proof state after:
case h.mpr.right
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
n : ℕ := List.length l
⊢ l ∈ seq A ∧ List.length l = n
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mpr.right
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
n : ℕ := List.length l
⊢ l ∈ seq A ∧ List.length l = n
Tactic:
apply And.intro h1
Proof state after:
case h.mpr.right
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
n : ℕ := List.length l
⊢ List.length l = n
Theorem: HTPI.Lemma_8_2_4_3
Proof state before:
case h.mpr.right
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
n : ℕ := List.length l
⊢ List.length l = n
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Lemma_8_2_4_4
Proof 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
Proof state after:
U : Type
A : Set U
h1 : ∀ S ∈ sbl_set A, ∃ n, seq_by_length A n = S
⊢ ctble (sbl_set A)
Theorem: HTPI.Lemma_8_2_4_4
Proof 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
Proof state after:
no goals
Theorem: HTPI.Lemma_8_2_4_4
Proof state before:
U : Type
A : Set U
⊢ ∀ S ∈ sbl_set A, ∃ n, seq_by_length A n = S
Tactic:
fix S : Set (List U)
Proof state after:
U : Type
A : Set U
S : Set (List U)
⊢ S ∈ sbl_set A → ∃ n, seq_by_length A n = S
Theorem: HTPI.Lemma_8_2_4_4
Proof 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
Proof state after:
U : Type
A : Set U
S : Set (List U)
h1 : S ∈ sbl_set A
⊢ ∃ n, seq_by_length A n = S
Theorem: HTPI.Lemma_8_2_4_4
Proof 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
Proof 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
Theorem: HTPI.Lemma_8_2_4_4
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_8_2_4
Proof state before:
U : Type
A : Set U
h1 : ctble A
⊢ ctble (seq A)
Tactic:
set F : Set (Set (List U)) := sbl_set A
Proof state after:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
⊢ ctble (seq A)
Theorem: HTPI.Theorem_8_2_4
Proof 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
Proof state after:
U : Type
A : Set U
h1 : ctble A
F : Set (Set (List U)) := sbl_set A
h2 : ctble F
⊢ ctble (seq A)
Theorem: HTPI.Theorem_8_2_4
Proof 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
Proof 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)
Theorem: HTPI.Theorem_8_2_4
Proof 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]
Proof 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)
Theorem: HTPI.Theorem_8_2_4
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_8_2_4
Proof 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)
Proof 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
Theorem: HTPI.Theorem_8_2_4
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_2_4
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_2_4
Proof 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
Proof 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
Theorem: HTPI.Theorem_8_2_4
Proof 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]
Proof 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)
Theorem: HTPI.Theorem_8_2_4
Proof 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
Proof state after:
no goals
Theorem: HTPI.set_elt_powerset_univ
Proof state before:
U : Type
A : Set U
⊢ A ∈ 𝒫 Univ U
Tactic:
fix x : U
Proof state after:
U : Type
A : Set U
x : U
⊢ x ∈ A → x ∈ Univ U
Theorem: HTPI.set_elt_powerset_univ
Proof state before:
U : Type
A : Set U
x : U
⊢ x ∈ A → x ∈ Univ U
Tactic:
assume h : x ∈ A
Proof state after:
U : Type
A : Set U
x : U
h : x ∈ A
⊢ x ∈ Univ U
Theorem: HTPI.set_elt_powerset_univ
Proof state before:
U : Type
A : Set U
x : U
h : x ∈ A
⊢ x ∈ Univ U
Tactic:
show x ∈ Univ U from elt_Univ x
Proof state after:
no goals
Theorem: HTPI.Cantor's_theorem
Proof state before:
⊢ ¬ctble (𝒫 Univ ℕ)
Tactic:
by_contra h1
Proof state after:
h1 : ctble (𝒫 Univ ℕ)
⊢ False
Theorem: HTPI.Cantor's_theorem
Proof state before:
h1 : ctble (𝒫 Univ ℕ)
⊢ False
Tactic:
rewrite [Theorem_8_1_5_2] at h1
Proof state after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
⊢ False
Theorem: HTPI.Cantor's_theorem
Proof state before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
⊢ False
Tactic:
obtain (R : Rel Nat (Set Nat))
  (h2 : fcnl_onto_from_nat R (𝒫 (Univ Nat))) from h1
Proof state after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : fcnl_onto_from_nat R (𝒫 Univ ℕ)
⊢ False
Theorem: HTPI.Cantor's_theorem
Proof state before:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : fcnl_onto_from_nat R (𝒫 Univ ℕ)
⊢ False
Tactic:
define at h2
Proof state after:
h1 : ∃ R, fcnl_onto_from_nat R (𝒫 Univ ℕ)
R : Rel ℕ (Set ℕ)
h2 : unique_val_on_N R ∧ nat_rel_onto R (𝒫 Univ ℕ)
⊢ False