Theorem: Regex.NFA.pathToNext_of_compile_of_pathIn (RegexCorrectness/NFA/Transition/Path/Equivalence.lean)

State before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathIn 0 (↑nfa.start) 0 cs
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
Tactic:
have : 0 < nfa.start.val := by
  rw [←eq, compile]
  exact ge_pushRegex_start (rfl : NFA.done.pushRegex _ r = _)
State after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathIn 0 (↑nfa.start) 0 cs
this : 0 < ↑nfa.start
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs

State before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathIn 0 (↑nfa.start) 0 cs
this : 0 < ↑nfa.start
⊢ nfa.pathToNext 0 1 (↑nfa.start) cs
Tactic:
exact pathToNext_of_compile_of_pathInAux eq this rfl path
State after:
no goals

State before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathIn 0 (↑nfa.start) 0 cs
⊢ 0 < ↑nfa.start
Tactic:
rw [←eq, compile]
State after:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathIn 0 (↑nfa.start) 0 cs
⊢ 0 < ↑(↑(done.pushRegex ⟨0, compile.proof_1⟩ r)).start

State before:
r : Data.Expr
nfa : NFA
cs : List Char
eq : compile r = nfa
path : nfa.pathIn 0 (↑nfa.start) 0 cs
⊢ 0 < ↑(↑(done.pushRegex ⟨0, compile.proof_1⟩ r)).start
Tactic:
exact ge_pushRegex_start (rfl : NFA.done.pushRegex _ r = _)
State after:
no goals