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

State before:
j i k : ℕ
nfa : NFA
start : ℕ
cs cs' : List Char
path₁ : nfa.pathToNext j start i cs
path₂ : nfa.pathToNext k start j cs'
⊢ nfa.pathToNext k start i (cs ++ cs')
Tactic:
obtain ⟨i₁, pcs₁, scs₁, eqs₁, path₁, step₁⟩ := path₁
State after:
case intro.intro.intro.intro.intro
j i k : ℕ
nfa : NFA
start : ℕ
cs cs' : List Char
path₂ : nfa.pathToNext k start j cs'
i₁ : ℕ
pcs₁ scs₁ : List Char
eqs₁ : cs = pcs₁ ++ scs₁
path₁ : nfa.pathIn start i i₁ pcs₁
step₁ : nfa.stepIn start i₁ j scs₁
⊢ nfa.pathToNext k start i (cs ++ cs')

State before:
case intro.intro.intro.intro.intro
j i k : ℕ
nfa : NFA
start : ℕ
cs cs' : List Char
path₂ : nfa.pathToNext k start j cs'
i₁ : ℕ
pcs₁ scs₁ : List Char
eqs₁ : cs = pcs₁ ++ scs₁
path₁ : nfa.pathIn start i i₁ pcs₁
step₁ : nfa.stepIn start i₁ j scs₁
⊢ nfa.pathToNext k start i (cs ++ cs')
Tactic:
obtain ⟨i₂, pcs₂, scs₂, eqs₂, path₂, step₂⟩ := path₂
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
j i k : ℕ
nfa : NFA
start : ℕ
cs cs' : List Char
i₁ : ℕ
pcs₁ scs₁ : List Char
eqs₁ : cs = pcs₁ ++ scs₁
path₁ : nfa.pathIn start i i₁ pcs₁
step₁ : nfa.stepIn start i₁ j scs₁
i₂ : ℕ
pcs₂ scs₂ : List Char
eqs₂ : cs' = pcs₂ ++ scs₂
path₂ : nfa.pathIn start j i₂ pcs₂
step₂ : nfa.stepIn start i₂ k scs₂
⊢ nfa.pathToNext k start i (cs ++ cs')

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
j i k : ℕ
nfa : NFA
start : ℕ
cs cs' : List Char
i₁ : ℕ
pcs₁ scs₁ : List Char
eqs₁ : cs = pcs₁ ++ scs₁
path₁ : nfa.pathIn start i i₁ pcs₁
step₁ : nfa.stepIn start i₁ j scs₁
i₂ : ℕ
pcs₂ scs₂ : List Char
eqs₂ : cs' = pcs₂ ++ scs₂
path₂ : nfa.pathIn start j i₂ pcs₂
step₂ : nfa.stepIn start i₂ k scs₂
⊢ nfa.pathToNext k start i (cs ++ cs')
Tactic:
exact ⟨i₂, pcs₁ ++ (scs₁ ++ pcs₂), scs₂, by simp [eqs₁, eqs₂], path₁.trans (.step step₁ path₂), step₂⟩
State after:
no goals

State before:
j i k : ℕ
nfa : NFA
start : ℕ
cs cs' : List Char
i₁ : ℕ
pcs₁ scs₁ : List Char
eqs₁ : cs = pcs₁ ++ scs₁
path₁ : nfa.pathIn start i i₁ pcs₁
step₁ : nfa.stepIn start i₁ j scs₁
i₂ : ℕ
pcs₂ scs₂ : List Char
eqs₂ : cs' = pcs₂ ++ scs₂
path₂ : nfa.pathIn start j i₂ pcs₂
step₂ : nfa.stepIn start i₂ k scs₂
⊢ cs ++ cs' = pcs₁ ++ (scs₁ ++ pcs₂) ++ scs₂
Tactic:
simp [eqs₁, eqs₂]
State after:
no goals