theorem String.Slice.skipPrefix?_eq_forwardPatternSkipPrefix? {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] {s : Slice} : s.skipPrefix? pat = Pattern.ForwardPattern.skipPrefix? pat s

theorem String.Slice.startsWith_eq_forwardPatternStartsWith {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] {s : Slice} : s.startsWith pat = Pattern.ForwardPattern.startsWith pat s

theorem String.Slice.dropPrefix?_eq_map_skipPrefix? {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] {s : Slice} : s.dropPrefix? pat = Option.map s.sliceFrom (s.skipPrefix? pat)

theorem String.Slice.Pattern.Model.skipPrefix?_eq_some_iff {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} {pos : s.Pos} : s.skipPrefix? pat = some pos ↔ IsLongestMatch pat pos

theorem String.Slice.Pattern.Model.skipPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} : s.skipPrefix? pat = none ↔ ¬MatchesAt pat s.startPos

@[simp]

theorem String.Slice.isSome_skipPrefix? {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] [Pattern.LawfulForwardPattern pat] {s : Slice} : (s.skipPrefix? pat).isSome = s.startsWith pat

theorem String.Slice.Pattern.Model.startsWith_eq_false_iff {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} : s.startsWith pat = false ↔ ¬MatchesAt pat s.startPos

theorem String.Slice.Pattern.Model.startsWith_iff {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} : s.startsWith pat = true ↔ MatchesAt pat s.startPos

@[simp]

theorem String.Slice.skipPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] [Pattern.LawfulForwardPattern pat] {s : Slice} : s.skipPrefix? pat = none ↔ s.startsWith pat = false

@[simp]

theorem String.Slice.dropPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] [Pattern.LawfulForwardPattern pat] {s : Slice} : s.dropPrefix? pat = none ↔ s.startsWith pat = false

theorem String.Slice.Pattern.Model.eq_append_of_dropPrefix?_eq_some {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s res : Slice} (h : s.dropPrefix? pat = some res) : ∃ (t : String), PatternModel.Matches pat t ∧ s.copy = t ++ res.copy

theorem String.Slice.Pos.skip?_eq_map_skipPrefix? {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] {s : Slice} {pos : s.Pos} : pos.skip? pat = Option.map ofSliceFrom ((s.sliceFrom pos).skipPrefix? pat)

theorem String.Slice.Pattern.Model.Pos.skip?_eq_some_iff {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} {pos res : s.Pos} : pos.skip? pat = some res ↔ IsLongestMatchAt pat pos res

theorem String.Slice.Pattern.Model.Pos.skip?_eq_none_iff {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} {pos : s.Pos} : pos.skip? pat = none ↔ ¬MatchesAt pat pos

theorem String.Slice.Pattern.Model.Pos.skip?_eq_matchAt? {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} {pos : s.Pos} : pos.skip? pat = matchAt? pat pos

@[simp]

