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

State before:
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h : i < (nfa.pushNode node inBounds).val.nodes.size
⊢ (nfa.pushNode node inBounds).val[i] = if h' : i < nfa.nodes.size then nfa[i] else node
Tactic:
simp at h
State after:
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h✝ : i < (nfa.pushNode node inBounds).val.nodes.size
h : i < nfa.nodes.size + 1
⊢ (nfa.pushNode node inBounds).val[i] = if h' : i < nfa.nodes.size then nfa[i] else node

State before:
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h✝ : i < (nfa.pushNode node inBounds).val.nodes.size
h : i < nfa.nodes.size + 1
⊢ (nfa.pushNode node inBounds).val[i] = if h' : i < nfa.nodes.size then nfa[i] else node
Tactic:
cases Nat.lt_or_eq_of_le (Nat.le_of_succ_le_succ h) with
| inl lt => simp [lt, pushNode_get_lt _ lt]
| inr eq => simp [eq]
State after:
no goals

State before:
case inl
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h✝ : i < (nfa.pushNode node inBounds).val.nodes.size
h : i < nfa.nodes.size + 1
lt : i < nfa.nodes.size
⊢ (nfa.pushNode node inBounds).val[i] = if h' : i < nfa.nodes.size then nfa[i] else node
Tactic:
simp [lt, pushNode_get_lt _ lt]
State after:
no goals

State before:
case inr
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h✝ : i < (nfa.pushNode node inBounds).val.nodes.size
h : i < nfa.nodes.size + 1
eq : i = nfa.nodes.size
⊢ (nfa.pushNode node inBounds).val[i] = if h' : i < nfa.nodes.size then nfa[i] else node
Tactic:
simp [eq]
State after:
no goals