@[simp]

theorem Regex.Strategy.materializeRegexGroups_empty : materializeRegexGroups Data.CaptureGroups.empty = fun (x : ℕ) => none

@[simp]

theorem Regex.Strategy.materializeRegexGroups_group {tag : ℕ} {first last : String.Pos} {groups : Data.CaptureGroups} : materializeRegexGroups (Data.CaptureGroups.group tag first last groups) = fun (tag' : ℕ) => if tag = tag' then some (first, last) else materializeRegexGroups groups tag'

@[simp]

theorem Regex.Strategy.materializeRegexGroups_concat {g₁ g₂ : Data.CaptureGroups} : materializeRegexGroups (g₁.concat g₂) = fun (tag : ℕ) => materializeRegexGroups g₂ tag <|> materializeRegexGroups g₁ tag

theorem Regex.Strategy.mem_tags_of_materializeRegexGroups_some {e : Data.Expr} {it it' : String.Iterator} {groups : Data.CaptureGroups} {tag : ℕ} (c : Data.Expr.Captures it it' groups e) (isSome : (materializeRegexGroups groups tag).isSome = true) : tag ∈ e.tags

@[simp]

theorem Regex.Strategy.materializeUpdatesAux_snoc {n : ℕ} {accum : Vector (Option String.Pos) n} {updates : List (ℕ × String.Pos)} {offset : ℕ} {pos : String.Pos} : materializeUpdatesAux n accum (updates ++ [(offset, pos)]) = (materializeUpdatesAux n accum updates).setIfInBounds offset (some pos)

theorem Regex.Strategy.materializeUpdatesAux_swap {n : ℕ} {accum : Vector (Option String.Pos) n} {updates : List (ℕ × String.Pos)} {offset₁ : ℕ} {pos₁ : String.Pos} {offset₂ : ℕ} {pos₂ : String.Pos} (ne : offset₁ ≠ offset₂) : materializeUpdatesAux n accum ((offset₁, pos₁) :: (offset₂, pos₂) :: updates) = materializeUpdatesAux n accum ((offset₂, pos₂) :: (offset₁, pos₁) :: updates)

theorem Regex.Strategy.materializeUpdatesAux_cons_of_not_in {n : ℕ} {accum : Vector (Option String.Pos) n} {updates : List (ℕ × String.Pos)} {offset : ℕ} {pos : String.Pos} (h : ∀ (offset' : ℕ) (pos' : String.Pos), (offset', pos') ∈ updates → offset ≠ offset') : materializeUpdatesAux n accum ((offset, pos) :: updates) = (materializeUpdatesAux n accum updates).setIfInBounds offset (some pos)

@[simp]

theorem Regex.Strategy.materializeUpdatesAux_nil {n : ℕ} {accum : Vector (Option String.Pos) n} : materializeUpdatesAux n accum [] = accum

theorem Regex.Strategy.materializeUpdatesAux_append {n : ℕ} {accum : Vector (Option String.Pos) n} {updates₁ updates₂ : List (ℕ × String.Pos)} : materializeUpdatesAux n accum (updates₁ ++ updates₂) = materializeUpdatesAux n (materializeUpdatesAux n accum updates₁) updates₂

theorem Regex.Strategy.materializeUpdatesAux_getElem {n : ℕ} {accum : Vector (Option String.Pos) n} {updates : List (ℕ × String.Pos)} {offset : ℕ} (h : offset < n) : (materializeUpdatesAux n accum updates)[offset] = ((materializeUpdatesAux n (Vector.replicate n none) updates)[offset] <|> accum[offset])

@[simp]

theorem Regex.Strategy.materializeUpdates_empty {n : ℕ} : materializeUpdates n [] = Vector.replicate n none

@[simp]

theorem Regex.Strategy.materializeUpdates_snoc {n : ℕ} {updates : List (ℕ × String.Pos)} {offset : ℕ} {pos : String.Pos} : materializeUpdates n (updates ++ [(offset, pos)]) = (materializeUpdates n updates).setIfInBounds offset (some pos)

theorem Regex.Strategy.materializeUpdates_append_getElem {n : ℕ} {updates₁ updates₂ : List (ℕ × String.Pos)} {offset : ℕ} (h : offset < n) : (materializeUpdates n (updates₁ ++ updates₂))[offset] = ((materializeUpdates n updates₂)[offset] <|> (materializeUpdates n updates₁)[offset])