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

State before:
U : Type
A : Set U
⊢ seq_by_length A 0 = {[]}
Tactic:
apply Set.ext
State after:
case h
U : Type
A : Set U
⊢ ∀ (x : List U), x ∈ seq_by_length A 0 ↔ x ∈ {[]}

State before:
case h
U : Type
A : Set U
⊢ ∀ (x : List U), x ∈ seq_by_length A 0 ↔ x ∈ {[]}
Tactic:
fix l : List U
State after:
case h
U : Type
A : Set U
l : List U
⊢ l ∈ seq_by_length A 0 ↔ l ∈ {[]}

State before:
case h
U : Type
A : Set U
l : List U
⊢ l ∈ seq_by_length A 0 ↔ l ∈ {[]}
Tactic:
apply Iff.intro
State after:
case h.mp
U : Type
A : Set U
l : List U
⊢ l ∈ seq_by_length A 0 → l ∈ {[]}

case h.mpr
U : Type
A : Set U
l : List U
⊢ l ∈ {[]} → l ∈ seq_by_length A 0

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
State after:
case h.mp
U : Type
A : Set U
l : List U
h1 : l ∈ seq_by_length A 0
⊢ l ∈ {[]}

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
State after:
case h.mp
U : Type
A : Set U
l : List U
h1 : l ∈ seq A ∧ List.length l = 0
⊢ l ∈ {[]}

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
State after:
case h.mp
U : Type
A : Set U
l : List U
h1 : l ∈ seq A ∧ l = []
⊢ l ∈ {[]}

State before:
case h.mp
U : Type
A : Set U
l : List U
h1 : l ∈ seq A ∧ l = []
⊢ l ∈ {[]}
Tactic:
define
State after:
case h.mp
U : Type
A : Set U
l : List U
h1 : l ∈ seq A ∧ l = []
⊢ l = []

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

State before:
case h.mpr
U : Type
A : Set U
l : List U
⊢ l ∈ {[]} → l ∈ seq_by_length A 0
Tactic:
assume h1 : l ∈ {[]}
State after:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l ∈ {[]}
⊢ l ∈ seq_by_length A 0

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
State after:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l = []
⊢ l ∈ seq_by_length A 0

State before:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l = []
⊢ l ∈ seq_by_length A 0
Tactic:
define
State after:
case h.mpr
U : Type
A : Set U
l : List U
h1 : l = []
⊢ l ∈ seq A ∧ List.length l = 0

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)
State after:
U : Type
A : Set U
l : List U
h1 : l = []
⊢ l ∈ seq A

State before:
U : Type
A : Set U
l : List U
h1 : l = []
⊢ l ∈ seq A
Tactic:
define
State after:
U : Type
A : Set U
l : List U
h1 : l = []
⊢ ∀ x ∈ l, x ∈ A

State before:
U : Type
A : Set U
l : List U
h1 : l = []
⊢ ∀ x ∈ l, x ∈ A
Tactic:
fix x : U
State after:
U : Type
A : Set U
l : List U
h1 : l = []
x : U
⊢ x ∈ l → x ∈ A

State before:
U : Type
A : Set U
l : List U
h1 : l = []
x : U
⊢ x ∈ l → x ∈ A
Tactic:
assume h2 : x ∈ l
State after:
U : Type
A : Set U
l : List U
h1 : l = []
x : U
h2 : x ∈ l
⊢ x ∈ A

State before:
U : Type
A : Set U
l : List U
h1 : l = []
x : U
h2 : x ∈ l
⊢ x ∈ A
Tactic:
contradict h2 with h3
State after:
U : Type
A : Set U
l : List U
h1 : l = []
x : U
h2 : x ∈ l
h3 : ¬x ∈ A
⊢ x ∉ l

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]
State after:
U : Type
A : Set U
l : List U
h1 : l = []
x : U
h2 : x ∈ l
h3 : ¬x ∈ A
⊢ x ∉ []

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