theorem String.Slice.skipPrefix?_char_eq_some_iff {c : Char} {s : Slice} {pos : s.Pos} : s.skipPrefix? c = some pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ s.startPos.get h = c

theorem String.Slice.startsWith_char_iff_get {c : Char} {s : Slice} : s.startsWith c = true ↔ ∃ (h : s.startPos ≠ s.endPos), s.startPos.get h = c

theorem String.Slice.startsWith_char_eq_false_iff_get {c : Char} {s : Slice} : s.startsWith c = false ↔ ∀ (h : s.startPos ≠ s.endPos), s.startPos.get h ≠ c

theorem String.Slice.startsWith_char_eq_head? {c : Char} {s : Slice} : s.startsWith c = (s.copy.toList.head? == some c)

theorem String.Slice.startsWith_char_iff_exists_append {c : Char} {s : Slice} : s.startsWith c = true ↔ ∃ (t : String), s.copy = singleton c ++ t

theorem String.Slice.startsWith_char_eq_false_iff_forall_append {c : Char} {s : Slice} : s.startsWith c = false ↔ ∀ (t : String), s.copy ≠ singleton c ++ t

theorem String.Slice.eq_append_of_dropPrefix?_char_eq_some {c : Char} {s res : Slice} (h : s.dropPrefix? c = some res) : s.copy = singleton c ++ res.copy

theorem String.Slice.Pos.skip?_char_eq_some_iff {c : Char} {s : Slice} {pos res : s.Pos} : pos.skip? c = some res ↔ ∃ (h : pos ≠ s.endPos), res = pos.next h ∧ pos.get h = c

@[simp]

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

theorem String.Slice.Pos.get_skipWhile_char_ne {c : Char} {s : Slice} {pos : s.Pos} {h : pos.skipWhile c ≠ s.endPos} : (pos.skipWhile c).get h ≠ c

theorem String.Slice.Pos.skipWhile_char_eq_self_iff_get {c : Char} {s : Slice} {pos : s.Pos} : pos.skipWhile c = pos ↔ ∀ (h : pos ≠ s.endPos), pos.get h ≠ c

