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

State before:
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
⊢ (nfa.pushNode node inBounds).val[nfa.nodes.size] = node
Tactic:
simp [pushNode, get_eq_nodes_get]
State after:
no goals