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

State before:
nfa nfa' : NFA
next start i : ℕ
cs : List Char
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
path : nfa.pathToNext next start i cs
⊢ nfa'.pathToNext next start i cs
Tactic:
obtain ⟨i', pcs, scs, eqs, path, step⟩ := path
State after:
case intro.intro.intro.intro.intro
nfa nfa' : NFA
next start i : ℕ
cs : List Char
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
⊢ nfa'.pathToNext next start i cs

State before:
case intro.intro.intro.intro.intro
nfa nfa' : NFA
next start i : ℕ
cs : List Char
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
⊢ nfa'.pathToNext next start i cs
Tactic:
obtain ⟨h', eq'⟩ := eq _ (le_of_pathIn_right path) step.h₂
State after:
case intro.intro.intro.intro.intro.intro
nfa nfa' : NFA
next start i : ℕ
cs : List Char
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
h' : i' < nfa'.nodes.size
eq' : nfa[i'] = nfa'[i']
⊢ nfa'.pathToNext next start i cs

State before:
case intro.intro.intro.intro.intro.intro
nfa nfa' : NFA
next start i : ℕ
cs : List Char
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
h' : i' < nfa'.nodes.size
eq' : nfa[i'] = nfa'[i']
⊢ nfa'.pathToNext next start i cs
Tactic:
exact ⟨i', pcs, scs, eqs, pathIn.cast start eq path, step.cast h' eq'⟩
State after:
no goals