Theorem: Regex.NFA.lt_of_charStep (RegexCorrectness/NFA/Basic.lean)

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

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

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