theorem String.Slice.skip?_startPos {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : s.startPos.skip? pat = s.skipPrefix? pat

theorem String.Slice.Pos.skip?_cast {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {pos : s.Pos} : (pos.cast hst).skip? pat = Option.map (fun (x : s.Pos) => x.cast hst) (pos.skip? pat)

theorem String.Slice.Pos.skip?_congr {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {pos : s.Pos} : pos.skip? pat = Option.map (fun (x : t.Pos) => x.cast ⋯) ((pos.cast hst).skip? pat)

theorem String.Slice.skipPrefix?_congr {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) : s.skipPrefix? pat = Option.map (fun (x : t.Pos) => x.cast ⋯) (t.skipPrefix? pat)

theorem String.Slice.startsWith_congr {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) : s.startsWith pat = t.startsWith pat

theorem String.Slice.dropPrefix?_congr {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) : Option.map copy (s.dropPrefix? pat) = Option.map copy (t.dropPrefix? pat)

theorem String.Slice.Pattern.Model.Pos.skipWhile_eq {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} {pos : s.Pos} : pos.skipWhile pat = (matchAt? pat pos).elim pos fun (x : s.Pos) => x.skipWhile pat

theorem String.Slice.Pos.skipWhile_cast {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {pos : s.Pos} : (pos.cast hst).skipWhile pat = (pos.skipWhile pat).cast hst

theorem String.Slice.Pos.skipWhile_congr {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {pos : s.Pos} : pos.skipWhile pat = ((pos.cast hst).skipWhile pat).cast ⋯

theorem String.Slice.Pattern.Model.Pos.skipWhile_eq_self {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} {pos : s.Pos} (h : ¬MatchesAt pat pos) : pos.skipWhile pat = pos

theorem String.Slice.Pattern.Model.Pos.skipWhile_eq_iff {ρ : Type} (pat : ρ) [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} (startPos endPos : s.Pos) : startPos.skipWhile pat = endPos ↔ IsLongestMatchAtChain pat startPos endPos ∧ (¬MatchesAt pat endPos ∨ IsLongestMatchAt pat endPos endPos)

theorem String.Slice.Pattern.Model.Pos.isLongestMatchAtChain_skipWhile {ρ : Type} (pat : ρ) [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} (pos : s.Pos) : IsLongestMatchAtChain pat pos (pos.skipWhile pat)

theorem String.Slice.Pattern.Model.Pos.not_matchesAt_or_isLongestMatchAt_skipWhile {ρ : Type} (pat : ρ) [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} (pos : s.Pos) : ¬MatchesAt pat (pos.skipWhile pat) ∨ IsLongestMatchAt pat (pos.skipWhile pat) (pos.skipWhile pat)

theorem String.Slice.Pattern.Model.Pos.not_matchesAt_skipWhile {ρ : Type} (pat : ρ) [PatternModel pat] [StrictPatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} (pos : s.Pos) : ¬MatchesAt pat (pos.skipWhile pat)

theorem String.Slice.Pattern.Model.Pos.skipWhile_eq_self_iff {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} {pos : s.Pos} : pos.skipWhile pat = pos ↔ ¬MatchesAt pat pos

theorem String.Slice.Pattern.Model.Pos.skipWhile_eq_self_iff_or {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} {pos : s.Pos} : pos.skipWhile pat = pos ↔ ¬MatchesAt pat pos ∨ IsLongestMatchAt pat pos pos

@[simp]

theorem String.Slice.Pos.le_skipWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} {pos : s.Pos} : pos ≤ pos.skipWhile pat

theorem String.Slice.Pattern.Model.Pos.le_skipWhile_of_isLongestMatchAtChain {ρ : Type} (pat : ρ) [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : IsLongestMatchAtChain pat startPos endPos) : endPos ≤ startPos.skipWhile pat

theorem String.Slice.skipPrefixWhile_eq_skipWhile_startPos {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] {s : Slice} : s.skipPrefixWhile pat = s.startPos.skipWhile pat

@[simp]

theorem String.Slice.cast_skipPrefixWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) : (s.skipPrefixWhile pat).cast hst = t.skipPrefixWhile pat

theorem String.Slice.Pattern.Model.skipPrefixWhile_eq_iff {ρ : Type} (pat : ρ) [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] (s : Slice) (res : s.Pos) : s.skipPrefixWhile pat = res ↔ IsLongestMatchAtChain pat s.startPos res ∧ (¬MatchesAt pat res ∨ IsLongestMatchAt pat res res)

theorem String.Slice.Pattern.Model.isLongestMatchAtChain_skipPrefixWhile {ρ : Type} (pat : ρ) [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] (s : Slice) : IsLongestMatchAtChain pat s.startPos (s.skipPrefixWhile pat)

theorem String.Slice.Pattern.Model.not_matchesAt_or_isLongestMatchAt_skipPrefixWhile {ρ : Type} (pat : ρ) [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] (s : Slice) : ¬MatchesAt pat (s.skipPrefixWhile pat) ∨ IsLongestMatchAt pat (s.skipPrefixWhile pat) (s.skipPrefixWhile pat)

theorem String.Slice.Pattern.Model.not_matchesAt_skipPrefixWhile {ρ : Type} (pat : ρ) [PatternModel pat] [StrictPatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] (s : Slice) : ¬MatchesAt pat (s.skipPrefixWhile pat)

theorem String.Slice.skipPrefixWhile_eq_startPos {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : s.startsWith pat = false → s.skipPrefixWhile pat = s.startPos

@[simp]

theorem String.Slice.skipPrefixWhile_eq_startPos_iff {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.Model.StrictPatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : s.skipPrefixWhile pat = s.startPos ↔ s.startsWith pat = false

theorem String.Slice.Pattern.Model.skipPrefixWhile_eq_startPos_iff_or {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} : s.skipPrefixWhile pat = s.startPos ↔ ¬MatchesAt pat s.startPos ∨ IsLongestMatch pat s.startPos

theorem String.Slice.dropWhile_eq_sliceFrom_skipPrefixWhile {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] {s : Slice} : s.dropWhile pat = s.sliceFrom (s.skipPrefixWhile pat)

theorem String.Slice.dropWhile_congr {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) : (s.dropWhile pat).copy = (t.dropWhile pat).copy

@[simp]

theorem String.Slice.startsWith_dropWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.Model.StrictPatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : (s.dropWhile pat).startsWith pat = false

theorem String.Slice.dropWhile_eq_self {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} (h : s.startsWith pat = false) : s.dropWhile pat = s

@[simp]

theorem String.Slice.dropWhile_eq_self_iff {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.Model.StrictPatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : s.dropWhile pat = s ↔ s.startsWith pat = false

theorem String.Slice.Pattern.Model.dropWhile_eq_self_iff_or {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} : s.dropWhile pat = s ↔ ¬MatchesAt pat s.startPos ∨ IsLongestMatch pat s.startPos

theorem String.Slice.takeWhile_eq_sliceTo_skipPrefixWhile {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] {s : Slice} : s.takeWhile pat = s.sliceTo (s.skipPrefixWhile pat)

@[simp]

theorem String.Slice.takeWhile_append_dropWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.LawfulForwardPattern pat] {s : Slice} : (s.takeWhile pat).copy ++ (s.dropWhile pat).copy = s.copy

theorem String.Slice.takeWhile_congr {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) : (s.takeWhile pat).copy = (t.takeWhile pat).copy

theorem String.Slice.isEmpty_takeWhile_eq_true {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} (h : s.startsWith pat = false) : (s.takeWhile pat).isEmpty = true

@[simp]

theorem String.Slice.isEmpty_takeWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.Model.StrictPatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : (s.takeWhile pat).isEmpty = !s.startsWith pat

theorem String.Slice.all_eq_skipPrefixWhile_beq {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] {s : Slice} : s.all pat = (s.skipPrefixWhile pat == s.endPos)

theorem String.Slice.Pattern.Model.all_eq_true_iff {ρ : Type} {pat : ρ} [PatternModel pat] [ForwardPattern pat] [LawfulForwardPatternModel pat] {s : Slice} : s.all pat = true ↔ IsLongestMatchAtChain pat s.startPos s.endPos

theorem String.Slice.all_congr {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) : s.all pat = t.all pat

@[simp]

theorem String.Slice.all_takeWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : (s.takeWhile pat).all pat = true

theorem String.Slice.isEmpty_takeWhile_iff_dropWhile_eq_self {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] {s : Slice} : (s.takeWhile pat).isEmpty = true ↔ s.dropWhile pat = s

theorem String.Slice.isEmpty_dropWhile_iff_takeWhile_eq_self {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] {s : Slice} : (s.dropWhile pat).isEmpty = true ↔ s.takeWhile pat = s

@[simp]

theorem String.Slice.takeWhile_eq_self_iff {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] {s : Slice} : s.takeWhile pat = s ↔ s.all pat = true

@[simp]

theorem String.Slice.isEmpty_dropWhile {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] {s : Slice} : (s.dropWhile pat).isEmpty = s.all pat

@[simp]

theorem String.Slice.dropWhile_dropWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : (s.dropWhile pat).dropWhile pat = s.dropWhile pat

theorem String.Slice.takeWhile_takeWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : (s.takeWhile pat).takeWhile pat = s.takeWhile pat

@[simp]

theorem String.Slice.isEmpty_takeWhile_dropWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : ((s.dropWhile pat).takeWhile pat).isEmpty = true

theorem String.Slice.isEmpty_dropWhile_takeWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : ((s.takeWhile pat).dropWhile pat).isEmpty = true

theorem String.Slice.skipSuffix?_eq_backwardPatternSkipSuffix? {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] {s : Slice} : s.skipSuffix? pat = Pattern.BackwardPattern.skipSuffix? pat s

theorem String.Slice.endsWith_eq_backwardPatternEndsWith {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] {s : Slice} : s.endsWith pat = Pattern.BackwardPattern.endsWith pat s

theorem String.Slice.dropSuffix?_eq_map_skipSuffix? {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] {s : Slice} : s.dropSuffix? pat = Option.map s.sliceTo (s.skipSuffix? pat)

theorem String.Slice.Pattern.Model.skipSuffix?_eq_some_iff {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} {pos : s.Pos} : s.skipSuffix? pat = some pos ↔ IsLongestRevMatch pat pos

theorem String.Slice.Pattern.Model.skipSuffix?_eq_none_iff {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} : s.skipSuffix? pat = none ↔ ¬RevMatchesAt pat s.endPos

@[simp]

theorem String.Slice.isSome_skipSuffix? {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] [Pattern.LawfulBackwardPattern pat] {s : Slice} : (s.skipSuffix? pat).isSome = s.endsWith pat

theorem String.Slice.Pattern.Model.endsWith_eq_false_iff {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} : s.endsWith pat = false ↔ ¬RevMatchesAt pat s.endPos

theorem String.Slice.Pattern.Model.endsWith_iff {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} : s.endsWith pat = true ↔ RevMatchesAt pat s.endPos

@[simp]

theorem String.Slice.skipSuffix?_eq_none_iff {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] [Pattern.LawfulBackwardPattern pat] {s : Slice} : s.skipSuffix? pat = none ↔ s.endsWith pat = false

@[simp]

theorem String.Slice.dropSuffix?_eq_none_iff {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] [Pattern.LawfulBackwardPattern pat] {s : Slice} : s.dropSuffix? pat = none ↔ s.endsWith pat = false

theorem String.Slice.Pattern.Model.eq_append_of_dropSuffix?_eq_some {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s res : Slice} (h : s.dropSuffix? pat = some res) : ∃ (t : String), PatternModel.Matches pat t ∧ s.copy = res.copy ++ t

theorem String.Slice.Pos.revSkip?_eq_map_skipSuffix? {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] {s : Slice} {pos : s.Pos} : pos.revSkip? pat = Option.map ofSliceTo ((s.sliceTo pos).skipSuffix? pat)

theorem String.Slice.Pattern.Model.Pos.revSkip?_eq_some_iff {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} {pos res : s.Pos} : pos.revSkip? pat = some res ↔ IsLongestRevMatchAt pat res pos

theorem String.Slice.Pattern.Model.Pos.revSkip?_eq_none_iff {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} {pos : s.Pos} : pos.revSkip? pat = none ↔ ¬RevMatchesAt pat pos

theorem String.Slice.Pattern.Model.Pos.revSkip?_eq_revMatchAt? {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} {pos : s.Pos} : pos.revSkip? pat = revMatchAt? pat pos

@[simp]

theorem String.Slice.revSkip?_endPos {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : s.endPos.revSkip? pat = s.skipSuffix? pat

theorem String.Slice.Pos.revSkip?_cast {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {pos : s.Pos} : (pos.cast hst).revSkip? pat = Option.map (fun (x : s.Pos) => x.cast hst) (pos.revSkip? pat)

theorem String.Slice.Pos.revSkip?_congr {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {pos : s.Pos} : pos.revSkip? pat = Option.map (fun (x : t.Pos) => x.cast ⋯) ((pos.cast hst).revSkip? pat)

theorem String.Slice.skipSuffix?_congr {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) : s.skipSuffix? pat = Option.map (fun (x : t.Pos) => x.cast ⋯) (t.skipSuffix? pat)

theorem String.Slice.endsWith_congr {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) : s.endsWith pat = t.endsWith pat

theorem String.Slice.dropSuffix?_congr {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) : Option.map copy (s.dropSuffix? pat) = Option.map copy (t.dropSuffix? pat)

theorem String.Slice.Pattern.Model.Pos.revSkipWhile_eq {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} {pos : s.Pos} : pos.revSkipWhile pat = (revMatchAt? pat pos).elim pos fun (x : s.Pos) => x.revSkipWhile pat

theorem String.Slice.Pos.revSkipWhile_cast {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {pos : s.Pos} : (pos.cast hst).revSkipWhile pat = (pos.revSkipWhile pat).cast hst

theorem String.Slice.Pos.revSkipWhile_congr {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) {pos : s.Pos} : pos.revSkipWhile pat = ((pos.cast hst).revSkipWhile pat).cast ⋯

theorem String.Slice.Pattern.Model.Pos.revSkipWhile_eq_self {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} {pos : s.Pos} (h : ¬RevMatchesAt pat pos) : pos.revSkipWhile pat = pos

theorem String.Slice.Pattern.Model.Pos.revSkipWhile_eq_iff {ρ : Type} (pat : ρ) [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} (startPos endPos : s.Pos) : endPos.revSkipWhile pat = startPos ↔ IsLongestRevMatchAtChain pat startPos endPos ∧ (¬RevMatchesAt pat startPos ∨ IsLongestRevMatchAt pat startPos startPos)

theorem String.Slice.Pattern.Model.Pos.isLongestRevMatchAtChain_revSkipWhile {ρ : Type} (pat : ρ) [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} (pos : s.Pos) : IsLongestRevMatchAtChain pat (pos.revSkipWhile pat) pos

theorem String.Slice.Pattern.Model.Pos.not_revMatchesAt_or_isLongestRevMatchAt_revSkipWhile {ρ : Type} (pat : ρ) [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} (pos : s.Pos) : ¬RevMatchesAt pat (pos.revSkipWhile pat) ∨ IsLongestRevMatchAt pat (pos.revSkipWhile pat) (pos.revSkipWhile pat)

theorem String.Slice.Pattern.Model.Pos.not_revMatchesAt_revSkipWhile {ρ : Type} (pat : ρ) [PatternModel pat] [StrictPatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} (pos : s.Pos) : ¬RevMatchesAt pat (pos.revSkipWhile pat)

theorem String.Slice.Pattern.Model.Pos.revSkipWhile_eq_self_iff {ρ : Type} {pat : ρ} [PatternModel pat] [StrictPatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} {pos : s.Pos} : pos.revSkipWhile pat = pos ↔ ¬RevMatchesAt pat pos

theorem String.Slice.Pattern.Model.Pos.revSkipWhile_eq_self_iff_or {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} {pos : s.Pos} : pos.revSkipWhile pat = pos ↔ ¬RevMatchesAt pat pos ∨ IsLongestRevMatchAt pat pos pos

@[simp]

theorem String.Slice.Pos.revSkipWhile_le {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} {pos : s.Pos} : pos.revSkipWhile pat ≤ pos

theorem String.Slice.Pattern.Model.Pos.revSkipWhile_le_of_isLongestRevMatchAtChain {ρ : Type} (pat : ρ) [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} {startPos endPos : s.Pos} (h : IsLongestRevMatchAtChain pat startPos endPos) : endPos.revSkipWhile pat ≤ startPos

theorem String.Slice.skipSuffixWhile_eq_revSkipWhile_endPos {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] {s : Slice} : s.skipSuffixWhile pat = s.endPos.revSkipWhile pat

@[simp]

theorem String.Slice.cast_skipSuffixWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) : (s.skipSuffixWhile pat).cast hst = t.skipSuffixWhile pat

theorem String.Slice.Pattern.Model.not_revMatchesAt_skipSuffixWhile {ρ : Type} (pat : ρ) [PatternModel pat] [StrictPatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] (s : Slice) : ¬RevMatchesAt pat (s.skipSuffixWhile pat)

theorem String.Slice.skipSuffixWhile_eq_endPos {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : s.endsWith pat = false → s.skipSuffixWhile pat = s.endPos

@[simp]

theorem String.Slice.skipSuffixWhile_eq_endPos_iff {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.Model.StrictPatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : s.skipSuffixWhile pat = s.endPos ↔ s.endsWith pat = false

theorem String.Slice.Pattern.Model.skipSuffixWhile_eq_iff {ρ : Type} (pat : ρ) [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] (s : Slice) (res : s.Pos) : s.skipSuffixWhile pat = res ↔ IsLongestRevMatchAtChain pat res s.endPos ∧ (¬RevMatchesAt pat res ∨ IsLongestRevMatchAt pat res res)

theorem String.Slice.Pattern.Model.isLongestRevMatchAtChain_skipSuffixWhile {ρ : Type} (pat : ρ) [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] (s : Slice) : IsLongestRevMatchAtChain pat (s.skipSuffixWhile pat) s.endPos

theorem String.Slice.Pattern.Model.not_revMatchesAt_or_isLongestRevMatchAt_skipSuffixWhile {ρ : Type} (pat : ρ) [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] (s : Slice) : ¬RevMatchesAt pat (s.skipSuffixWhile pat) ∨ IsLongestRevMatchAt pat (s.skipSuffixWhile pat) (s.skipSuffixWhile pat)

theorem String.Slice.Pattern.Model.skipSuffixWhile_eq_endPos_iff_or {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} : s.skipSuffixWhile pat = s.endPos ↔ ¬RevMatchesAt pat s.endPos ∨ IsLongestRevMatchAt pat s.endPos s.endPos

theorem String.Slice.dropEndWhile_eq_sliceTo_skipSuffixWhile {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] {s : Slice} : s.dropEndWhile pat = s.sliceTo (s.skipSuffixWhile pat)

theorem String.Slice.dropEndWhile_congr {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) : (s.dropEndWhile pat).copy = (t.dropEndWhile pat).copy

@[simp]

theorem String.Slice.endsWith_dropEndWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.Model.StrictPatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : (s.dropEndWhile pat).endsWith pat = false

theorem String.Slice.dropEndWhile_eq_self {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} (h : s.endsWith pat = false) : s.dropEndWhile pat = s

@[simp]

theorem String.Slice.dropEndWhile_eq_self_iff {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.Model.StrictPatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : s.dropEndWhile pat = s ↔ s.endsWith pat = false

theorem String.Slice.Pattern.Model.dropEndWhile_eq_self_iff_or {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} : s.dropEndWhile pat = s ↔ ¬RevMatchesAt pat s.endPos ∨ IsLongestRevMatchAt pat s.endPos s.endPos

theorem String.Slice.takeEndWhile_eq_sliceFrom_skipSuffixWhile {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] {s : Slice} : s.takeEndWhile pat = s.sliceFrom (s.skipSuffixWhile pat)

@[simp]

theorem String.Slice.dropEndWhile_append_takeEndWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.LawfulBackwardPattern pat] {s : Slice} : (s.dropEndWhile pat).copy ++ (s.takeEndWhile pat).copy = s.copy

theorem String.Slice.takeEndWhile_congr {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) : (s.takeEndWhile pat).copy = (t.takeEndWhile pat).copy

theorem String.Slice.isEmpty_takeEndWhile_eq_true {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} (h : s.endsWith pat = false) : (s.takeEndWhile pat).isEmpty = true

@[simp]

theorem String.Slice.isEmpty_takeEndWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.Model.StrictPatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : (s.takeEndWhile pat).isEmpty = !s.endsWith pat

theorem String.Slice.revAll_eq_skipSuffixWhile_beq {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] {s : Slice} : s.revAll pat = (s.skipSuffixWhile pat == s.startPos)

theorem String.Slice.Pattern.Model.revAll_eq_true_iff {ρ : Type} {pat : ρ} [PatternModel pat] [BackwardPattern pat] [LawfulBackwardPatternModel pat] {s : Slice} : s.revAll pat = true ↔ IsLongestRevMatchAtChain pat s.startPos s.endPos

theorem String.Slice.revAll_congr {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s t : Slice} (hst : s.copy = t.copy) : s.revAll pat = t.revAll pat

@[simp]

theorem String.Slice.revAll_takeEndWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : (s.takeEndWhile pat).revAll pat = true

theorem String.Slice.isEmpty_takeEndWhile_iff_dropEndWhile_eq_self {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] {s : Slice} : (s.takeEndWhile pat).isEmpty = true ↔ s.dropEndWhile pat = s

theorem String.Slice.isEmpty_dropEndWhile_iff_takeEndWhile_eq_self {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] {s : Slice} : (s.dropEndWhile pat).isEmpty = true ↔ s.takeEndWhile pat = s

@[simp]

theorem String.Slice.takeEndWhile_eq_self_iff {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] {s : Slice} : s.takeEndWhile pat = s ↔ s.revAll pat = true

@[simp]

theorem String.Slice.isEmpty_dropEndWhile {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] {s : Slice} : (s.dropEndWhile pat).isEmpty = s.revAll pat

@[simp]

theorem String.Slice.dropEndWhile_dropEndWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : (s.dropEndWhile pat).dropEndWhile pat = s.dropEndWhile pat

theorem String.Slice.takeEndWhile_takeEndWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : (s.takeEndWhile pat).takeEndWhile pat = s.takeEndWhile pat

@[simp]

theorem String.Slice.isEmpty_takeEndWhile_dropEndWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : ((s.dropEndWhile pat).takeEndWhile pat).isEmpty = true

theorem String.Slice.isEmpty_dropEndWhile_takeEndWhile {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : ((s.takeEndWhile pat).dropEndWhile pat).isEmpty = true

theorem String.skipPrefix?_eq_skipPrefix?_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} : s.skipPrefix? pat = Option.map Pos.ofToSlice (s.toSlice.skipPrefix? pat)

theorem String.skipPrefix?_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} : s.toSlice.skipPrefix? pat = Option.map Pos.toSlice (s.skipPrefix? pat)

theorem String.Slice.skipPrefix?_copy {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] [Pattern.Model.PatternModel pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : s.copy.skipPrefix? pat = Option.map Pos.copy (s.skipPrefix? pat)

theorem String.startsWith_eq_startsWith_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} : s.startsWith pat = s.toSlice.startsWith pat

@[simp]

theorem String.startsWith_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} : s.toSlice.startsWith pat = s.startsWith pat

@[simp]

theorem String.Slice.startsWith_copy {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] [Pattern.Model.PatternModel pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : s.copy.startsWith pat = s.startsWith pat

theorem String.dropPrefix?_eq_dropPrefix?_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} : s.dropPrefix? pat = s.toSlice.dropPrefix? pat

@[simp]

theorem String.dropPrefix?_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} : s.toSlice.dropPrefix? pat = s.dropPrefix? pat

@[simp]

theorem String.Slice.copy_dropPrefix?_copy {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] [Pattern.Model.PatternModel pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : Option.map copy (s.copy.dropPrefix? pat) = Option.map copy (s.dropPrefix? pat)

theorem String.Pos.skip?_eq_skip?_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} {pos : s.Pos} : pos.skip? pat = Option.map ofToSlice (pos.toSlice.skip? pat)

theorem String.Pos.skip?_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} {pos : s.Pos} : pos.toSlice.skip? pat = Option.map toSlice (pos.skip? pat)

theorem String.Slice.Pos.skip?_copy {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] [Pattern.Model.PatternModel pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} {pos : s.Pos} : pos.copy.skip? pat = Option.map copy (pos.skip? pat)

theorem String.Pos.skipWhile_eq_skipWhile_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} {pos : s.Pos} : pos.skipWhile pat = ofToSlice (pos.toSlice.skipWhile pat)

theorem String.Pos.skipWhile_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} {pos : s.Pos} : pos.toSlice.skipWhile pat = (pos.skipWhile pat).toSlice

theorem String.Slice.Pos.skipWhile_copy {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] [Pattern.Model.PatternModel pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} {pos : s.Pos} : pos.copy.skipWhile pat = (pos.skipWhile pat).copy

@[simp]

theorem String.Pos.le_skipWhile {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String} {pos : s.Pos} : pos ≤ pos.skipWhile pat

theorem String.skipPrefixWhile_eq_skipPrefixWhile_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} : s.skipPrefixWhile pat = Pos.ofToSlice (s.toSlice.skipPrefixWhile pat)

theorem String.skipPrefixWhile_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} : s.toSlice.skipPrefixWhile pat = (s.skipPrefixWhile pat).toSlice

theorem String.Slice.skipPrefixWhile_copy {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] [Pattern.Model.PatternModel pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : s.copy.skipPrefixWhile pat = (s.skipPrefixWhile pat).copy

theorem String.skipPrefixWhile_eq_startPos {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.ForwardPattern pat] [Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String} : s.startsWith pat = false → s.skipPrefixWhile pat = s.startPos

@[simp]

theorem String.skipPrefixWhile_eq_startPos_iff {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.Model.StrictPatternModel pat] [Slice.Pattern.ForwardPattern pat] [Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String} : s.skipPrefixWhile pat = s.startPos ↔ s.startsWith pat = false

theorem String.dropWhile_eq_dropWhile_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} : s.dropWhile pat = s.toSlice.dropWhile pat

@[simp]

theorem String.dropWhile_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} : s.toSlice.dropWhile pat = s.dropWhile pat

@[simp]

theorem String.Slice.dropWhile_copy {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] [Pattern.Model.PatternModel pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : (s.copy.dropWhile pat).copy = (s.dropWhile pat).copy

@[simp]

theorem String.startsWith_dropWhile {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.Model.StrictPatternModel pat] [Slice.Pattern.ForwardPattern pat] [Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String} : (s.dropWhile pat).startsWith pat = false

theorem String.dropWhile_eq_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.ForwardPattern pat] [Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String} (h : s.startsWith pat = false) : s.dropWhile pat = s.toSlice

@[simp]

theorem String.dropWhile_eq_toSlice_iff {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.Model.StrictPatternModel pat] [Slice.Pattern.ForwardPattern pat] [Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String} : s.dropWhile pat = s.toSlice ↔ s.startsWith pat = false

theorem String.takeWhile_eq_takeWhile_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} : s.takeWhile pat = s.toSlice.takeWhile pat

