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

State before:
U : Type
A : Set U
⊢ ⋃₀ sbl_set A = seq A
Tactic:
apply Set.ext
State after:
case h
U : Type
A : Set U
⊢ ∀ (x : List U), x ∈ ⋃₀ sbl_set A ↔ x ∈ seq A

State before:
case h
U : Type
A : Set U
⊢ ∀ (x : List U), x ∈ ⋃₀ sbl_set A ↔ x ∈ seq A
Tactic:
fix l : List U
State after:
case h
U : Type
A : Set U
l : List U
⊢ l ∈ ⋃₀ sbl_set A ↔ l ∈ seq A

State before:
case h
U : Type
A : Set U
l : List U
⊢ l ∈ ⋃₀ sbl_set A ↔ l ∈ seq A
Tactic:
apply Iff.intro
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

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)
State after:
case h.mp
U : Type
A : Set U
l : List U
h1 : l ∈ ⋃₀ sbl_set A
⊢ l ∈ seq A

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
State after:
case h.mp
U : Type
A : Set U
l : List U
h1 : ∃ t ∈ sbl_set A, l ∈ t
⊢ l ∈ seq A

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
State after:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
⊢ l ∈ ⋃₀ sbl_set A

State before:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
⊢ l ∈ ⋃₀ sbl_set A
Tactic:
define
State after:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l ∈ seq A
⊢ ∃ t ∈ sbl_set A, l ∈ t

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
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

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)
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals