theorem String.Slice.find?_bool_eq_some_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} : s.find? p = some pos ↔ ∃ (h : pos ≠ s.endPos), p (pos.get h) = true ∧ ∀ (pos' : s.Pos) (h' : pos' < pos), p (pos'.get ⋯) = false

theorem String.Slice.find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : s.find? p = some pos ↔ ∃ (h : pos ≠ s.endPos), p (pos.get h) ∧ ∀ (pos' : s.Pos) (h' : pos' < pos), ¬p (pos'.get ⋯)

theorem String.Slice.find?_bool_eq_some_iff_splits {p : Char → Bool} {s : Slice} {pos : s.Pos} : s.find? p = some pos ↔ ∃ (t : String), ∃ (c : Char), ∃ (u : String), pos.Splits t (singleton c ++ u) ∧ p c = true ∧ ∀ (d : Char), d ∈ t.toList → p d = false

theorem String.Slice.find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : s.find? p = some pos ↔ ∃ (t : String), ∃ (c : Char), ∃ (u : String), pos.Splits t (singleton c ++ u) ∧ p c ∧ ∀ (d : Char), d ∈ t.toList → ¬p d

@[simp]

theorem String.Slice.contains_bool_eq {p : Char → Bool} {s : Slice} : s.contains p = s.copy.toList.any p

@[simp]

theorem String.Slice.contains_prop_eq {p : Char → Prop} [DecidablePred p] {s : Slice} : s.contains p = s.copy.toList.any fun (b : Char) => decide (p b)

theorem String.Slice.Pos.find?_bool_eq_some_iff {p : Char → Bool} {s : Slice} {pos pos' : s.Pos} : pos.find? p = some pos' ↔ pos ≤ pos' ∧ (∃ (h : pos' ≠ s.endPos), p (pos'.get h) = true) ∧ ∀ (pos'' : s.Pos), pos ≤ pos'' → ∀ (h' : pos'' < pos'), p (pos''.get ⋯) = false

theorem String.Slice.Pos.find?_bool_eq_some_iff_splits {p : Char → Bool} {s : Slice} {pos : s.Pos} {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} : pos.find? p = some pos' ↔ ∃ (v : String), ∃ (c : Char), ∃ (w : String), pos'.Splits (t ++ v) (singleton c ++ w) ∧ p c = true ∧ ∀ (d : Char), d ∈ v.toList → p d = false

theorem String.Slice.Pos.find?_bool_eq_none_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} : pos.find? p = none ↔ ∀ (pos' : s.Pos), pos ≤ pos' → ∀ (h : pos' ≠ s.endPos), p (pos'.get h) = false

theorem String.Slice.Pos.find?_bool_eq_none_iff_of_splits {p : Char → Bool} {s : Slice} {pos : s.Pos} {t u : String} (hs : pos.Splits t u) : pos.find? p = none ↔ ∀ (c : Char), c ∈ u.toList → p c = false

theorem String.Slice.Pos.find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos pos' : s.Pos} : pos.find? p = some pos' ↔ pos ≤ pos' ∧ (∃ (h : pos' ≠ s.endPos), p (pos'.get h)) ∧ ∀ (pos'' : s.Pos), pos ≤ pos'' → ∀ (h' : pos'' < pos'), ¬p (pos''.get ⋯)

theorem String.Slice.Pos.find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} : pos.find? p = some pos' ↔ ∃ (v : String), ∃ (c : Char), ∃ (w : String), pos'.Splits (t ++ v) (singleton c ++ w) ∧ p c ∧ ∀ (d : Char), d ∈ v.toList → ¬p d

