induction r generalizing nfa next with
| empty =>
  apply pushRegex.empty eq
  intro eq
  subst eq
  simp
| epsilon =>
  apply pushRegex.epsilon eq
  intro eq
  subst eq
  simp
| char c =>
  apply pushRegex.char eq
  intro eq
  subst eq
  simp
| classes c =>
  apply pushRegex.sparse eq
  intro eq
  subst eq
  simp
| group =>
  apply pushRegex.group eq
  intro nfa' nfa'' nfa''' property _ _ _ _ eq₃ eq
  rw [eq]
  simp
  rw [eq₃]
  simp
  apply Nat.le_of_lt (Nat.lt_trans nfa'.property nfa''.property)
| alternate r₁ r₂ =>
  apply pushRegex.alternate eq
  intro nfa₁ _ nfa₂ _ _ _ _ _ _ _ _ eq₅ eq
  rw [eq]
  simp
  rw [eq₅]
  simp [pushNode]
  exact Nat.le_of_lt (Nat.lt_trans nfa₁.property nfa₂.property)
| concat r₁ r₂ ih₁ =>
  apply pushRegex.concat eq
  intro nfa₂ nfa₁ _ _ eq₁ eq
  rw [eq]
  simp
  exact Nat.le_trans (Nat.le_of_lt nfa₂.property) (ih₁ eq₁.symm)
| star r =>
  apply pushRegex.star eq
  intro _ _ _ nfa' _ _ _ _ _ _ eq₄ eq
  rw [eq]
  simp
  rw [eq₄]
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next r = result
⊢ nfa.nodes.size ≤ ↑(↑result).start
no goals