theorem String.Slice.skipPrefix?_bool_eq_some_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} : s.skipPrefix? p = some pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h) = true

theorem String.Slice.startsWith_bool_iff_get {p : Char → Bool} {s : Slice} : s.startsWith p = true ↔ ∃ (h : s.startPos ≠ s.endPos), p (s.startPos.get h) = true

theorem String.Slice.startsWith_bool_eq_false_iff_get {p : Char → Bool} {s : Slice} : s.startsWith p = false ↔ ∀ (h : s.startPos ≠ s.endPos), p (s.startPos.get h) = false

theorem String.Slice.startsWith_bool_eq_head? {p : Char → Bool} {s : Slice} : s.startsWith p = Option.any p s.copy.toList.head?

theorem String.Slice.eq_append_of_dropPrefix?_bool_eq_some {p : Char → Bool} {s res : Slice} (h : s.dropPrefix? p = some res) : ∃ (c : Char), s.copy = singleton c ++ res.copy ∧ p c = true

theorem String.Slice.skipPrefix?_prop_eq_some_iff {P : Char → Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} : s.skipPrefix? P = some pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ P (s.startPos.get h)

theorem String.Slice.startsWith_prop_iff_get {P : Char → Prop} [DecidablePred P] {s : Slice} : s.startsWith P = true ↔ ∃ (h : s.startPos ≠ s.endPos), P (s.startPos.get h)

theorem String.Slice.startsWith_prop_eq_false_iff_get {P : Char → Prop} [DecidablePred P] {s : Slice} : s.startsWith P = false ↔ ∀ (h : s.startPos ≠ s.endPos), ¬P (s.startPos.get h)

theorem String.Slice.startsWith_prop_eq_head? {P : Char → Prop} [DecidablePred P] {s : Slice} : s.startsWith P = Option.any (fun (x : Char) => decide (P x)) s.copy.toList.head?

theorem String.Slice.eq_append_of_dropPrefix?_prop_eq_some {P : Char → Prop} [DecidablePred P] {s res : Slice} (h : s.dropPrefix? P = some res) : ∃ (c : Char), s.copy = singleton c ++ res.copy ∧ P c

theorem String.Slice.skipSuffix?_bool_eq_some_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} : s.skipSuffix? p = some pos ↔ ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get ⋯) = true

theorem String.Slice.endsWith_bool_iff_get {p : Char → Bool} {s : Slice} : s.endsWith p = true ↔ ∃ (h : s.endPos ≠ s.startPos), p ((s.endPos.prev h).get ⋯) = true

theorem String.Slice.endsWith_bool_eq_false_iff_get {p : Char → Bool} {s : Slice} : s.endsWith p = false ↔ ∀ (h : s.endPos ≠ s.startPos), p ((s.endPos.prev h).get ⋯) = false

theorem String.Slice.endsWith_bool_eq_getLast? {p : Char → Bool} {s : Slice} : s.endsWith p = Option.any p s.copy.toList.getLast?

theorem String.Slice.eq_append_of_dropSuffix?_bool_eq_some {p : Char → Bool} {s res : Slice} (h : s.dropSuffix? p = some res) : ∃ (c : Char), s.copy = res.copy ++ singleton c ∧ p c = true

theorem String.Slice.skipSuffix?_prop_eq_some_iff {P : Char → Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} : s.skipSuffix? P = some pos ↔ ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ P ((s.endPos.prev h).get ⋯)

theorem String.Slice.endsWith_prop_iff_get {P : Char → Prop} [DecidablePred P] {s : Slice} : s.endsWith P = true ↔ ∃ (h : s.endPos ≠ s.startPos), P ((s.endPos.prev h).get ⋯)

theorem String.Slice.endsWith_prop_eq_false_iff_get {P : Char → Prop} [DecidablePred P] {s : Slice} : s.endsWith P = false ↔ ∀ (h : s.endPos ≠ s.startPos), ¬P ((s.endPos.prev h).get ⋯)

theorem String.Slice.endsWith_prop_eq_getLast? {P : Char → Prop} [DecidablePred P] {s : Slice} : s.endsWith P = Option.any (fun (x : Char) => decide (P x)) s.copy.toList.getLast?

theorem String.Slice.eq_append_of_dropSuffix?_prop_eq_some {P : Char → Prop} [DecidablePred P] {s res : Slice} (h : s.dropSuffix? P = some res) : ∃ (c : Char), s.copy = res.copy ++ singleton c ∧ P c