@[simp]

theorem String.takeWhile_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} : s.toSlice.takeWhile pat = s.takeWhile pat

@[simp]

theorem String.Slice.takeWhile_copy {ρ : Type} {pat : ρ} [Pattern.ForwardPattern pat] [Pattern.Model.PatternModel pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : (s.copy.takeWhile pat).copy = (s.takeWhile pat).copy

@[simp]

theorem String.takeWhile_append_dropWhile {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.ForwardPattern pat] [Slice.Pattern.LawfulForwardPattern pat] {s : String} : (s.takeWhile pat).copy ++ (s.dropWhile pat).copy = s

theorem String.isEmpty_takeWhile_eq_true {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.ForwardPattern pat] [Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String} (h : s.startsWith pat = false) : (s.takeWhile pat).isEmpty = true

@[simp]

theorem String.isEmpty_takeWhile {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.Model.StrictPatternModel pat] [Slice.Pattern.ForwardPattern pat] [Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String} : (s.takeWhile pat).isEmpty = !s.startsWith pat

theorem String.all_eq_all_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} : s.all pat = s.toSlice.all pat

@[simp]

theorem String.all_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} : s.toSlice.all pat = s.all pat

@[simp]

theorem String.Slice.all_copy {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.ForwardPattern pat] [Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : s.copy.all pat = s.all pat

@[simp]

theorem String.all_takeWhile {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.ForwardPattern pat] [Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String} : (s.takeWhile pat).all pat = true

@[simp]

theorem String.takeWhile_eq_toSlice_iff {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} : s.takeWhile pat = s.toSlice ↔ s.all pat = true

@[simp]

theorem String.isEmpty_dropWhile {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} : (s.dropWhile pat).isEmpty = s.all pat

@[simp]

theorem String.dropWhile_dropWhile {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.ForwardPattern pat] [Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String} : (s.dropWhile pat).dropWhile pat = s.dropWhile pat

theorem String.takeWhile_takeWhile {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.ForwardPattern pat] [Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : Slice} : (s.takeWhile pat).takeWhile pat = s.takeWhile pat

@[simp]

theorem String.isEmpty_takeWhile_dropWhile {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.ForwardPattern pat] [Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String} : ((s.dropWhile pat).takeWhile pat).isEmpty = true

theorem String.isEmpty_dropWhile_takeWhile {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.ForwardPattern pat] [Slice.Pattern.Model.LawfulForwardPatternModel pat] {s : String} : ((s.takeWhile pat).dropWhile pat).isEmpty = true

theorem String.skipSuffix?_eq_skipSuffix?_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} : s.skipSuffix? pat = Option.map Pos.ofToSlice (s.toSlice.skipSuffix? pat)

