theorem String.Slice.Pattern.Model.find?_eq_some_iff {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] [∀ (s : Slice), Std.LawfulIteratorLoop (σ s) Id Id] [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} {pos : s.Pos} : s.find? pat = some pos ↔ MatchesAt pat pos ∧ ∀ (pos' : s.Pos), pos' < pos → ¬MatchesAt pat pos'

theorem String.Slice.Pattern.Model.find?_eq_none_iff {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] [∀ (s : Slice), Std.LawfulIteratorLoop (σ s) Id Id] [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} : s.find? pat = none ↔ ∀ (pos : s.Pos), ¬MatchesAt pat pos

@[simp]

theorem String.Slice.isSome_find? {ρ : Type} (pat : ρ) {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] [∀ (s : Slice), Std.LawfulIteratorLoop (σ s) Id Id] [Pattern.ToForwardSearcher pat σ] {s : Slice} : (s.find? pat).isSome = s.contains pat

@[simp]

theorem String.Slice.find?_eq_none_iff {ρ : Type} (pat : ρ) {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] [∀ (s : Slice), Std.LawfulIteratorLoop (σ s) Id Id] [Pattern.ToForwardSearcher pat σ] {s : Slice} : s.find? pat = none ↔ s.contains pat = false

theorem String.Slice.Pattern.Model.contains_eq_false_iff {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] [∀ (s : Slice), Std.LawfulIteratorLoop (σ s) Id Id] [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} : s.contains pat = false ↔ ∀ (pos : s.Pos), ¬MatchesAt pat pos

theorem String.Slice.Pattern.Model.contains_eq_true_iff {ρ : Type} (pat : ρ) [PatternModel pat] {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] [∀ (s : Slice), Std.LawfulIteratorLoop (σ s) Id Id] [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} : s.contains pat = true ↔ ∃ (pos : s.Pos), MatchesAt pat pos

theorem String.Slice.Pos.find?_eq_find?_sliceFrom {ρ : Type} {pat : ρ} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Pattern.SearchStep s)] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] [Pattern.ToForwardSearcher pat σ] {s : Slice} {p : s.Pos} : p.find? pat = Option.map ofSliceFrom ((s.sliceFrom p).find? pat)

theorem String.Slice.Pattern.Model.posFind?_eq_some_iff {ρ : Type} {pat : ρ} [PatternModel pat] {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] [∀ (s : Slice), Std.LawfulIteratorLoop (σ s) Id Id] [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} {pos pos' : s.Pos} : pos.find? pat = some pos' ↔ pos ≤ pos' ∧ MatchesAt pat pos' ∧ ∀ (pos'' : s.Pos), pos ≤ pos'' → pos'' < pos' → ¬MatchesAt pat pos''

theorem String.Slice.Pattern.Model.posFind?_eq_none_iff {ρ : Type} {pat : ρ} [PatternModel pat] {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (SearchStep s)] [∀ (s : Slice), Std.Iterators.Finite (σ s) Id] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] [∀ (s : Slice), Std.LawfulIteratorLoop (σ s) Id Id] [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} {pos : s.Pos} : pos.find? pat = none ↔ ∀ (pos' : s.Pos), pos ≤ pos' → ¬MatchesAt pat pos'

theorem String.Pos.find?_eq_find?_toSlice {ρ : Type} {pat : ρ} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] [Slice.Pattern.ToForwardSearcher pat σ] {s : String} {p : s.Pos} : p.find? pat = Option.map ofToSlice (p.toSlice.find? pat)

theorem String.find?_eq_find?_toSlice {ρ : Type} {pat : ρ} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] [Slice.Pattern.ToForwardSearcher pat σ] {s : String} : s.find? pat = Option.map Pos.ofToSlice (s.toSlice.find? pat)

theorem String.contains_eq_contains_toSlice {ρ : Type} {pat : ρ} {σ : Slice → Type} [(s : Slice) → Std.Iterator (σ s) Id (Slice.Pattern.SearchStep s)] [(s : Slice) → Std.IteratorLoop (σ s) Id Id] [Slice.Pattern.ToForwardSearcher pat σ] {s : String} : s.contains pat = s.toSlice.contains pat