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

State before:
i j : ℕ
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'.pathIn start i j cs
⊢ nfa.pathIn start i j cs
Tactic:
induction path with
| base h => exact .base h
| @step i j k cs cs' step _ ih =>
  have eq := eq _ step.h₁ assm
  have : j < nfa.nodes.size := by
    cases step with
    | @charStep c _ _ step => exact lt_of_charStep (eq.symm ▸ step)
    | εStep _ _ step => exact lt_of_εStep (eq.symm ▸ step)
  exact .step (step.cast assm eq.symm) (ih this)
State after:
no goals

State before:
case base
i j : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i✝ : ℕ
h : start ≤ i✝
assm : i✝ < nfa.nodes.size
⊢ 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 : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq : ∀ (i : ℕ), start ≤ i → ∀ (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 : j < nfa.nodes.size → nfa.pathIn start j k cs'
assm : i < nfa.nodes.size
⊢ nfa.pathIn start i k (cs ++ cs')
Tactic:
have eq := eq _ step.h₁ assm
State after:
case step
i✝ j✝ : ℕ
cs✝ : List Char
nfa nfa' : NFA
start : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (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 : j < nfa.nodes.size → nfa.pathIn start j k cs'
assm : 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 : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (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 : j < nfa.nodes.size → nfa.pathIn start j k cs'
assm : i < nfa.nodes.size
eq : nfa[i] = nfa'[i]
⊢ nfa.pathIn start i k (cs ++ cs')
Tactic:
have : j < nfa.nodes.size := by
  cases step with
  | @charStep c _ _ step => exact lt_of_charStep (eq.symm ▸ step)
  | εStep _ _ step => exact lt_of_εStep (eq.symm ▸ step)
State after:
case step
i✝ j✝ : ℕ
cs✝ : List Char
nfa nfa' : NFA
start : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (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 : j < nfa.nodes.size → nfa.pathIn start j k cs'
assm : i < nfa.nodes.size
eq : nfa[i] = nfa'[i]
this : j < nfa.nodes.size
⊢ nfa.pathIn start i k (cs ++ cs')

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

State before:
i✝ j✝ : ℕ
cs✝ : List Char
nfa nfa' : NFA
start : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (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 : j < nfa.nodes.size → nfa.pathIn start j k cs'
assm : i < nfa.nodes.size
eq : nfa[i] = nfa'[i]
⊢ j < nfa.nodes.size
Tactic:
cases step with
| @charStep c _ _ step => exact lt_of_charStep (eq.symm ▸ step)
| εStep _ _ step => exact lt_of_εStep (eq.symm ▸ step)
State after:
no goals

State before:
case charStep
i✝ j✝ : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i j k : ℕ
cs' : List Char
rest✝ : nfa'.pathIn start j k cs'
ih : j < nfa.nodes.size → nfa.pathIn start j k cs'
assm : i < nfa.nodes.size
eq : nfa[i] = nfa'[i]
c : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa'.nodes.size
step : j ∈ nfa'[i].charStep c
⊢ j < nfa.nodes.size
Tactic:
exact lt_of_charStep (eq.symm ▸ step)
State after:
no goals

State before:
case εStep
i✝ j✝ : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
le : nfa.nodes.size ≤ nfa'.nodes.size
eq✝ : ∀ (i : ℕ), start ≤ i → ∀ (h₂ : i < nfa.nodes.size), nfa[i] = nfa'[i]
i j k : ℕ
cs' : List Char
rest✝ : nfa'.pathIn start j k cs'
ih : j < nfa.nodes.size → nfa.pathIn start j k cs'
assm : i < nfa.nodes.size
eq : nfa[i] = nfa'[i]
h₁✝ : start ≤ i
h₂✝ : i < nfa'.nodes.size
step : j ∈ nfa'[i].εStep
⊢ j < nfa.nodes.size
Tactic:
exact lt_of_εStep (eq.symm ▸ step)
State after:
no goals