theorem String.Slice.find?_char_eq_some_iff {c : Char} {s : Slice} {pos : s.Pos} : s.find? c = some pos ↔ ∃ (h : pos ≠ s.endPos), pos.get h = c ∧ ∀ (pos' : s.Pos) (h' : pos' < pos), pos'.get ⋯ ≠ c

@[simp]

theorem String.Slice.contains_char_eq {c : Char} {s : Slice} : s.contains c = decide (c ∈ s.copy.toList)

theorem String.Slice.find?_char_eq_some_iff_splits {c : Char} {s : Slice} {pos : s.Pos} : s.find? c = some pos ↔ ∃ (t : String), ∃ (u : String), pos.Splits t (singleton c ++ u) ∧ ¬c ∈ t.toList

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

theorem String.Slice.Pos.find?_char_eq_some_iff_splits {c : Char} {s : Slice} {pos : s.Pos} {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} : pos.find? c = some pos' ↔ ∃ (v : String), ∃ (w : String), pos'.Splits (t ++ v) (singleton c ++ w) ∧ ¬c ∈ v.toList

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

theorem String.Slice.Pos.find?_char_eq_none_iff_not_mem_of_splits {c : Char} {s : Slice} {pos : s.Pos} {t u : String} (hs : pos.Splits t u) : pos.find? c = none ↔ ¬c ∈ u.toList

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

theorem String.Pos.find?_char_eq_some_iff_splits {c : Char} {s : String} {pos : s.Pos} {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} : pos.find? c = some pos' ↔ ∃ (v : String), ∃ (w : String), pos'.Splits (t ++ v) (singleton c ++ w) ∧ ¬c ∈ v.toList

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

theorem String.Pos.find?_char_eq_none_iff_not_mem_of_splits {c : Char} {s : String} {pos : s.Pos} {t u : String} (hs : pos.Splits t u) : pos.find? c = none ↔ ¬c ∈ u.toList

theorem String.Pos.find?_char_eq_find?_beq {c : Char} {s : String} {pos : s.Pos} : pos.find? c = pos.find? fun (x : Char) => x == c

theorem String.find?_char_eq_find?_beq {c : Char} {s : String} : s.find? c = s.find? fun (x : Char) => x == c

theorem String.contains_char_eq_contains_beq {c : Char} {s : String} : s.contains c = s.contains fun (x : Char) => x == c

theorem String.find?_char_eq_some_iff {c : Char} {s : String} {pos : s.Pos} : s.find? c = some pos ↔ ∃ (h : pos ≠ s.endPos), pos.get h = c ∧ ∀ (pos' : s.Pos) (h' : pos' < pos), pos'.get ⋯ ≠ c

theorem String.find?_char_eq_some_iff_splits {c : Char} {s : String} {pos : s.Pos} : s.find? c = some pos ↔ ∃ (t : String), ∃ (u : String), pos.Splits t (singleton c ++ u) ∧ ¬c ∈ t.toList

@[simp]

theorem String.contains_char_eq {c : Char} {s : String} : s.contains c = decide (c ∈ s.toList)