Theorem: Regex.NFA.matches_of_path.concat (RegexCorrectness/NFA/Transition/Path/Equivalence/MatchOfPath.lean)

State before:
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
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
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₂
⊢ Expr.matches cs (r₁.concat r₂)
Tactic:
apply pushRegex.concat eq
State after:
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
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
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),
    nfa₂ = nfa.pushRegex next r₂ →
      nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁ → result = ⟨↑nfa₁, property⟩ → Expr.matches cs (r₁.concat r₂)

State before:
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
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
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),
    nfa₂ = nfa.pushRegex next r₂ →
      nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁ → result = ⟨↑nfa₁, property⟩ → Expr.matches cs (r₁.concat r₂)
Tactic:
intro nfa₂ nfa₁ property eq₂ eq₁ eq'
State after:
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
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
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⟩
⊢ Expr.matches cs (r₁.concat r₂)

State before:
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
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
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⟩
⊢ Expr.matches cs (r₁.concat r₂)
Tactic:
rw [eq'] at path
State after:
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
path : (↑⟨↑nfa₁, property⟩).pathToNext (↑next) nfa.nodes.size (↑(↑⟨↑nfa₁, property⟩).start) cs
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq' : result = ⟨↑nfa₁, property⟩
⊢ Expr.matches cs (r₁.concat r₂)

State before:
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
path : (↑⟨↑nfa₁, property⟩).pathToNext (↑next) nfa.nodes.size (↑(↑⟨↑nfa₁, property⟩).start) cs
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq' : result = ⟨↑nfa₁, property⟩
⊢ Expr.matches cs (r₁.concat r₂)
Tactic:
simp at path
State after:
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
path : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq' : result = ⟨↑nfa₁, property⟩
⊢ Expr.matches cs (r₁.concat r₂)

State before:
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
path : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq' : result = ⟨↑nfa₁, property⟩
⊢ Expr.matches cs (r₁.concat r₂)
Tactic:
have get (i : Nat) (_ : Array.size nfa.nodes ≤ i) (h₂ : i < nfa₂.val.nodes.size) :
  nfa₂.val[i] = nfa₁.val[i]'(Nat.lt_trans h₂ nfa₁.property) := by
  rw [pushRegex_get_lt eq₁.symm]
State after:
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
path : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
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]
⊢ Expr.matches cs (r₁.concat r₂)

State before:
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
path : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
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]
⊢ Expr.matches cs (r₁.concat r₂)
Tactic:
obtain ⟨i, cs₁, cs₂, eqs, path, step₂⟩ := path
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₂
⊢ Expr.matches cs (r₁.concat r₂)

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₂
⊢ Expr.matches cs (r₁.concat r₂)
Tactic:
have lti : i < nfa₂.val.nodes.size := by
  by_contra nlt
  apply Nat.lt_irrefl next
  have := eq_or_ge_of_step_pushRegex eq₁.symm (Nat.le_of_not_lt nlt) step₂.h₂ step₂.step
  cases this with
  | inl eq =>
    have := ge_pushRegex_start eq₂.symm
    calc
      _ < nfa.nodes.size := next.isLt
      _ ≤ nfa₂.val.start := this
      _ = next := eq.symm
  | inr ge =>
    calc
      _ < nfa.nodes.size := next.isLt
      _ < nfa₂.val.nodes.size := nfa₂.property
      _ ≤ next := ge
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
⊢ Expr.matches cs (r₁.concat r₂)

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
⊢ Expr.matches cs (r₁.concat r₂)
Tactic:
have ⟨cs₃, cs₄, eqs', path₁, path₂⟩ :=
  pathIn_split eq₁.symm lti (ge_pushRegex_start eq₁.symm) path
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₄
⊢ Expr.matches cs (r₁.concat r₂)

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₄
⊢ Expr.matches cs (r₁.concat r₂)
Tactic:
have m₁ := ih₁ eq₁.symm path₁
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₁
⊢ Expr.matches cs (r₁.concat r₂)

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
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₂)

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₁
path₂ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) (cs₄ ++ cs₂)
⊢ Expr.matches cs (r₁.concat r₂)
Tactic:
have m₂ := ih₂ eq₂.symm path₂
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₂)
m₂ : Expr.matches (cs₄ ++ cs₂) r₂
⊢ Expr.matches cs (r₁.concat r₂)

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₁
path₂ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) (cs₄ ++ cs₂)
m₂ : Expr.matches (cs₄ ++ cs₂) r₂
⊢ Expr.matches cs (r₁.concat r₂)
Tactic:
simp [eqs, eqs']
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₂)
m₂ : Expr.matches (cs₄ ++ cs₂) r₂
⊢ Expr.matches (cs₃ ++ (cs₄ ++ cs₂)) (r₁.concat r₂)

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₁
path₂ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) (cs₄ ++ cs₂)
m₂ : Expr.matches (cs₄ ++ cs₂) r₂
⊢ Expr.matches (cs₃ ++ (cs₄ ++ cs₂)) (r₁.concat r₂)
Tactic:
exact .concat _ _ _ _ m₁ m₂
State after:
no goals