theorem String.skipSuffix?_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} : s.toSlice.skipSuffix? pat = Option.map Pos.toSlice (s.skipSuffix? pat)

theorem String.Slice.skipSuffix?_copy {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] [Pattern.Model.PatternModel pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : s.copy.skipSuffix? pat = Option.map Pos.copy (s.skipSuffix? pat)

theorem String.endsWith_eq_endsWith_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} : s.endsWith pat = s.toSlice.endsWith pat

@[simp]

theorem String.endsWith_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} : s.toSlice.endsWith pat = s.endsWith pat

@[simp]

theorem String.Slice.endsWith_copy {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] [Pattern.Model.PatternModel pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : s.copy.endsWith pat = s.endsWith pat

theorem String.dropSuffix?_eq_dropSuffix?_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} : s.dropSuffix? pat = s.toSlice.dropSuffix? pat

@[simp]

theorem String.dropSuffix?_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} : s.toSlice.dropSuffix? pat = s.dropSuffix? pat

@[simp]

theorem String.Slice.copy_dropSuffix?_copy {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] [Pattern.Model.PatternModel pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : Option.map copy (s.copy.dropSuffix? pat) = Option.map copy (s.dropSuffix? pat)

theorem String.revSkip?_eq_revSkip?_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} {pos : s.Pos} : pos.revSkip? pat = Option.map Pos.ofToSlice (pos.toSlice.revSkip? pat)

