Theorem: Regex.NFA.pathIn.trans (RegexCorrectness/NFA/Transition/Path/Basic.lean)

State before:
nfa : NFA
i j : ℕ
cs : List Char
k : ℕ
cs' : List Char
start : ℕ
path₁ : nfa.pathIn start i j cs
path₂ : nfa.pathIn start j k cs'
⊢ nfa.pathIn start i k (cs ++ cs')
Tactic:
induction path₁ with
| base _ => exact path₂
| step step _ ih =>
  simp
  exact .step step (ih path₂)
State after:
no goals

State before:
case base
nfa : NFA
i j : ℕ
cs : List Char
k : ℕ
cs' : List Char
start i✝ : ℕ
h✝ : start ≤ i✝
path₂ : nfa.pathIn start i✝ k cs'
⊢ nfa.pathIn start i✝ k ([] ++ cs')
Tactic:
exact path₂
State after:
no goals

State before:
case step
nfa : NFA
i j : ℕ
cs : List Char
k : ℕ
cs' : List Char
start i✝ j✝ k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : nfa.stepIn start i✝ j✝ cs₁✝
rest✝ : nfa.pathIn start j✝ k✝ cs₂✝
ih : nfa.pathIn start k✝ k cs' → nfa.pathIn start j✝ k (cs₂✝ ++ cs')
path₂ : nfa.pathIn start k✝ k cs'
⊢ nfa.pathIn start i✝ k (cs₁✝ ++ cs₂✝ ++ cs')
Tactic:
simp
State after:
case step
nfa : NFA
i j : ℕ
cs : List Char
k : ℕ
cs' : List Char
start i✝ j✝ k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : nfa.stepIn start i✝ j✝ cs₁✝
rest✝ : nfa.pathIn start j✝ k✝ cs₂✝
ih : nfa.pathIn start k✝ k cs' → nfa.pathIn start j✝ k (cs₂✝ ++ cs')
path₂ : nfa.pathIn start k✝ k cs'
⊢ nfa.pathIn start i✝ k (cs₁✝ ++ (cs₂✝ ++ cs'))

State before:
case step
nfa : NFA
i j : ℕ
cs : List Char
k : ℕ
cs' : List Char
start i✝ j✝ k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : nfa.stepIn start i✝ j✝ cs₁✝
rest✝ : nfa.pathIn start j✝ k✝ cs₂✝
ih : nfa.pathIn start k✝ k cs' → nfa.pathIn start j✝ k (cs₂✝ ++ cs')
path₂ : nfa.pathIn start k✝ k cs'
⊢ nfa.pathIn start i✝ k (cs₁✝ ++ (cs₂✝ ++ cs'))
Tactic:
exact .step step (ih path₂)
State after:
no goals