Theorem: Word.ε_mem_prefixes (WTA.lean)

State before:
α : Type
u : α⋆
⊢ ε ∈ prefixes u
Tactic:
induction u
State after:
case nil
α : Type
⊢ ε ∈ prefixes []

case cons
α : Type
head✝ : α
tail✝ : List α
tail_ih✝ : ε ∈ prefixes tail✝
⊢ ε ∈ prefixes (head✝ :: tail✝)

State before:
α : Type
⊢ ε ∈ prefixes []
Tactic:
case nil => simp [prefixes, Set.mem_singleton]
State after:
no goals

State before:
α : Type
i : α
v : List α
hi : ε ∈ prefixes v
⊢ ε ∈ prefixes (i :: v)
Tactic:
case cons i v hi => 
  simp [prefixes] 
  simp [Membership.mem] at *
  exact hi
State after:
no goals

State before:
α : Type
⊢ ε ∈ prefixes []
Tactic:
simp [prefixes, Set.mem_singleton]
State after:
no goals

State before:
α : Type
i : α
v : List α
hi : ε ∈ prefixes v
⊢ ε ∈ prefixes (i :: v)
Tactic:
simp [prefixes]
State after:
α : Type
i : α
v : List α
hi : ε ∈ prefixes v
⊢ ε ∈ fun u => u = i⬝v ∨ u ∈ prefixes v

State before:
α : Type
i : α
v : List α
hi : ε ∈ prefixes v
⊢ ε ∈ fun u => u = i⬝v ∨ u ∈ prefixes v
Tactic:
simp [Membership.mem] at *
State after:
α : Type
i : α
v : List α
hi : prefixes v ε
⊢ prefixes v ε

State before:
α : Type
i : α
v : List α
hi : prefixes v ε
⊢ prefixes v ε
Tactic:
exact hi
State after:
no goals