Theorem: Strings.all_str_mem_kleene_closure (FOL/Parsing/Text.lean)

State before:
α : Type
s : Str α
⊢ s ∈ kleene_closure α
Tactic:
simp only [kleene_closure]
State after:
α : Type
s : Str α
⊢ s ∈ ⋃ n, exp α n

State before:
α : Type
s : Str α
⊢ s ∈ ⋃ n, exp α n
Tactic:
simp
State after:
α : Type
s : Str α
⊢ ∃ i, s ∈ exp α i

State before:
α : Type
s : Str α
⊢ ∃ i, s ∈ exp α i
Tactic:
exact str_mem_exp s
State after:
no goals