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.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.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.startsWith_eq_startsWith_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.ForwardPattern pat] {s : String} : s.startsWith pat = s.toSlice.startsWith pat

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

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.endsWith_eq_endsWith_toSlice {ρ : Type} {pat : ρ} [Slice.Pattern.BackwardPattern pat] {s : String} : s.endsWith pat = s.toSlice.endsWith pat

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