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

@[simp]

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

@[simp]

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

theorem String.Slice.Pos.apply_skipWhile_bool_eq_false {p : Char → Bool} {s : Slice} {pos : s.Pos} {h : pos.skipWhile p ≠ s.endPos} : p ((pos.skipWhile p).get h) = false

theorem String.Slice.Pos.skipWhile_bool_eq_self_iff_get {p : Char → Bool} {s : Slice} {pos : s.Pos} : pos.skipWhile p = pos ↔ ∀ (h : pos ≠ s.endPos), p (pos.get h) = false

theorem String.Slice.Pos.apply_eq_true_of_lt_skipWhile_bool {p : Char → Bool} {s : Slice} {pos pos' : s.Pos} (h₁ : pos ≤ pos') (h₂ : pos' < pos.skipWhile p) : p (pos'.get ⋯) = true

theorem String.Slice.apply_skipPrefixWhile_bool_eq_false {p : Char → Bool} {s : Slice} {h : s.skipPrefixWhile p ≠ s.endPos} : p ((s.skipPrefixWhile p).get h) = false

theorem String.Slice.apply_eq_true_of_lt_skipPrefixWhile_bool {p : Char → Bool} {s : Slice} {pos : s.Pos} (h : pos < s.skipPrefixWhile p) : p (pos.get ⋯) = true

@[simp]

theorem String.Slice.all_bool_eq {p : Char → Bool} {s : Slice} : s.all p = s.copy.toList.all p

@[simp]

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

@[simp]

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

theorem String.Slice.Pos.apply_skipWhile_prop {P : Char → Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} {h : pos.skipWhile P ≠ s.endPos} : ¬P ((pos.skipWhile P).get h)

theorem String.Slice.Pos.skipWhile_prop_eq_self_iff_get {P : Char → Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} : pos.skipWhile P = pos ↔ ∀ (h : pos ≠ s.endPos), ¬P (pos.get h)

theorem String.Slice.Pos.apply_of_lt_skipWhile_prop {P : Char → Prop} [DecidablePred P] {s : Slice} {pos pos' : s.Pos} (h₁ : pos ≤ pos') (h₂ : pos' < pos.skipWhile P) : P (pos'.get ⋯)

theorem String.Slice.apply_skipPrefixWhile_prop {P : Char → Prop} [DecidablePred P] {s : Slice} {h : s.skipPrefixWhile P ≠ s.endPos} : ¬P ((s.skipPrefixWhile P).get h)

theorem String.Slice.apply_of_lt_skipPrefixWhile_prop {P : Char → Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} (h : pos < s.skipPrefixWhile P) : P (pos.get ⋯)

@[simp]

theorem String.Slice.all_prop_eq {P : Char → Prop} [DecidablePred P] {s : Slice} : s.all P = s.copy.toList.all fun (x : Char) => decide (P x)

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

@[simp]

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

@[simp]

theorem String.Slice.Pos.revSkip?_bool_eq_none_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} : pos.revSkip? p = none ↔ ∀ (h : pos ≠ s.startPos), p ((pos.prev h).get ⋯) = false

theorem String.Slice.Pos.apply_revSkipWhile_bool_eq_false {p : Char → Bool} {s : Slice} {pos : s.Pos} {h : pos.revSkipWhile p ≠ s.startPos} : p (((pos.revSkipWhile p).prev h).get ⋯) = false

theorem String.Slice.Pos.revSkipWhile_bool_eq_self_iff_get {p : Char → Bool} {s : Slice} {pos : s.Pos} : pos.revSkipWhile p = pos ↔ ∀ (h : pos ≠ s.startPos), p ((pos.prev h).get ⋯) = false

theorem String.Slice.Pos.apply_eq_true_of_revSkipWhile_le_bool {p : Char → Bool} {s : Slice} {pos pos' : s.Pos} (h₁ : pos' < pos) (h₂ : pos.revSkipWhile p ≤ pos') : p (pos'.get ⋯) = true

theorem String.Slice.apply_skipSuffixWhile_bool_eq_false {p : Char → Bool} {s : Slice} {h : s.skipSuffixWhile p ≠ s.startPos} : p (((s.skipSuffixWhile p).prev h).get ⋯) = false

