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

State before:
α : Type
s : Str α
⊢ ∃ n, s ∈ exp α n
Tactic:
obtain s1 := rev_str_mem_exp s.reverse
State after:
α : Type
s : Str α
s1 : ∃ n, (List.reverse s).reverse ∈ exp α n
⊢ ∃ n, s ∈ exp α n

State before:
α : Type
s : Str α
s1 : ∃ n, (List.reverse s).reverse ∈ exp α n
⊢ ∃ n, s ∈ exp α n
Tactic:
simp only [List.reverse_reverse] at s1
State after:
α : Type
s : Str α
s1 : ∃ n, s ∈ exp α n
⊢ ∃ n, s ∈ exp α n

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