Theorem: Regex.NFA.lt_of_εStep (RegexCorrectness/NFA/Basic.lean)

State before:
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa[i].εStep
⊢ j < nfa.nodes.size
Tactic:
have inBounds := nfa.inBounds ⟨i, h⟩
State after:
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa[i].εStep
inBounds : nfa.nodes[↑⟨i, h⟩].inBounds nfa.nodes.size
⊢ j < nfa.nodes.size

State before:
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa[i].εStep
inBounds : nfa.nodes[↑⟨i, h⟩].inBounds nfa.nodes.size
⊢ j < nfa.nodes.size
Tactic:
simp [get_eq_nodes_get] at mem
State after:
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa.nodes[i].εStep
inBounds : nfa.nodes[↑⟨i, h⟩].inBounds nfa.nodes.size
⊢ j < nfa.nodes.size

State before:
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa.nodes[i].εStep
inBounds : nfa.nodes[↑⟨i, h⟩].inBounds nfa.nodes.size
⊢ j < nfa.nodes.size
Tactic:
exact lt_of_inBounds_of_εStep inBounds mem
State after:
no goals