@[simp]

theorem String.Slice.Pos.next_le_iff_lt {s : Slice} {p q : s.Pos} {h : p ≠ s.endPos} : p.next h ≤ q ↔ p < q

@[simp]

theorem String.Slice.Pos.lt_next_iff_le {s : Slice} {p q : s.Pos} {h : q ≠ s.endPos} : p < q.next h ↔ p ≤ q

theorem String.Slice.Pos.next_eq_iff {s : Slice} {p q : s.Pos} {h : p ≠ s.endPos} : p.next h = q ↔ p < q ∧ ∀ (q' : s.Pos), p < q' → q ≤ q'

@[simp]

theorem String.Pos.next_le_iff_lt {s : String} {p q : s.Pos} {h : p ≠ s.endPos} : p.next h ≤ q ↔ p < q

@[simp]

theorem String.Pos.lt_next_iff_le {s : String} {p q : s.Pos} {h : q ≠ s.endPos} : p < q.next h ↔ p ≤ q

theorem String.Pos.next_eq_iff {s : String} {p q : s.Pos} {h : p ≠ s.endPos} : p.next h = q ↔ p < q ∧ ∀ (q' : s.Pos), p < q' → q ≤ q'

@[simp]

theorem String.Slice.Pos.le_startPos {s : Slice} (p : s.Pos) : p ≤ s.startPos ↔ p = s.startPos

@[simp]

theorem String.Slice.Pos.startPos_lt_iff {s : Slice} (p : s.Pos) : s.startPos < p ↔ p ≠ s.startPos

@[simp]

theorem String.Slice.Pos.endPos_le {s : Slice} (p : s.Pos) : s.endPos ≤ p ↔ p = s.endPos

@[simp]

theorem String.Slice.Pos.lt_endPos_iff {s : Slice} (p : s.Pos) : p < s.endPos ↔ p ≠ s.endPos

@[simp]

theorem String.Pos.le_startPos {s : String} (p : s.Pos) : p ≤ s.startPos ↔ p = s.startPos

@[simp]

theorem String.Pos.startPos_lt_iff {s : String} {p : s.Pos} : s.startPos < p ↔ p ≠ s.startPos

@[simp]

theorem String.Pos.endPos_le {s : String} (p : s.Pos) : s.endPos ≤ p ↔ p = s.endPos

@[simp]

theorem String.Slice.Pos.not_lt_startPos {s : Slice} {p : s.Pos} : ¬p < s.startPos

theorem String.Slice.Pos.ne_startPos_of_lt {s : Slice} {p q : s.Pos} : p < q → q ≠ s.startPos

@[simp]

theorem String.Pos.not_lt_startPos {s : String} {p : s.Pos} : ¬p < s.startPos

@[simp]

theorem String.Slice.Pos.not_endPos_lt {s : Slice} {p : s.Pos} : ¬s.endPos < p

@[simp]

theorem String.Pos.not_endPos_lt {s : String} {p : s.Pos} : ¬s.endPos < p

theorem String.Pos.ne_endPos_of_lt {s : String} {p q : s.Pos} : p < q → p ≠ s.endPos

@[simp]

theorem String.Slice.Pos.le_next {s : Slice} {p : s.Pos} {h : p ≠ s.endPos} : p ≤ p.next h

@[simp]

theorem String.Pos.le_next {s : String} {p : s.Pos} {h : p ≠ s.endPos} : p ≤ p.next h

@[simp]

theorem String.Slice.Pos.next_ne_startPos {s : Slice} {p : s.Pos} {h : p ≠ s.endPos} : p.next h ≠ s.startPos

theorem String.Slice.Pos.ofSliceTo_lt_ofSliceTo_iff {s : Slice} {p : s.Pos} {q r : (s.sliceTo p).Pos} : ofSliceTo q < ofSliceTo r ↔ q < r

theorem String.Slice.Pos.ofSliceTo_le_ofSliceTo_iff {s : Slice} {p : s.Pos} {q r : (s.sliceTo p).Pos} : ofSliceTo q ≤ ofSliceTo r ↔ q ≤ r

@[simp]

theorem String.Slice.Pos.offset_le_rawEndPos {s : Slice} {p : s.Pos} : p.offset ≤ s.rawEndPos

@[simp]

theorem String.Pos.offset_le_rawEndPos {s : String} {p : s.Pos} : p.offset ≤ s.rawEndPos

@[simp]

theorem String.Slice.Pos.byteIdx_offset_le_utf8ByteSize {s : Slice} {p : s.Pos} : p.offset.byteIdx ≤ s.utf8ByteSize

@[simp]

theorem String.Pos.byteIdx_offset_le_utf8ByteSize {s : String} {p : s.Pos} : p.offset.byteIdx ≤ s.utf8ByteSize

@[simp]

theorem String.Slice.Pos.offset_lt_rawEndPos_iff {s : Slice} {p : s.Pos} : p.offset < s.rawEndPos ↔ p ≠ s.endPos

@[simp]

theorem String.Pos.offset_lt_rawEndPos_iff {s : String} {p : s.Pos} : p.offset < s.rawEndPos ↔ p ≠ s.endPos

@[simp]

theorem String.Slice.Pos.getUTF8Byte_offset {s : Slice} {p : s.Pos} {h : p.offset < s.rawEndPos} : s.getUTF8Byte p.offset h = p.byte ⋯

theorem String.Slice.Pos.isUTF8FirstByte_getUTF8Byte_offset {s : Slice} {p : s.Pos} {h : p.offset < s.rawEndPos} : (s.getUTF8Byte p.offset h).IsUTF8FirstByte

theorem String.Pos.getUTF8Byte_offset {s : String} {p : s.Pos} {h : p.offset < s.rawEndPos} : s.getUTF8Byte p.offset h = p.byte ⋯

theorem String.Pos.isUTF8FirstByte_getUTF8Byte_offset {s : String} {p : s.Pos} {h : p.offset < s.rawEndPos} : (s.getUTF8Byte p.offset h).IsUTF8FirstByte