theorem String.Slice.apply_eq_true_of_skipSuffixWhile_le_bool {p : Char → Bool} {s : Slice} {pos : s.Pos} (h : s.skipSuffixWhile p ≤ pos) (h' : pos < s.endPos) : p (pos.get ⋯) = true

@[simp]

theorem String.Slice.revAll_bool_eq {p : Char → Bool} {s : Slice} : s.revAll p = s.copy.toList.all p

@[simp]

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

@[simp]

theorem String.Slice.Pos.revSkip?_prop_eq_none_iff {P : Char → Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} : pos.revSkip? P = none ↔ ∀ (h : pos ≠ s.startPos), ¬P ((pos.prev h).get ⋯)

theorem String.Slice.Pos.apply_revSkipWhile_prop {P : Char → Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} {h : pos.revSkipWhile P ≠ s.startPos} : ¬P (((pos.revSkipWhile P).prev h).get ⋯)

theorem String.Slice.Pos.revSkipWhile_prop_eq_self_iff_get {P : Char → Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} : pos.revSkipWhile P = pos ↔ ∀ (h : pos ≠ s.startPos), ¬P ((pos.prev h).get ⋯)

theorem String.Slice.Pos.apply_of_revSkipWhile_le_prop {P : Char → Prop} [DecidablePred P] {s : Slice} {pos pos' : s.Pos} (h₁ : pos' < pos) (h₂ : pos.revSkipWhile P ≤ pos') : P (pos'.get ⋯)

theorem String.Slice.apply_skipSuffixWhile_prop {P : Char → Prop} [DecidablePred P] {s : Slice} {h : s.skipSuffixWhile P ≠ s.startPos} : ¬P (((s.skipSuffixWhile P).prev h).get ⋯)

theorem String.Slice.apply_of_skipSuffixWhile_le_prop {P : Char → Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} (h : s.skipSuffixWhile P ≤ pos) (h' : pos < s.endPos) : P (pos.get ⋯)

@[simp]

theorem String.Slice.revAll_prop_eq {P : Char → Prop} [DecidablePred P] {s : Slice} : s.revAll P = s.copy.toList.all fun (x : Char) => decide (P x)

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

@[simp]

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

@[simp]

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

theorem String.Pos.apply_skipWhile_bool_eq_false {p : Char → Bool} {s : String} {pos : s.Pos} {h : pos.skipWhile p ≠ s.endPos} : p ((pos.skipWhile p).get h) = false

theorem String.Pos.skipWhile_bool_eq_self_iff_get {p : Char → Bool} {s : String} {pos : s.Pos} : pos.skipWhile p = pos ↔ ∀ (h : pos ≠ s.endPos), p (pos.get h) = false

theorem String.Pos.apply_eq_true_of_lt_skipWhile_bool {p : Char → Bool} {s : String} {pos pos' : s.Pos} (h₁ : pos ≤ pos') (h₂ : pos' < pos.skipWhile p) : p (pos'.get ⋯) = true

theorem String.apply_skipPrefixWhile_bool_eq_false {p : Char → Bool} {s : String} {h : s.skipPrefixWhile p ≠ s.endPos} : p ((s.skipPrefixWhile p).get h) = false

theorem String.apply_eq_true_of_lt_skipPrefixWhile_bool {p : Char → Bool} {s : String} {pos : s.Pos} (h : pos < s.skipPrefixWhile p) : p (pos.get ⋯) = true

@[simp]

theorem String.all_bool_eq {p : Char → Bool} {s : String} : s.all p = s.toList.all p

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

@[simp]

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

@[simp]

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

theorem String.Pos.apply_skipWhile_prop {P : Char → Prop} [DecidablePred P] {s : String} {pos : s.Pos} {h : pos.skipWhile P ≠ s.endPos} : ¬P ((pos.skipWhile P).get h)

theorem String.Pos.skipWhile_prop_eq_self_iff_get {P : Char → Prop} [DecidablePred P] {s : String} {pos : s.Pos} : pos.skipWhile P = pos ↔ ∀ (h : pos ≠ s.endPos), ¬P (pos.get h)

theorem String.Pos.apply_of_lt_skipWhile_prop {P : Char → Prop} [DecidablePred P] {s : String} {pos pos' : s.Pos} (h₁ : pos ≤ pos') (h₂ : pos' < pos.skipWhile P) : P (pos'.get ⋯)

theorem String.apply_skipPrefixWhile_prop {P : Char → Prop} [DecidablePred P] {s : String} {h : s.skipPrefixWhile P ≠ s.endPos} : ¬P ((s.skipPrefixWhile P).get h)

theorem String.apply_of_lt_skipPrefixWhile_prop {P : Char → Prop} [DecidablePred P] {s : String} {pos : s.Pos} (h : pos < s.skipPrefixWhile P) : P (pos.get ⋯)

@[simp]

theorem String.all_prop_eq {P : Char → Prop} [DecidablePred P] {s : String} : s.all P = s.toList.all fun (x : Char) => decide (P x)

@[simp]

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

@[simp]

theorem String.Pos.revSkip?_bool_eq_none_iff {p : Char → Bool} {s : String} {pos : s.Pos} : pos.revSkip? p = none ↔ ∀ (h : pos ≠ s.startPos), p ((pos.prev h).get ⋯) = false

theorem String.Pos.apply_revSkipWhile_bool_eq_false {p : Char → Bool} {s : String} {pos : s.Pos} {h : pos.revSkipWhile p ≠ s.startPos} : p (((pos.revSkipWhile p).prev h).get ⋯) = false

theorem String.Pos.revSkipWhile_bool_eq_self_iff_get {p : Char → Bool} {s : String} {pos : s.Pos} : pos.revSkipWhile p = pos ↔ ∀ (h : pos ≠ s.startPos), p ((pos.prev h).get ⋯) = false

theorem String.Pos.apply_eq_true_of_revSkipWhile_le_bool {p : Char → Bool} {s : String} {pos pos' : s.Pos} (h₁ : pos' < pos) (h₂ : pos.revSkipWhile p ≤ pos') : p (pos'.get ⋯) = true

theorem String.apply_skipSuffixWhile_bool_eq_false {p : Char → Bool} {s : String} {h : s.skipSuffixWhile p ≠ s.startPos} : p (((s.skipSuffixWhile p).prev h).get ⋯) = false

theorem String.apply_eq_true_of_skipSuffixWhile_le_bool {p : Char → Bool} {s : String} {pos : s.Pos} (h : s.skipSuffixWhile p ≤ pos) (h' : pos < s.endPos) : p (pos.get ⋯) = true

@[simp]

theorem String.revAll_bool_eq {p : Char → Bool} {s : String} : s.revAll p = s.toList.all p

@[simp]

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

@[simp]

theorem String.Pos.revSkip?_prop_eq_none_iff {P : Char → Prop} [DecidablePred P] {s : String} {pos : s.Pos} : pos.revSkip? P = none ↔ ∀ (h : pos ≠ s.startPos), ¬P ((pos.prev h).get ⋯)

theorem String.Pos.apply_revSkipWhile_prop {P : Char → Prop} [DecidablePred P] {s : String} {pos : s.Pos} {h : pos.revSkipWhile P ≠ s.startPos} : ¬P (((pos.revSkipWhile P).prev h).get ⋯)

theorem String.Pos.revSkipWhile_prop_eq_self_iff_get {P : Char → Prop} [DecidablePred P] {s : String} {pos : s.Pos} : pos.revSkipWhile P = pos ↔ ∀ (h : pos ≠ s.startPos), ¬P ((pos.prev h).get ⋯)

theorem String.Pos.apply_of_revSkipWhile_le_prop {P : Char → Prop} [DecidablePred P] {s : String} {pos pos' : s.Pos} (h₁ : pos' < pos) (h₂ : pos.revSkipWhile P ≤ pos') : P (pos'.get ⋯)

theorem String.apply_skipSuffixWhile_prop {P : Char → Prop} [DecidablePred P] {s : String} {h : s.skipSuffixWhile P ≠ s.startPos} : ¬P (((s.skipSuffixWhile P).prev h).get ⋯)

theorem String.apply_of_skipSuffixWhile_le_prop {P : Char → Prop} [DecidablePred P] {s : String} {pos : s.Pos} (h : s.skipSuffixWhile P ≤ pos) (h' : pos < s.endPos) : P (pos.get ⋯)

@[simp]

theorem String.revAll_prop_eq {P : Char → Prop} [DecidablePred P] {s : String} : s.revAll P = s.toList.all fun (x : Char) => decide (P x)