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

State before:
i j : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
path : nfa.pathIn start i j cs
⊢ nfa'.pathIn start i j cs
Tactic:
induction path with
| base h => exact .base h
| step step _ ih =>
  let ⟨h, eq⟩ := eq _ step.h₁ step.h₂
  exact .step (step.cast h eq) ih
State after:
no goals

State before:
case base
i j : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
i✝ : ℕ
h : start ≤ i✝
⊢ nfa'.pathIn start i✝ i✝ []
Tactic:
exact .base h
State after:
no goals

State before:
case step
i j : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
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 j✝ k✝ cs₂✝
⊢ nfa'.pathIn start i✝ k✝ (cs₁✝ ++ cs₂✝)
Tactic:
let ⟨h, eq⟩ := eq _ step.h₁ step.h₂
State after:
case step
i j : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
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 j✝ k✝ cs₂✝
h : i✝ < nfa'.nodes.size
eq : nfa[i✝] = nfa'[i✝]
⊢ nfa'.pathIn start i✝ k✝ (cs₁✝ ++ cs₂✝)

State before:
case step
i j : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), ∃ (h' : i < nfa'.nodes.size), nfa[i] = nfa'[i]
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 j✝ k✝ cs₂✝
h : i✝ < nfa'.nodes.size
eq : nfa[i✝] = nfa'[i✝]
⊢ nfa'.pathIn start i✝ k✝ (cs₁✝ ++ cs₂✝)
Tactic:
exact .step (step.cast h eq) ih
State after:
no goals