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

State before:
nfa : NFA
next start start' i : ℕ
cs : List Char
assm : start' ≤ i
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
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
next start start' i : ℕ
cs : List Char
assm : start' ≤ i
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
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
next start start' i : ℕ
cs : List Char
assm : start' ≤ i
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
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.castLE assm inBounds
State after:
case intro.intro.intro.intro.intro
nfa : NFA
next start start' i : ℕ
cs : List Char
assm : start' ≤ i
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
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
nfa : NFA
next start start' i : ℕ
cs : List Char
assm : start' ≤ i
inBounds :
  ∀ (i j : ℕ),
    start' ≤ i → ∀ (h₂ : i < nfa.nodes.size), (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep → start ≤ j → start' ≤ j
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:
exact ⟨i', pcs, scs, eqs, path', step.castStart' (le_of_pathIn_right path')⟩
State after:
no goals