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

State before:
α : Type
s : Str α
⊢ List.reverse s ∈ exp α (List.length s)
Tactic:
induction s
State after:
case nil
α : Type
⊢ [].reverse ∈ exp α [].length

case cons
α : Type
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝.reverse ∈ exp α tail✝.length
⊢ (head✝ :: tail✝).reverse ∈ exp α (head✝ :: tail✝).length

State before:
α : Type
⊢ [].reverse ∈ exp α [].length
Tactic:
case nil =>
  simp
  exact exp.zero
State after:
no goals

State before:
α : Type
hd : α
tl : List α
ih : tl.reverse ∈ exp α tl.length
⊢ (hd :: tl).reverse ∈ exp α (hd :: tl).length
Tactic:
case cons hd tl ih =>
  simp
  exact exp.succ tl.length hd tl.reverse ih
State after:
no goals

State before:
α : Type
⊢ [].reverse ∈ exp α [].length
Tactic:
simp
State after:
α : Type
⊢ [] ∈ exp α 0

State before:
α : Type
⊢ [] ∈ exp α 0
Tactic:
exact exp.zero
State after:
no goals

State before:
α : Type
hd : α
tl : List α
ih : tl.reverse ∈ exp α tl.length
⊢ (hd :: tl).reverse ∈ exp α (hd :: tl).length
Tactic:
simp
State after:
α : Type
hd : α
tl : List α
ih : tl.reverse ∈ exp α tl.length
⊢ tl.reverse ++ [hd] ∈ exp α (tl.length + 1)

State before:
α : Type
hd : α
tl : List α
ih : tl.reverse ∈ exp α tl.length
⊢ tl.reverse ++ [hd] ∈ exp α (tl.length + 1)
Tactic:
exact exp.succ tl.length hd tl.reverse ih
State after:
no goals