Theorem: Regex.NFA.matches_of_path.group
Proof state before:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa''').start) i' cs₁
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂
⊢ (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
Tactic:
have heq : i' = nfa.nodes.size ∧ cs₂ = [] := by
  cases Nat.eq_or_lt_of_le (le_of_pathIn_right path) with
  | inl eq =>
    have eqStart : nfa'''.val[nfa.nodes.size] = .save (2 * i + 1) next := by
      simp [eq₃]
      rw [pushNode_get_lt _ (Nat.lt_trans nfa'.property nfa''.property)]
      rw [pushRegex_get_lt eq₂.symm _ nfa'.property]
      simp [eq₁]
    rw [←eq] at step
    cases step with
    | charStep _ _ step =>
      rw [eqStart] at step
      simp [Node.charStep] at step
    | εStep _ _ eqs => exact ⟨eq.symm, rfl⟩
  | inr gt =>
    apply False.elim
    cases Nat.lt_or_ge i' nfa''.val.nodes.size with
    | inl lt =>
      have h₁ : nfa'.val.nodes.size ≤ i' := by
        simp [eq₁]
        exact gt
      have : i' < nfa'''.val.nodes.size := Nat.lt_trans lt nfa'''.property
      have : nfa'''.val[i'] = nfa''.val[i'] := by
        simp [eq₃]
        rw [pushNode_get_lt _ lt]
      have := eq_or_ge_of_step_pushRegex eq₂.symm h₁ lt (step.cast lt this).step
      cases this with
      | inl eq =>
        rw [eq₁] at eq
        simp at eq
        exact Nat.lt_irrefl _ (eq ▸ next.isLt)
      | inr ge => exact Nat.lt_irrefl _ (Nat.lt_of_lt_of_le (Nat.lt_trans next.isLt nfa'.property) ge)
    | inr ge =>
      have eqStart : nfa'''.val[nfa''.val.nodes.size]'nfa'''.property = .save (2 * i) nfa''.val.start := by
        simp [eq₃]
      have h₂ := step.h₂
      simp [eq₃] at h₂
      have : i' = nfa''.val.nodes.size := Nat.eq_of_le_of_lt_succ ge h₂
      have step := step.step
      simp [this, eqStart, Node.charStep, Node.εStep] at step
      have : nfa.nodes.size < nfa''.val.start := Nat.lt_of_lt_of_le nfa'.property (ge_pushRegex_start eq₂.symm)
      exact Nat.lt_irrefl _ (Nat.lt_trans (step ▸ this) next.isLt)
Proof state after:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Expr.group i r) = result
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }} {cs : List Char},
    nfa.pushRegex next r = result →
      (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs → Expr.matches cs r
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : result = ⟨↑nfa''', property⟩
i' : ℕ
cs₁ cs₂ : List Char
eqs : cs = cs₁ ++ cs₂
path : (↑nfa''').pathIn nfa.nodes.size (↑(↑nfa''').start) i' cs₁
step : (↑nfa''').stepIn nfa.nodes.size i' (↑next) cs₂
heq : i' = nfa.nodes.size ∧ cs₂ = []
⊢ (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs