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

State before:
α : Type
s : Str α
⊢ ∃ n, List.reverse s ∈ exp α n
Tactic:
induction s
State after:
case nil
α : Type
⊢ ∃ n, [].reverse ∈ exp α n

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

State before:
α : Type
⊢ ∃ n, [].reverse ∈ exp α n
Tactic:
case nil =>
  apply Exists.intro 0
  exact exp.zero
State after:
no goals

State before:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
⊢ ∃ n, (hd :: tl).reverse ∈ exp α n
Tactic:
case cons hd tl ih =>
  apply Exists.elim ih
  intro n a1
  apply Exists.intro (n + 1)
  simp
  exact exp.succ n hd tl.reverse a1
State after:
no goals

State before:
α : Type
⊢ ∃ n, [].reverse ∈ exp α n
Tactic:
apply Exists.intro 0
State after:
α : Type
⊢ [].reverse ∈ exp α 0

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

State before:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
⊢ ∃ n, (hd :: tl).reverse ∈ exp α n
Tactic:
apply Exists.elim ih
State after:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
⊢ ∀ (a : ℕ), tl.reverse ∈ exp α a → ∃ n, (hd :: tl).reverse ∈ exp α n

State before:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
⊢ ∀ (a : ℕ), tl.reverse ∈ exp α a → ∃ n, (hd :: tl).reverse ∈ exp α n
Tactic:
intro n a1
State after:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
n : ℕ
a1 : tl.reverse ∈ exp α n
⊢ ∃ n, (hd :: tl).reverse ∈ exp α n

State before:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
n : ℕ
a1 : tl.reverse ∈ exp α n
⊢ ∃ n, (hd :: tl).reverse ∈ exp α n
Tactic:
apply Exists.intro (n + 1)
State after:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
n : ℕ
a1 : tl.reverse ∈ exp α n
⊢ (hd :: tl).reverse ∈ exp α (n + 1)

State before:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
n : ℕ
a1 : tl.reverse ∈ exp α n
⊢ (hd :: tl).reverse ∈ exp α (n + 1)
Tactic:
simp
State after:
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
n : ℕ
a1 : tl.reverse ∈ exp α n
⊢ tl.reverse ++ [hd] ∈ exp α (n + 1)

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