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

State before:
α : Type
s : Str α
n : ℕ
h1 : s ∈ exp α n
⊢ List.length s = n
Tactic:
induction h1
State after:
case zero
α : Type
s : Str α
n : ℕ
⊢ [].length = 0

case succ
α : Type
s : Str α
n n✝ : ℕ
a✝¹ : α
s✝ : Str α
a✝ : s✝ ∈ exp α n✝
a_ih✝ : List.length s✝ = n✝
⊢ List.length (s✝ ++ [a✝¹]) = n✝ + 1

State before:
α : Type
s : Str α
n : ℕ
⊢ [].length = 0
Tactic:
case zero =>
  simp
State after:
no goals

State before:
α : Type
s✝ : Str α
n m : ℕ
a : α
s : Str α
ih_1 : s ∈ exp α m
ih_2 : List.length s = m
⊢ List.length (s ++ [a]) = m + 1
Tactic:
case succ m a s ih_1 ih_2 =>
  simp
  exact ih_2
State after:
no goals

State before:
α : Type
s : Str α
n : ℕ
⊢ [].length = 0
Tactic:
simp
State after:
no goals

State before:
α : Type
s✝ : Str α
n m : ℕ
a : α
s : Str α
ih_1 : s ∈ exp α m
ih_2 : List.length s = m
⊢ List.length (s ++ [a]) = m + 1
Tactic:
simp
State after:
α : Type
s✝ : Str α
n m : ℕ
a : α
s : Str α
ih_1 : s ∈ exp α m
ih_2 : List.length s = m
⊢ List.length s = m

State before:
α : Type
s✝ : Str α
n m : ℕ
a : α
s : Str α
ih_1 : s ∈ exp α m
ih_2 : List.length s = m
⊢ List.length s = m
Tactic:
exact ih_2
State after:
no goals