cases ih₁ with
| inl eq =>
  simp [eq]
  exact ge_pushRegex_start eq₂.symm
| inr ge => exact Nat.le_trans (Nat.le_of_lt nfa₂.property) ge
case inr.h
i j : ℕ
r₁ r₂ : Data.Expr
ih₁✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₁ = result →
      nfa.nodes.size ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
ih₂ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r₂ = result →
      nfa.nodes.size ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (r₁.concat r₂) = result
h₁ : nfa.nodes.size ≤ i
h₂✝ : i < (↑result).nodes.size
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₂ : ∀ (h : i < (↑nfa₂).nodes.size), (↑result)[i] = (↑nfa₂)[i]
ge : i ≥ (↑nfa₂).nodes.size
h₂ : i < (↑nfa₁).nodes.size
step : (∃ c, j ∈ (↑nfa₁)[i].charStep c) ∨ j ∈ (↑nfa₁)[i].εStep
ih₁ : j = ↑(↑nfa₂).start ∨ (↑nfa₂).nodes.size ≤ j
⊢ nfa.nodes.size ≤ j
no goals