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

State before:
α : Type
s : Str α
⊢ s ∈ exp α (List.length s)
Tactic:
obtain s1 := rev_str_mem_exp_str_len s.reverse
State after:
α : Type
s : Str α
s1 : (List.reverse s).reverse ∈ exp α (List.reverse s).length
⊢ s ∈ exp α (List.length s)

State before:
α : Type
s : Str α
s1 : (List.reverse s).reverse ∈ exp α (List.reverse s).length
⊢ s ∈ exp α (List.length s)
Tactic:
simp at s1
State after:
α : Type
s : Str α
s1 : s ∈ exp α (List.length s)
⊢ s ∈ exp α (List.length s)

State before:
α : Type
s : Str α
s1 : s ∈ exp α (List.length s)
⊢ s ∈ exp α (List.length s)
Tactic:
exact s1
State after:
no goals