@[simp]

theorem Regex.OptimizationInfo.findStart_toString {it : String.Iterator} {opt : OptimizationInfo} : (opt.findStart it).toString = it.toString

theorem Regex.OptimizationInfo.findStart_le_pos {it : String.Iterator} {opt : OptimizationInfo} : it.pos ≤ (opt.findStart it).pos

theorem Regex.OptimizationInfo.valid_findStart_of_valid {it : String.Iterator} {opt : OptimizationInfo} (v : it.Valid) : (opt.findStart it).Valid

theorem Regex.OptimizationInfo.findStart_completeness {it it' it'' : String.Iterator} {opt : OptimizationInfo} {groups : Data.CaptureGroups} {e : Data.Expr} (eq : opt = fromExpr e) (v : it.Valid) (eqs : it'.toString = it.toString) (ge : it.pos ≤ it'.pos) (lt : it'.pos < (opt.findStart it).pos) (c : Data.Expr.Captures it' it'' groups e) : False