theorem String.revSkip?_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} {pos : s.Pos} : pos.toSlice.revSkip? pat = Option.map Pos.toSlice (pos.revSkip? pat)

theorem String.Slice.Pos.revSkip?_copy {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] [Pattern.Model.PatternModel pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} {pos : s.Pos} : pos.copy.revSkip? pat = Option.map copy (pos.revSkip? pat)

theorem String.Pos.revSkipWhile_eq_revSkipWhile_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} {pos : s.Pos} : pos.revSkipWhile pat = ofToSlice (pos.toSlice.revSkipWhile pat)

theorem String.Pos.revSkipWhile_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} {pos : s.Pos} : pos.toSlice.revSkipWhile pat = (pos.revSkipWhile pat).toSlice

theorem String.Slice.Pos.revSkipWhile_copy {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] [Pattern.Model.PatternModel pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} {pos : s.Pos} : pos.copy.revSkipWhile pat = (pos.revSkipWhile pat).copy

@[simp]

theorem String.Pos.revSkipWhile_le {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String} {pos : s.Pos} : pos.revSkipWhile pat ≤ pos

theorem String.skipSuffixWhile_eq_skipSuffixWhile_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} : s.skipSuffixWhile pat = Pos.ofToSlice (s.toSlice.skipSuffixWhile pat)

