theorem Regex.Syntax.Parser.Ast.subset_repeatConcat_go_tags (e accum : Data.Expr) (n : ℕ) (h : e.tags ⊆ accum.tags) : e.tags ⊆ (repeatConcat.go e accum n).tags

theorem Regex.Syntax.Parser.Ast.repeatConcat_go_tags_subset (e accum : Data.Expr) (n : ℕ) : (repeatConcat.go e accum n).tags ⊆ accum.tags ∪ e.tags

theorem Regex.Syntax.Parser.Ast.repeatConcat_tags (e : Data.Expr) (n : ℕ) : (repeatConcat e n).tags = e.tags

theorem Regex.Syntax.Parser.Ast.applyRepetitions_tags (min : ℕ) (max : Option ℕ) (greedy : Bool) (e : Data.Expr) : (applyRepetitions min max greedy e).tags ⊆ e.tags

theorem Regex.Syntax.Parser.Ast.toRegexAux_tags {index index' : ℕ} {ast : Ast} {e : Data.Expr} (h : toRegexAux index ast = (index', e)) : index ≤ index' ∧ e.tags ⊆ Finset.Ico index index'

theorem Regex.Syntax.Parser.Ast.repeatConcat_go_disjoint (e accum : Data.Expr) (n : ℕ) (h : e.Disjoint) (haccum : accum.Disjoint) : (repeatConcat.go e accum n).Disjoint

theorem Regex.Syntax.Parser.Ast.repeatConcat_disjoint (e : Data.Expr) (n : ℕ) (h : e.Disjoint) : (repeatConcat e n).Disjoint

theorem Regex.Syntax.Parser.Ast.applyRepetitions_disjoint (min : ℕ) (max : Option ℕ) (greedy : Bool) (e : Data.Expr) (h : e.Disjoint) : (applyRepetitions min max greedy e).Disjoint

theorem Regex.Syntax.Parser.Ast.toRegexAux_disjoint (index : ℕ) (ast : Ast) : (toRegexAux index ast).2.Disjoint

theorem Regex.Syntax.Parser.Ast.toRegex_disjoint (ast : Ast) : ast.toRegex.Disjoint

theorem Regex.Syntax.Parser.Ast.toRegexAux_group_of_group {ast : Ast} : (toRegexAux 0 ast.group).2 = Data.Expr.group 0 (toRegexAux 1 ast).2

theorem Regex.Syntax.Parser.Ast.toRegex_group_of_group (ast : Ast) : ∃ (e : Data.Expr), ast.group.toRegex = Data.Expr.group 0 e