Theorem: Regex.NFA.matches_of_path.concat
Proof state before:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.concat 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₁
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' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq' : result = ⟨↑nfa₁, property⟩
get : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑nfa₁)[i]
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₂
lti : i < (↑nfa₂).nodes.size
cs₃ cs₄ : List Char
eqs' : cs₁ = cs₃ ++ cs₄
path₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) (↑nfa₂).nodes.size (↑(↑nfa₁).start) cs₃
path₂ : (↑nfa₁).pathIn nfa.nodes.size (↑(↑nfa₂).start) i cs₄
m₁ : Expr.matches cs₃ r₁
⊢ Expr.matches cs (r₁.concat r₂)
Tactic:
have path₂ : pathToNext nfa₂ next nfa.nodes.size nfa₂.val.start.val (cs₄ ++ cs₂) := by
  have step₂ : stepIn nfa₂ nfa.nodes.size i next cs₂ := by
    apply step₂.cast lti
    rw [get i step₂.h₁ lti]
  refine ⟨i, cs₄, cs₂, rfl, ?_, step₂⟩
  apply path₂.cast' nfa₂.val.start.isLt (Nat.le_of_lt nfa₁.property) get
Proof state after:
case intro.intro.intro.intro.intro
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next (r₁.concat 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₁
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' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa₁).nodes.size
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq' : result = ⟨↑nfa₁, property⟩
get : ∀ (i : ℕ), nfa.nodes.size ≤ i → ∀ (h₂ : i < (↑nfa₂).nodes.size), (↑nfa₂)[i] = (↑nfa₁)[i]
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₂
lti : i < (↑nfa₂).nodes.size
cs₃ cs₄ : List Char
eqs' : cs₁ = cs₃ ++ cs₄
path₁ : (↑nfa₁).pathToNext (↑(↑nfa₂).start) (↑nfa₂).nodes.size (↑(↑nfa₁).start) cs₃
path₂✝ : (↑nfa₁).pathIn nfa.nodes.size (↑(↑nfa₂).start) i cs₄
m₁ : Expr.matches cs₃ r₁
path₂ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) (cs₄ ++ cs₂)
⊢ Expr.matches cs (r₁.concat r₂)