State before:
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
path : (↑nfa₁).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₁).start) cs
eq₂ : nfa₂ = nfa.pushRegex next r₂
eq₁ : nfa₁ = (↑nfa₂).pushRegex (↑nfa₂).start r₁
eq' : result = ⟨↑nfa₁, property⟩
i : ℕ
x✝ : nfa.nodes.size ≤ i
h₂ : i < (↑nfa₂).nodes.size
⊢ (↑nfa₂)[i] = (↑nfa₁)[i]
Tactic:
rw [pushRegex_get_lt eq₁.symm]
State after:
no goals

State before:
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₂
⊢ i < (↑nfa₂).nodes.size
Tactic:
by_contra nlt
State after:
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₂
nlt : ¬i < (↑nfa₂).nodes.size
⊢ False

State before:
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₂
nlt : ¬i < (↑nfa₂).nodes.size
⊢ False
Tactic:
apply Nat.lt_irrefl next
State after:
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₂
nlt : ¬i < (↑nfa₂).nodes.size
⊢ ↑next < ↑next

State before:
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₂
nlt : ¬i < (↑nfa₂).nodes.size
⊢ ↑next < ↑next
Tactic:
have := eq_or_ge_of_step_pushRegex eq₁.symm (Nat.le_of_not_lt nlt) step₂.h₂ step₂.step
State after:
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₂
nlt : ¬i < (↑nfa₂).nodes.size
this : ↑next = ↑(↑nfa₂).start ∨ (↑nfa₂).nodes.size ≤ ↑next
⊢ ↑next < ↑next

State before:
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₂
nlt : ¬i < (↑nfa₂).nodes.size
this : ↑next = ↑(↑nfa₂).start ∨ (↑nfa₂).nodes.size ≤ ↑next
⊢ ↑next < ↑next
Tactic:
cases this with
| inl eq =>
  have := ge_pushRegex_start eq₂.symm
  calc
    _ < nfa.nodes.size := next.isLt
    _ ≤ nfa₂.val.start := this
    _ = next := eq.symm
| inr ge =>
  calc
    _ < nfa.nodes.size := next.isLt
    _ < nfa₂.val.nodes.size := nfa₂.property
    _ ≤ next := ge
State after:
no goals

State before:
case inl
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₂
nlt : ¬i < (↑nfa₂).nodes.size
eq : ↑next = ↑(↑nfa₂).start
⊢ ↑next < ↑next
Tactic:
have := ge_pushRegex_start eq₂.symm
State after:
case inl
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₂
nlt : ¬i < (↑nfa₂).nodes.size
eq : ↑next = ↑(↑nfa₂).start
this : nfa.nodes.size ≤ ↑(↑nfa₂).start
⊢ ↑next < ↑next

State before:
case inl
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₂
nlt : ¬i < (↑nfa₂).nodes.size
eq : ↑next = ↑(↑nfa₂).start
this : nfa.nodes.size ≤ ↑(↑nfa₂).start
⊢ ↑next < ↑next
Tactic:
calc
  _ < nfa.nodes.size := next.isLt
  _ ≤ nfa₂.val.start := this
  _ = next := eq.symm
State after:
no goals

State before:
case inr
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₂
nlt : ¬i < (↑nfa₂).nodes.size
ge : (↑nfa₂).nodes.size ≤ ↑next
⊢ ↑next < ↑next
Tactic:
calc
  _ < nfa.nodes.size := next.isLt
  _ < nfa₂.val.nodes.size := nfa₂.property
  _ ≤ next := ge
State after:
no goals

State before:
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₁
⊢ (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) (cs₄ ++ cs₂)
Tactic:
have step₂ : stepIn nfa₂ nfa.nodes.size i next cs₂ := by
  apply step₂.cast lti
  rw [get i step₂.h₁ lti]
State after:
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₁
step₂ : (↑nfa₂).stepIn nfa.nodes.size i (↑next) cs₂
⊢ (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) (cs₄ ++ cs₂)

State before:
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₁
step₂ : (↑nfa₂).stepIn nfa.nodes.size i (↑next) cs₂
⊢ (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) (cs₄ ++ cs₂)
Tactic:
refine ⟨i, cs₄, cs₂, rfl, ?_, step₂⟩
State after:
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₁
step₂ : (↑nfa₂).stepIn nfa.nodes.size i (↑next) cs₂
⊢ (↑nfa₂).pathIn nfa.nodes.size (↑(↑nfa₂).start) i cs₄

State before:
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₁
step₂ : (↑nfa₂).stepIn nfa.nodes.size i (↑next) cs₂
⊢ (↑nfa₂).pathIn nfa.nodes.size (↑(↑nfa₂).start) i cs₄
Tactic:
apply path₂.cast' nfa₂.val.start.isLt (Nat.le_of_lt nfa₁.property) get
State after:
no goals

State before:
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₁
⊢ (↑nfa₂).stepIn nfa.nodes.size i (↑next) cs₂
Tactic:
apply step₂.cast lti
State after:
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₁
⊢ (↑nfa₁)[i] = (↑nfa₂)[i]

State before:
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₁
⊢ (↑nfa₁)[i] = (↑nfa₂)[i]
Tactic:
rw [get i step₂.h₁ lti]
State after:
no goals