theorem String.skipSuffixWhile_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} : s.toSlice.skipSuffixWhile pat = (s.skipSuffixWhile pat).toSlice

theorem String.Slice.skipSuffixWhile_copy {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] [Pattern.Model.PatternModel pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : s.copy.skipSuffixWhile pat = (s.skipSuffixWhile pat).copy

theorem String.skipSuffixWhile_eq_endPos {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.BackwardPattern pat] [Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String} : s.endsWith pat = false → s.skipSuffixWhile pat = s.endPos

@[simp]

theorem String.skipSuffixWhile_eq_endPos_iff {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.Model.StrictPatternModel pat] [Slice.Pattern.BackwardPattern pat] [Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String} : s.skipSuffixWhile pat = s.endPos ↔ s.endsWith pat = false

theorem String.dropEndWhile_eq_dropEndWhile_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} : s.dropEndWhile pat = s.toSlice.dropEndWhile pat

@[simp]

theorem String.dropEndWhile_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} : s.toSlice.dropEndWhile pat = s.dropEndWhile pat

@[simp]

theorem String.Slice.dropEndWhile_copy {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] [Pattern.Model.PatternModel pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : (s.copy.dropEndWhile pat).copy = (s.dropEndWhile pat).copy

@[simp]

theorem String.endsWith_dropEndWhile {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.Model.StrictPatternModel pat] [Slice.Pattern.BackwardPattern pat] [Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String} : (s.dropEndWhile pat).endsWith pat = false

theorem String.dropEndWhile_eq_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.BackwardPattern pat] [Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String} (h : s.endsWith pat = false) : s.dropEndWhile pat = s.toSlice

