Theorem: Regex.NFA.pushNode_get_lt (Regex/NFA/Compile.lean)

State before:
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h : i < nfa.nodes.size
⊢ (nfa.pushNode node inBounds).val[i] = nfa[i]
Tactic:
simp [pushNode, get_eq_nodes_get]
State after:
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h : i < nfa.nodes.size
⊢ (nfa.nodes.push node)[i] = nfa.nodes[i]

State before:
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h : i < nfa.nodes.size
⊢ (nfa.nodes.push node)[i] = nfa.nodes[i]
Tactic:
rw [Array.get_push_lt]
State after:
no goals