Theorem: Regex.NFA.stepIn.nil_of_snoc (RegexCorrectness/NFA/Transition/Path/Basic.lean)

State before:
nfa : NFA
i j : ℕ
cs : List Char
c : Char
start : ℕ
h : nfa.stepIn start i j (cs ++ [c])
⊢ cs = []
Tactic:
generalize h' : cs ++ [c] = cs' at h
State after:
nfa : NFA
i j : ℕ
cs : List Char
c : Char
start : ℕ
cs' : List Char
h' : cs ++ [c] = cs'
h : nfa.stepIn start i j cs'
⊢ cs = []

State before:
nfa : NFA
i j : ℕ
cs : List Char
c : Char
start : ℕ
cs' : List Char
h' : cs ++ [c] = cs'
h : nfa.stepIn start i j cs'
⊢ cs = []
Tactic:
cases h with
| εStep => simp at h'
| charStep =>
  cases cs with
  | nil => rfl
  | cons _ _ =>
    have := congrArg List.length h'
    simp at this
State after:
no goals

State before:
case εStep
nfa : NFA
i j : ℕ
cs : List Char
c : Char
start : ℕ
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].εStep
h' : cs ++ [c] = []
⊢ cs = []
Tactic:
simp at h'
State after:
no goals

State before:
case charStep
nfa : NFA
i j : ℕ
cs : List Char
c : Char
start : ℕ
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].charStep c✝
h' : cs ++ [c] = [c✝]
⊢ cs = []
Tactic:
cases cs with
| nil => rfl
| cons _ _ =>
  have := congrArg List.length h'
  simp at this
State after:
no goals

State before:
case charStep.nil
nfa : NFA
i j : ℕ
c : Char
start : ℕ
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].charStep c✝
h' : [] ++ [c] = [c✝]
⊢ [] = []
Tactic:
rfl
State after:
no goals

State before:
case charStep.cons
nfa : NFA
i j : ℕ
c : Char
start : ℕ
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].charStep c✝
head✝ : Char
tail✝ : List Char
h' : head✝ :: tail✝ ++ [c] = [c✝]
⊢ head✝ :: tail✝ = []
Tactic:
have := congrArg List.length h'
State after:
case charStep.cons
nfa : NFA
i j : ℕ
c : Char
start : ℕ
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].charStep c✝
head✝ : Char
tail✝ : List Char
h' : head✝ :: tail✝ ++ [c] = [c✝]
this : (head✝ :: tail✝ ++ [c]).length = [c✝].length
⊢ head✝ :: tail✝ = []

State before:
case charStep.cons
nfa : NFA
i j : ℕ
c : Char
start : ℕ
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].charStep c✝
head✝ : Char
tail✝ : List Char
h' : head✝ :: tail✝ ++ [c] = [c✝]
this : (head✝ :: tail✝ ++ [c]).length = [c✝].length
⊢ head✝ :: tail✝ = []
Tactic:
simp at this
State after:
no goals