@[simp]

theorem String.dropEndWhile_eq_toSlice_iff {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.Model.StrictPatternModel pat] [Slice.Pattern.BackwardPattern pat] [Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String} : s.dropEndWhile pat = s.toSlice ↔ s.endsWith pat = false

theorem String.takeEndWhile_eq_takeEndWhile_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} : s.takeEndWhile pat = s.toSlice.takeEndWhile pat

@[simp]

theorem String.takeEndWhile_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} : s.toSlice.takeEndWhile pat = s.takeEndWhile pat

@[simp]

theorem String.Slice.takeEndWhile_copy {ρ : Type} {pat : ρ} [Pattern.BackwardPattern pat] [Pattern.Model.PatternModel pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : (s.copy.takeEndWhile pat).copy = (s.takeEndWhile pat).copy

@[simp]

theorem String.dropEndWhile_append_takeEndWhile {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.BackwardPattern pat] [Slice.Pattern.LawfulBackwardPattern pat] {s : String} : (s.dropEndWhile pat).copy ++ (s.takeEndWhile pat).copy = s

theorem String.isEmpty_takeEndWhile_eq_true {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.BackwardPattern pat] [Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String} (h : s.endsWith pat = false) : (s.takeEndWhile pat).isEmpty = true

@[simp]

theorem String.isEmpty_takeEndWhile {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.Model.StrictPatternModel pat] [Slice.Pattern.BackwardPattern pat] [Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String} : (s.takeEndWhile pat).isEmpty = !s.endsWith pat

theorem String.revAll_eq_revAll_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} : s.revAll pat = s.toSlice.revAll pat

