Theorem: Regex.NFA.inBounds' (Regex/NFA/Basic.lean)

State before:
n : Node
nfa : NFA
i : Fin nfa.nodes.size
hn : nfa[i] = n
⊢ n.inBounds nfa.nodes.size
Tactic:
rw [←hn]
State after:
n : Node
nfa : NFA
i : Fin nfa.nodes.size
hn : nfa[i] = n
⊢ nfa[i].inBounds nfa.nodes.size

State before:
n : Node
nfa : NFA
i : Fin nfa.nodes.size
hn : nfa[i] = n
⊢ nfa[i].inBounds nfa.nodes.size
Tactic:
have inBounds := nfa.inBounds i
State after:
n : Node
nfa : NFA
i : Fin nfa.nodes.size
hn : nfa[i] = n
inBounds : nfa.nodes[↑i].inBounds nfa.nodes.size
⊢ nfa[i].inBounds nfa.nodes.size

State before:
n : Node
nfa : NFA
i : Fin nfa.nodes.size
hn : nfa[i] = n
inBounds : nfa.nodes[↑i].inBounds nfa.nodes.size
⊢ nfa[i].inBounds nfa.nodes.size
Tactic:
have : nfa[i] = nfa.nodes[i.val] := rfl
State after:
n : Node
nfa : NFA
i : Fin nfa.nodes.size
hn : nfa[i] = n
inBounds : nfa.nodes[↑i].inBounds nfa.nodes.size
this : nfa[i] = nfa.nodes[↑i]
⊢ nfa[i].inBounds nfa.nodes.size

State before:
n : Node
nfa : NFA
i : Fin nfa.nodes.size
hn : nfa[i] = n
inBounds : nfa.nodes[↑i].inBounds nfa.nodes.size
this : nfa[i] = nfa.nodes[↑i]
⊢ nfa[i].inBounds nfa.nodes.size
Tactic:
exact this ▸ inBounds
State after:
no goals