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

State before:
j k : ℕ
nfa : NFA
i : ℕ
cs : List Char
start : ℕ
assm : j < nfa.nodes.size
step : k ∈ nfa[j].εStep
path : nfa.pathIn start i j cs
⊢ nfa.pathIn (min start k) i k cs
Tactic:
induction path with
| base h =>
  exact .step (.εStep (Nat.le_trans (Nat.min_le_left _ _) h) assm step) (.base (Nat.min_le_right _ _))
| step step' rest ih =>
  have ih := ih assm step
  exact .step (step'.castStart (Nat.min_le_left _ _)) ih
State after:
no goals

State before:
case base
j k : ℕ
nfa : NFA
i : ℕ
cs : List Char
start i✝ : ℕ
h : start ≤ i✝
assm : i✝ < nfa.nodes.size
step : k ∈ nfa[i✝].εStep
⊢ nfa.pathIn (min start k) i✝ k []
Tactic:
exact .step (.εStep (Nat.le_trans (Nat.min_le_left _ _) h) assm step) (.base (Nat.min_le_right _ _))
State after:
no goals

State before:
case step
j k : ℕ
nfa : NFA
i : ℕ
cs : List Char
start i✝ j✝ k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn start i✝ j✝ cs₁✝
rest : nfa.pathIn start j✝ k✝ cs₂✝
ih : ∀ (assm : k✝ < nfa.nodes.size), k ∈ nfa[k✝].εStep → nfa.pathIn (min start k) j✝ k cs₂✝
assm : k✝ < nfa.nodes.size
step : k ∈ nfa[k✝].εStep
⊢ nfa.pathIn (min start k) i✝ k (cs₁✝ ++ cs₂✝)
Tactic:
have ih := ih assm step
State after:
case step
j k : ℕ
nfa : NFA
i : ℕ
cs : List Char
start i✝ j✝ k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn start i✝ j✝ cs₁✝
rest : nfa.pathIn start j✝ k✝ cs₂✝
ih✝ : ∀ (assm : k✝ < nfa.nodes.size), k ∈ nfa[k✝].εStep → nfa.pathIn (min start k) j✝ k cs₂✝
assm : k✝ < nfa.nodes.size
step : k ∈ nfa[k✝].εStep
ih : nfa.pathIn (min start k) j✝ k cs₂✝
⊢ nfa.pathIn (min start k) i✝ k (cs₁✝ ++ cs₂✝)

State before:
case step
j k : ℕ
nfa : NFA
i : ℕ
cs : List Char
start i✝ j✝ k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn start i✝ j✝ cs₁✝
rest : nfa.pathIn start j✝ k✝ cs₂✝
ih✝ : ∀ (assm : k✝ < nfa.nodes.size), k ∈ nfa[k✝].εStep → nfa.pathIn (min start k) j✝ k cs₂✝
assm : k✝ < nfa.nodes.size
step : k ∈ nfa[k✝].εStep
ih : nfa.pathIn (min start k) j✝ k cs₂✝
⊢ nfa.pathIn (min start k) i✝ k (cs₁✝ ++ cs₂✝)
Tactic:
exact .step (step'.castStart (Nat.min_le_left _ _)) ih
State after:
no goals