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

State before:
i next : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
assm : i < nfa.nodes.size
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (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
i next : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
assm : i < nfa.nodes.size
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (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
i next : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
assm : i < nfa.nodes.size
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (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:
have path' := path.cast' assm le eq
State after:
case intro.intro.intro.intro.intro
i next : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
assm : i < nfa.nodes.size
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (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
path' : nfa.pathIn start i i' pcs
⊢ nfa.pathToNext next start i cs

State before:
case intro.intro.intro.intro.intro
i next : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
assm : i < nfa.nodes.size
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (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
path' : nfa.pathIn start i i' pcs
⊢ nfa.pathToNext next start i cs
Tactic:
have lt : i' < nfa.nodes.size := path'.lt_right assm
State after:
case intro.intro.intro.intro.intro
i next : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
assm : i < nfa.nodes.size
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (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
path' : nfa.pathIn start i i' pcs
lt : i' < nfa.nodes.size
⊢ nfa.pathToNext next start i cs

State before:
case intro.intro.intro.intro.intro
i next : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
assm : i < nfa.nodes.size
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (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
path' : nfa.pathIn start i i' pcs
lt : i' < nfa.nodes.size
⊢ nfa.pathToNext next start i cs
Tactic:
exact ⟨i', pcs, scs, eqs, path', step.cast lt (eq i' step.h₁ lt).symm⟩
State after:
no goals