theorem String.skipPrefix?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos : s.Pos} : s.skipPrefix? p = some pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h) = true

theorem String.startsWith_bool_iff_get {p : Char → Bool} {s : String} : s.startsWith p = true ↔ ∃ (h : s.startPos ≠ s.endPos), p (s.startPos.get h) = true

theorem String.startsWith_bool_eq_false_iff_get {p : Char → Bool} {s : String} : s.startsWith p = false ↔ ∀ (h : s.startPos ≠ s.endPos), p (s.startPos.get h) = false

theorem String.startsWith_bool_eq_head? {p : Char → Bool} {s : String} : s.startsWith p = Option.any p s.toList.head?

theorem String.eq_append_of_dropPrefix?_bool_eq_some {p : Char → Bool} {s : String} {res : Slice} (h : s.dropPrefix? p = some res) : ∃ (c : Char), s = singleton c ++ res.copy ∧ p c = true

theorem String.skipPrefix?_prop_eq_some_iff {P : Char → Prop} [DecidablePred P] {s : String} {pos : s.Pos} : s.skipPrefix? P = some pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ P (s.startPos.get h)

theorem String.startsWith_prop_iff_get {P : Char → Prop} [DecidablePred P] {s : String} : s.startsWith P = true ↔ ∃ (h : s.startPos ≠ s.endPos), P (s.startPos.get h)

theorem String.startsWith_prop_eq_false_iff_get {P : Char → Prop} [DecidablePred P] {s : String} : s.startsWith P = false ↔ ∀ (h : s.startPos ≠ s.endPos), ¬P (s.startPos.get h)

theorem String.startsWith_prop_eq_head? {P : Char → Prop} [DecidablePred P] {s : String} : s.startsWith P = Option.any (fun (x : Char) => decide (P x)) s.toList.head?

theorem String.eq_append_of_dropPrefix?_prop_eq_some {P : Char → Prop} [DecidablePred P] {s : String} {res : Slice} (h : s.dropPrefix? P = some res) : ∃ (c : Char), s = singleton c ++ res.copy ∧ P c

theorem String.skipSuffix?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos : s.Pos} : s.skipSuffix? p = some pos ↔ ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get ⋯) = true

theorem String.endsWith_bool_iff_get {p : Char → Bool} {s : String} : s.endsWith p = true ↔ ∃ (h : s.endPos ≠ s.startPos), p ((s.endPos.prev h).get ⋯) = true

theorem String.endsWith_bool_eq_false_iff_get {p : Char → Bool} {s : String} : s.endsWith p = false ↔ ∀ (h : s.endPos ≠ s.startPos), p ((s.endPos.prev h).get ⋯) = false

theorem String.endsWith_bool_eq_getLast? {p : Char → Bool} {s : String} : s.endsWith p = Option.any p s.toList.getLast?

theorem String.eq_append_of_dropSuffix?_bool_eq_some {p : Char → Bool} {s : String} {res : Slice} (h : s.dropSuffix? p = some res) : ∃ (c : Char), s = res.copy ++ singleton c ∧ p c = true

theorem String.skipSuffix?_prop_eq_some_iff {P : Char → Prop} [DecidablePred P] {s : String} {pos : s.Pos} : s.skipSuffix? P = some pos ↔ ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ P ((s.endPos.prev h).get ⋯)

theorem String.endsWith_prop_iff_get {P : Char → Prop} [DecidablePred P] {s : String} : s.endsWith P = true ↔ ∃ (h : s.endPos ≠ s.startPos), P ((s.endPos.prev h).get ⋯)

theorem String.endsWith_prop_eq_false_iff_get {P : Char → Prop} [DecidablePred P] {s : String} : s.endsWith P = false ↔ ∀ (h : s.endPos ≠ s.startPos), ¬P ((s.endPos.prev h).get ⋯)

theorem String.endsWith_prop_eq_getLast? {P : Char → Prop} [DecidablePred P] {s : String} : s.endsWith P = Option.any (fun (x : Char) => decide (P x)) s.toList.getLast?

theorem String.eq_append_of_dropSuffix?_prop_eq_some {P : Char → Prop} [DecidablePred P] {s : String} {res : Slice} (h : s.dropSuffix? P = some res) : ∃ (c : Char), s = res.copy ++ singleton c ∧ P c