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

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

State before:
case base
j k : ℕ
nfa : NFA
i : ℕ
cs : List Char
c : Char
start i✝ : ℕ
h : start ≤ i✝
assm : i✝ < nfa.nodes.size
step : k ∈ nfa[i✝].charStep c
⊢ nfa.pathIn (min start k) i✝ k ([] ++ [c])
Tactic:
simp
State after:
case base
j k : ℕ
nfa : NFA
i : ℕ
cs : List Char
c : Char
start i✝ : ℕ
h : start ≤ i✝
assm : i✝ < nfa.nodes.size
step : k ∈ nfa[i✝].charStep c
⊢ nfa.pathIn (min start k) i✝ k [c]

State before:
case base
j k : ℕ
nfa : NFA
i : ℕ
cs : List Char
c : Char
start i✝ : ℕ
h : start ≤ i✝
assm : i✝ < nfa.nodes.size
step : k ∈ nfa[i✝].charStep c
⊢ nfa.pathIn (min start k) i✝ k [c]
Tactic:
exact .step (.charStep (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
c : 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'].charStep c → nfa.pathIn (min start k) j k (cs''' ++ [c])
assm : k' < nfa.nodes.size
step : k ∈ nfa[k'].charStep c
⊢ nfa.pathIn (min start k) i k (cs'' ++ cs''' ++ [c])
Tactic:
simp
State after:
case step
j✝ k : ℕ
nfa : NFA
i✝ : ℕ
cs : List Char
c : 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'].charStep c → nfa.pathIn (min start k) j k (cs''' ++ [c])
assm : k' < nfa.nodes.size
step : k ∈ nfa[k'].charStep c
⊢ nfa.pathIn (min start k) i k (cs'' ++ (cs''' ++ [c]))

State before:
case step
j✝ k : ℕ
nfa : NFA
i✝ : ℕ
cs : List Char
c : 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'].charStep c → nfa.pathIn (min start k) j k (cs''' ++ [c])
assm : k' < nfa.nodes.size
step : k ∈ nfa[k'].charStep c
⊢ nfa.pathIn (min start k) i k (cs'' ++ (cs''' ++ [c]))
Tactic:
have ih := ih assm step
State after:
case step
j✝ k : ℕ
nfa : NFA
i✝ : ℕ
cs : List Char
c : 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'].charStep c → nfa.pathIn (min start k) j k (cs''' ++ [c])
assm : k' < nfa.nodes.size
step : k ∈ nfa[k'].charStep c
ih : nfa.pathIn (min start k) j k (cs''' ++ [c])
⊢ nfa.pathIn (min start k) i k (cs'' ++ (cs''' ++ [c]))

State before:
case step
j✝ k : ℕ
nfa : NFA
i✝ : ℕ
cs : List Char
c : 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'].charStep c → nfa.pathIn (min start k) j k (cs''' ++ [c])
assm : k' < nfa.nodes.size
step : k ∈ nfa[k'].charStep c
ih : nfa.pathIn (min start k) j k (cs''' ++ [c])
⊢ nfa.pathIn (min start k) i k (cs'' ++ (cs''' ++ [c]))
Tactic:
exact pathIn.step (step'.castStart (Nat.min_le_left _ _)) ih
State after:
no goals