@[simp]

theorem String.revAll_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} : s.toSlice.revAll pat = s.revAll pat

@[simp]

theorem String.Slice.revAll_copy {ρ : Type} {pat : ρ} [Pattern.Model.PatternModel pat] [Pattern.BackwardPattern pat] [Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : s.copy.revAll pat = s.revAll pat

@[simp]

theorem String.revAll_takeEndWhile {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.BackwardPattern pat] [Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String} : (s.takeEndWhile pat).revAll pat = true

@[simp]

theorem String.takeEndWhile_eq_toSlice_iff {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} : s.takeEndWhile pat = s.toSlice ↔ s.revAll pat = true

@[simp]

theorem String.isEmpty_dropEndWhile {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} : (s.dropEndWhile pat).isEmpty = s.revAll pat

@[simp]

theorem String.dropEndWhile_dropEndWhile {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.BackwardPattern pat] [Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String} : (s.dropEndWhile pat).dropEndWhile pat = s.dropEndWhile pat

theorem String.takeEndWhile_takeEndWhile {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.BackwardPattern pat] [Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : Slice} : (s.takeEndWhile pat).takeEndWhile pat = s.takeEndWhile pat

@[simp]

theorem String.isEmpty_takeEndWhile_dropEndWhile {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.BackwardPattern pat] [Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String} : ((s.dropEndWhile pat).takeEndWhile pat).isEmpty = true

theorem String.isEmpty_dropEndWhile_takeEndWhile {ρ : Type} {pat : ρ} [Slice.Pattern.Model.PatternModel pat] [Slice.Pattern.BackwardPattern pat] [Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String} : ((s.takeEndWhile pat).dropEndWhile pat).isEmpty = true