theorem String.Slice.Pos.get_eq_of_lt_skipWhile_char {c : Char} {s : Slice} {pos pos' : s.Pos} (h₁ : pos ≤ pos') (h₂ : pos' < pos.skipWhile c) : pos'.get ⋯ = c

theorem String.Slice.get_skipPrefixWhile_char_ne {c : Char} {s : Slice} {h : s.skipPrefixWhile c ≠ s.endPos} : (s.skipPrefixWhile c).get h ≠ c

theorem String.Slice.get_eq_of_lt_skipPrefixWhile_char {c : Char} {s : Slice} {pos : s.Pos} (h : pos < s.skipPrefixWhile c) : pos.get ⋯ = c

@[simp]

theorem String.Slice.all_char_iff {c : Char} {s : Slice} : s.all c = true ↔ s.copy.toList = List.replicate s.copy.toList.length c

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

@[simp]

theorem String.Slice.Pos.revSkip?_char_eq_none_iff {c : Char} {s : Slice} {pos : s.Pos} : pos.revSkip? c = none ↔ ∀ (h : pos ≠ s.startPos), (pos.prev h).get ⋯ ≠ c

theorem String.Slice.Pos.get_revSkipWhile_char_ne {c : Char} {s : Slice} {pos : s.Pos} {h : pos.revSkipWhile c ≠ s.startPos} : ((pos.revSkipWhile c).prev h).get ⋯ ≠ c

theorem String.Slice.Pos.revSkipWhile_char_eq_self_iff_get {c : Char} {s : Slice} {pos : s.Pos} : pos.revSkipWhile c = pos ↔ ∀ (h : pos ≠ s.startPos), (pos.prev h).get ⋯ ≠ c

theorem String.Slice.Pos.get_eq_of_revSkipWhile_le_char {c : Char} {s : Slice} {pos pos' : s.Pos} (h₁ : pos' < pos) (h₂ : pos.revSkipWhile c ≤ pos') : pos'.get ⋯ = c

theorem String.Slice.get_skipSuffixWhile_char_ne {c : Char} {s : Slice} {h : s.skipSuffixWhile c ≠ s.startPos} : ((s.skipSuffixWhile c).prev h).get ⋯ ≠ c

theorem String.Slice.get_eq_of_skipSuffixWhile_le_char {c : Char} {s : Slice} {pos : s.Pos} (h : s.skipSuffixWhile c ≤ pos) (h' : pos < s.endPos) : pos.get ⋯ = c

@[simp]

theorem String.Slice.revAll_char_iff {c : Char} {s : Slice} : s.revAll c = true ↔ s.copy.toList = List.replicate s.copy.toList.length c

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

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

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

theorem String.Slice.endsWith_char_iff_exists_append {c : Char} {s : Slice} : s.endsWith c = true ↔ ∃ (t : String), s.copy = t ++ singleton c

theorem String.Slice.endsWith_char_eq_getLast? {c : Char} {s : Slice} : s.endsWith c = (s.copy.toList.getLast? == some c)

theorem String.Slice.endsWith_char_eq_false_iff_forall_append {c : Char} {s : Slice} : s.endsWith c = false ↔ ∀ (t : String), s.copy ≠ t ++ singleton c

theorem String.Slice.eq_append_of_dropSuffix?_char_eq_some {c : Char} {s res : Slice} (h : s.dropSuffix? c = some res) : s.copy = res.copy ++ singleton c

theorem String.skipPrefix?_char_eq_some_iff {c : Char} {s : String} {pos : s.Pos} : s.skipPrefix? c = some pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ s.startPos.get h = c

theorem String.startsWith_char_iff_get {c : Char} {s : String} : s.startsWith c = true ↔ ∃ (h : s.startPos ≠ s.endPos), s.startPos.get h = c

theorem String.startsWith_char_eq_false_iff_get {c : Char} {s : String} : s.startsWith c = false ↔ ∀ (h : s.startPos ≠ s.endPos), s.startPos.get h ≠ c

theorem String.startsWith_char_eq_head? {c : Char} {s : String} : s.startsWith c = (s.toList.head? == some c)

theorem String.startsWith_char_iff_exists_append {c : Char} {s : String} : s.startsWith c = true ↔ ∃ (t : String), s = singleton c ++ t

theorem String.startsWith_char_eq_false_iff_forall_append {c : Char} {s : String} : s.startsWith c = false ↔ ∀ (t : String), s ≠ singleton c ++ t

theorem String.eq_append_of_dropPrefix?_char_eq_some {c : Char} {s : String} {res : Slice} (h : s.dropPrefix? c = some res) : s = singleton c ++ res.copy

theorem String.skipSuffix?_char_eq_some_iff {c : Char} {s : String} {pos : s.Pos} : s.skipSuffix? c = some pos ↔ ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ (s.endPos.prev h).get ⋯ = c

theorem String.endsWith_char_iff_get {c : Char} {s : String} : s.endsWith c = true ↔ ∃ (h : s.endPos ≠ s.startPos), (s.endPos.prev h).get ⋯ = c

theorem String.endsWith_char_eq_false_iff_get {c : Char} {s : String} : s.endsWith c = false ↔ ∀ (h : s.endPos ≠ s.startPos), (s.endPos.prev h).get ⋯ ≠ c

theorem String.endsWith_char_eq_getLast? {c : Char} {s : String} : s.endsWith c = (s.toList.getLast? == some c)

theorem String.endsWith_char_iff_exists_append {c : Char} {s : String} : s.endsWith c = true ↔ ∃ (t : String), s = t ++ singleton c

theorem String.endsWith_char_eq_false_iff_forall_append {c : Char} {s : String} : s.endsWith c = false ↔ ∀ (t : String), s ≠ t ++ singleton c

theorem String.eq_append_of_dropSuffix?_char_eq_some {c : Char} {s : String} {res : Slice} (h : s.dropSuffix? c = some res) : s = res.copy ++ singleton c