theorem String.Slice.Pos.find?_prop_eq_none_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} : pos.find? p = none ↔ ∀ (pos' : s.Pos), pos ≤ pos' → ∀ (h : pos' ≠ s.endPos), ¬p (pos'.get h)

theorem String.Slice.Pos.find?_prop_eq_none_iff_of_splits {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} {t u : String} (hs : pos.Splits t u) : pos.find? p = none ↔ ∀ (c : Char), c ∈ u.toList → ¬p c

theorem String.Pos.find?_prop_eq_find?_decide {p : Char → Prop} [DecidablePred p] {s : String} {pos : s.Pos} : pos.find? p = pos.find? fun (x : Char) => decide (p x)

theorem String.find?_prop_eq_find?_decide {p : Char → Prop} [DecidablePred p] {s : String} : s.find? p = s.find? fun (x : Char) => decide (p x)

theorem String.contains_prop_eq_contains_decide {p : Char → Prop} [DecidablePred p] {s : String} : s.contains p = s.contains fun (x : Char) => decide (p x)

theorem String.Pos.find?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos pos' : s.Pos} : pos.find? p = some pos' ↔ pos ≤ pos' ∧ (∃ (h : pos' ≠ s.endPos), p (pos'.get h) = true) ∧ ∀ (pos'' : s.Pos), pos ≤ pos'' → ∀ (h' : pos'' < pos'), p (pos''.get ⋯) = false

theorem String.Pos.find?_bool_eq_some_iff_splits {p : Char → Bool} {s : String} {pos : s.Pos} {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} : pos.find? p = some pos' ↔ ∃ (v : String), ∃ (c : Char), ∃ (w : String), pos'.Splits (t ++ v) (singleton c ++ w) ∧ p c = true ∧ ∀ (d : Char), d ∈ v.toList → p d = false

theorem String.Pos.find?_bool_eq_none_iff {p : Char → Bool} {s : String} {pos : s.Pos} : pos.find? p = none ↔ ∀ (pos' : s.Pos), pos ≤ pos' → ∀ (h : pos' ≠ s.endPos), p (pos'.get h) = false

theorem String.Pos.find?_bool_eq_none_iff_of_splits {p : Char → Bool} {s : String} {pos : s.Pos} {t u : String} (hs : pos.Splits t u) : pos.find? p = none ↔ ∀ (c : Char), c ∈ u.toList → p c = false

theorem String.Pos.find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : String} {pos pos' : s.Pos} : pos.find? p = some pos' ↔ pos ≤ pos' ∧ (∃ (h : pos' ≠ s.endPos), p (pos'.get h)) ∧ ∀ (pos'' : s.Pos), pos ≤ pos'' → ∀ (h' : pos'' < pos'), ¬p (pos''.get ⋯)

theorem String.Pos.find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s : String} {pos : s.Pos} {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} : pos.find? p = some pos' ↔ ∃ (v : String), ∃ (c : Char), ∃ (w : String), pos'.Splits (t ++ v) (singleton c ++ w) ∧ p c ∧ ∀ (d : Char), d ∈ v.toList → ¬p d

theorem String.Pos.find?_prop_eq_none_iff {p : Char → Prop} [DecidablePred p] {s : String} {pos : s.Pos} : pos.find? p = none ↔ ∀ (pos' : s.Pos), pos ≤ pos' → ∀ (h : pos' ≠ s.endPos), ¬p (pos'.get h)

theorem String.Pos.find?_prop_eq_none_iff_of_splits {p : Char → Prop} [DecidablePred p] {s : String} {pos : s.Pos} {t u : String} (hs : pos.Splits t u) : pos.find? p = none ↔ ∀ (c : Char), c ∈ u.toList → ¬p c

theorem String.find?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos : s.Pos} : s.find? p = some pos ↔ ∃ (h : pos ≠ s.endPos), p (pos.get h) = true ∧ ∀ (pos' : s.Pos) (h' : pos' < pos), p (pos'.get ⋯) = false

theorem String.find?_bool_eq_some_iff_splits {p : Char → Bool} {s : String} {pos : s.Pos} : s.find? p = some pos ↔ ∃ (t : String), ∃ (c : Char), ∃ (u : String), pos.Splits t (singleton c ++ u) ∧ p c = true ∧ ∀ (d : Char), d ∈ t.toList → p d = false

theorem String.find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : String} {pos : s.Pos} : s.find? p = some pos ↔ ∃ (h : pos ≠ s.endPos), p (pos.get h) ∧ ∀ (pos' : s.Pos) (h' : pos' < pos), ¬p (pos'.get ⋯)

theorem String.find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s : String} {pos : s.Pos} : s.find? p = some pos ↔ ∃ (t : String), ∃ (c : Char), ∃ (u : String), pos.Splits t (singleton c ++ u) ∧ p c ∧ ∀ (d : Char), d ∈ t.toList → ¬p d

@[simp]

theorem String.contains_bool_eq {p : Char → Bool} {s : String} : s.contains p = s.toList.any p

@[simp]

theorem String.contains_prop_eq {p : Char → Prop} [DecidablePred p] {s : String} : s.contains p = s.toList.any fun (b : Char) => decide (p b)