@[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.endPos_le {s : String} (p : s.Pos) : s.endPos ≤ p ↔ p = s.endPos

@[simp]

theorem String.Pos.lt_endPos_iff {s : String} (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.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.ne_next {s : Slice} {p : s.Pos} {h : p ≠ s.endPos} : p ≠ p.next h

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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.sliceTo_lt_sliceTo_iff {s : Slice} {p₀ q r : s.Pos} {h₁ : q ≤ p₀} {h₂ : r ≤ p₀} : p₀.sliceTo q h₁ < p₀.sliceTo r h₂ ↔ q < r

@[simp]

theorem String.Slice.Pos.sliceTo_le_sliceTo_iff {s : Slice} {p₀ q r : s.Pos} {h₁ : q ≤ p₀} {h₂ : r ≤ p₀} : p₀.sliceTo q h₁ ≤ p₀.sliceTo r h₂ ↔ q ≤ r

@[simp]

theorem String.Pos.sliceTo_lt_sliceTo_iff {s : String} {p₀ q r : s.Pos} {h₁ : q ≤ p₀} {h₂ : r ≤ p₀} : p₀.sliceTo q h₁ < p₀.sliceTo r h₂ ↔ q < r

@[simp]

theorem String.Pos.sliceTo_le_sliceTo_iff {s : String} {p₀ q r : s.Pos} {h₁ : q ≤ p₀} {h₂ : r ≤ p₀} : p₀.sliceTo q h₁ ≤ p₀.sliceTo r h₂ ↔ q ≤ r

@[simp]

theorem String.Slice.Pos.sliceFrom_lt_sliceFrom_iff {s : Slice} {p₀ q r : s.Pos} {h₁ : p₀ ≤ q} {h₂ : p₀ ≤ r} : p₀.sliceFrom q h₁ < p₀.sliceFrom r h₂ ↔ q < r

@[simp]

theorem String.Slice.Pos.sliceFrom_le_sliceFrom_iff {s : Slice} {p₀ q r : s.Pos} {h₁ : p₀ ≤ q} {h₂ : p₀ ≤ r} : p₀.sliceFrom q h₁ ≤ p₀.sliceFrom r h₂ ↔ q ≤ r

@[simp]

theorem String.Pos.sliceFrom_lt_sliceFrom_iff {s : String} {p₀ q r : s.Pos} {h₁ : p₀ ≤ q} {h₂ : p₀ ≤ r} : p₀.sliceFrom q h₁ < p₀.sliceFrom r h₂ ↔ q < r

@[simp]

theorem String.Pos.sliceFrom_le_sliceFrom_iff {s : String} {p₀ q r : s.Pos} {h₁ : p₀ ≤ q} {h₂ : p₀ ≤ r} : p₀.sliceFrom q h₁ ≤ p₀.sliceFrom r h₂ ↔ q ≤ r

theorem String.Slice.Pos.ofSliceFrom_lt_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} : ofSliceFrom p < q ↔ ∃ (h : p₀ ≤ q), p < p₀.sliceFrom q h

theorem String.Slice.Pos.le_ofSliceFrom_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} : q ≤ ofSliceFrom p ↔ ∀ (h : p₀ ≤ q), p₀.sliceFrom q h ≤ p

theorem String.Slice.Pos.ofSliceFrom_le_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} : ofSliceFrom p ≤ q ↔ ∃ (h : p₀ ≤ q), p ≤ p₀.sliceFrom q h

theorem String.Slice.Pos.lt_ofSliceFrom_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} : q < ofSliceFrom p ↔ ∀ (h : p₀ ≤ q), p₀.sliceFrom q h < p

theorem String.Pos.ofSliceFrom_lt_iff {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} : ofSliceFrom p < q ↔ ∃ (h : p₀ ≤ q), p < p₀.sliceFrom q h

theorem String.Pos.le_ofSliceFrom_iff {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} : q ≤ ofSliceFrom p ↔ ∀ (h : p₀ ≤ q), p₀.sliceFrom q h ≤ p

theorem String.Pos.ofSliceFrom_le_iff {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} : ofSliceFrom p ≤ q ↔ ∃ (h : p₀ ≤ q), p ≤ p₀.sliceFrom q h

theorem String.Pos.lt_ofSliceFrom_iff {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} : q < ofSliceFrom p ↔ ∀ (h : p₀ ≤ q), p₀.sliceFrom q h < p

theorem String.Slice.Pos.ofSliceFrom_next {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h : p ≠ (s.sliceFrom p₀).endPos} : ofSliceFrom (p.next h) = (ofSliceFrom p).next ⋯

theorem String.Slice.Pos.next_ofSliceFrom {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h : ofSliceFrom p ≠ s.endPos} : (ofSliceFrom p).next h = ofSliceFrom (p.next ⋯)

theorem String.Pos.ofSliceFrom_next {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h : p ≠ (s.sliceFrom p₀).endPos} : ofSliceFrom (p.next h) = (ofSliceFrom p).next ⋯

theorem String.Pos.next_ofSliceFrom {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h : ofSliceFrom p ≠ s.endPos} : (ofSliceFrom p).next h = ofSliceFrom (p.next ⋯)

theorem String.Slice.Pos.le_ofSliceTo_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} : q ≤ ofSliceTo p ↔ ∃ (h : q ≤ p₀), p₀.sliceTo q h ≤ p

theorem String.Slice.Pos.ofSliceTo_lt_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} : ofSliceTo p < q ↔ ∀ (h : q ≤ p₀), p < p₀.sliceTo q h

theorem String.Slice.Pos.lt_ofSliceTo_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} : q < ofSliceTo p ↔ ∃ (h : q ≤ p₀), p₀.sliceTo q h < p

theorem String.Slice.Pos.ofSliceTo_le_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} : ofSliceTo p ≤ q ↔ ∀ (h : q ≤ p₀), p ≤ p₀.sliceTo q h

theorem String.Pos.le_ofSliceTo_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} : q ≤ ofSliceTo p ↔ ∃ (h : q ≤ p₀), p₀.sliceTo q h ≤ p

theorem String.Pos.ofSliceTo_lt_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} : ofSliceTo p < q ↔ ∀ (h : q ≤ p₀), p < p₀.sliceTo q h

theorem String.Pos.lt_ofSliceTo_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} : q < ofSliceTo p ↔ ∃ (h : q ≤ p₀), p₀.sliceTo q h < p

theorem String.Pos.ofSliceTo_le_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} : ofSliceTo p ≤ q ↔ ∀ (h : q ≤ p₀), p ≤ p₀.sliceTo q h

theorem String.Slice.Pos.lt_sliceFrom_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h : p₀ ≤ q} : p < p₀.sliceFrom q h ↔ ofSliceFrom p < q

theorem String.Slice.Pos.sliceFrom_le_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h : p₀ ≤ q} : p₀.sliceFrom q h ≤ p ↔ q ≤ ofSliceFrom p

theorem String.Slice.Pos.le_sliceFrom_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h : p₀ ≤ q} : p ≤ p₀.sliceFrom q h ↔ ofSliceFrom p ≤ q

theorem String.Slice.Pos.sliceFrom_lt_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h : p₀ ≤ q} : p₀.sliceFrom q h < p ↔ q < ofSliceFrom p

theorem String.Pos.lt_sliceFrom_iff {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h : p₀ ≤ q} : p < p₀.sliceFrom q h ↔ ofSliceFrom p < q

theorem String.Pos.sliceFrom_le_iff {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h : p₀ ≤ q} : p₀.sliceFrom q h ≤ p ↔ q ≤ ofSliceFrom p

theorem String.Pos.le_sliceFrom_iff {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h : p₀ ≤ q} : p ≤ p₀.sliceFrom q h ↔ ofSliceFrom p ≤ q

theorem String.Pos.sliceFrom_lt_iff {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h : p₀ ≤ q} : p₀.sliceFrom q h < p ↔ q < ofSliceFrom p

theorem String.Slice.Pos.sliceTo_le_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h : q ≤ p₀} : p₀.sliceTo q h ≤ p ↔ q ≤ ofSliceTo p

theorem String.Slice.Pos.lt_sliceTo_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h : q ≤ p₀} : p < p₀.sliceTo q h ↔ ofSliceTo p < q

theorem String.Slice.Pos.sliceTo_lt_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h : q ≤ p₀} : p₀.sliceTo q h < p ↔ q < ofSliceTo p

theorem String.Slice.Pos.le_sliceTo_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h : q ≤ p₀} : p ≤ p₀.sliceTo q h ↔ ofSliceTo p ≤ q

theorem String.Pos.sliceTo_le_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h : q ≤ p₀} : p₀.sliceTo q h ≤ p ↔ q ≤ ofSliceTo p

theorem String.Pos.lt_sliceTo_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h : q ≤ p₀} : p < p₀.sliceTo q h ↔ ofSliceTo p < q

theorem String.Pos.sliceTo_lt_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h : q ≤ p₀} : p₀.sliceTo q h < p ↔ q < ofSliceTo p

theorem String.Pos.le_sliceTo_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h : q ≤ p₀} : p ≤ p₀.sliceTo q h ↔ ofSliceTo p ≤ q

theorem String.Slice.Pos.ofSliceTo_ne_endPos {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} (h : p ≠ (s.sliceTo p₀).endPos) : ofSliceTo p ≠ s.endPos

theorem String.Slice.Pos.ne_endPos_of_sliceTo_ne_endPos {s : Slice} {p p₀ : s.Pos} {h₀ : p ≤ p₀} (h : p₀.sliceTo p h₀ ≠ (s.sliceTo p₀).endPos) : p ≠ s.endPos

theorem String.Slice.Pos.ofSliceFrom_ne_startPos {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} (h : p ≠ (s.sliceFrom p₀).startPos) : ofSliceFrom p ≠ s.startPos

theorem String.Slice.Pos.ne_startPos_of_sliceFrom_ne_startPos {s : Slice} {p p₀ : s.Pos} {h₀ : p₀ ≤ p} (h : p₀.sliceFrom p h₀ ≠ (s.sliceFrom p₀).startPos) : p ≠ s.startPos

theorem String.Pos.ofSliceTo_ne_endPos {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} (h : p ≠ (s.sliceTo p₀).endPos) : ofSliceTo p ≠ s.endPos

theorem String.Pos.ne_endPos_of_sliceTo_ne_endPos {s : String} {p p₀ : s.Pos} {h₀ : p ≤ p₀} (h : p₀.sliceTo p h₀ ≠ (s.sliceTo p₀).endPos) : p ≠ s.endPos

theorem String.Pos.ofSliceFrom_ne_startPos {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} (h : p ≠ (s.sliceFrom p₀).startPos) : ofSliceFrom p ≠ s.startPos

theorem String.Pos.ne_startPos_of_sliceFrom_ne_startPos {s : String} {p p₀ : s.Pos} {h₀ : p₀ ≤ p} (h : p₀.sliceFrom p h₀ ≠ (s.sliceFrom p₀).startPos) : p ≠ s.startPos

theorem String.Slice.Pos.ofSliceTo_next {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h : p ≠ (s.sliceTo p₀).endPos} : ofSliceTo (p.next h) = (ofSliceTo p).next ⋯

theorem String.Pos.ofSliceTo_next {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h : p ≠ (s.sliceTo p₀).endPos} : ofSliceTo (p.next h) = (ofSliceTo p).next ⋯

@[simp]

theorem String.Slice.Pos.slice_lt_slice_iff {s : Slice} {p₀ p₁ q r : s.Pos} {h₁ : p₀ ≤ q} {h₁' : p₀ ≤ r} {h₂ : q ≤ p₁} {h₂' : r ≤ p₁} : q.slice p₀ p₁ h₁ h₂ < r.slice p₀ p₁ h₁' h₂' ↔ q < r

@[simp]

theorem String.Slice.Pos.slice_le_slice_iff {s : Slice} {p₀ p₁ q r : s.Pos} {h₁ : p₀ ≤ q} {h₁' : p₀ ≤ r} {h₂ : q ≤ p₁} {h₂' : r ≤ p₁} : q.slice p₀ p₁ h₁ h₂ ≤ r.slice p₀ p₁ h₁' h₂' ↔ q ≤ r

@[simp]

theorem String.Pos.slice_lt_slice_iff {s : String} {p₀ p₁ q r : s.Pos} {h₁ : p₀ ≤ q} {h₁' : p₀ ≤ r} {h₂ : q ≤ p₁} {h₂' : r ≤ p₁} : q.slice p₀ p₁ h₁ h₂ < r.slice p₀ p₁ h₁' h₂' ↔ q < r

@[simp]

theorem String.Pos.slice_le_slice_iff {s : String} {p₀ p₁ q r : s.Pos} {h₁ : p₀ ≤ q} {h₁' : p₀ ≤ r} {h₂ : q ≤ p₁} {h₂' : r ≤ p₁} : q.slice p₀ p₁ h₁ h₂ ≤ r.slice p₀ p₁ h₁' h₂' ↔ q ≤ r

theorem String.Slice.Pos.le_ofSlice_iff {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} : q ≤ ofSlice p ↔ ∃ (h₁ : q ≤ p₁), ∀ (h₀ : p₀ ≤ q), q.slice p₀ p₁ h₀ h₁ ≤ p

theorem String.Slice.Pos.ofSlice_lt_iff {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} : ofSlice p < q ↔ ∀ (h₁ : q ≤ p₁), ∃ (h₀ : p₀ ≤ q), p < q.slice p₀ p₁ h₀ h₁

theorem String.Slice.Pos.lt_ofSlice_iff {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} : q < ofSlice p ↔ ∃ (h₁ : q ≤ p₁), ∀ (h₀ : p₀ ≤ q), q.slice p₀ p₁ h₀ h₁ < p

theorem String.Slice.Pos.ofSlice_le_iff {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} : ofSlice p ≤ q ↔ ∀ (h₁ : q ≤ p₁), ∃ (h₀ : p₀ ≤ q), p ≤ q.slice p₀ p₁ h₀ h₁

theorem String.Pos.le_ofSlice_iff {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} : q ≤ ofSlice p ↔ ∃ (h₁ : q ≤ p₁), ∀ (h₀ : p₀ ≤ q), q.slice p₀ p₁ h₀ h₁ ≤ p

theorem String.Pos.ofSlice_lt_iff {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} : ofSlice p < q ↔ ∀ (h₁ : q ≤ p₁), ∃ (h₀ : p₀ ≤ q), p < q.slice p₀ p₁ h₀ h₁

theorem String.Pos.lt_ofSlice_iff {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} : q < ofSlice p ↔ ∃ (h₁ : q ≤ p₁), ∀ (h₀ : p₀ ≤ q), q.slice p₀ p₁ h₀ h₁ < p

theorem String.Pos.ofSlice_le_iff {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} : ofSlice p ≤ q ↔ ∀ (h₁ : q ≤ p₁), ∃ (h₀ : p₀ ≤ q), p ≤ q.slice p₀ p₁ h₀ h₁

theorem String.Slice.Pos.slice_le_iff {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ : p₀ ≤ q} {h₁ : q ≤ p₁} : q.slice p₀ p₁ h₀ h₁ ≤ p ↔ q ≤ ofSlice p

theorem String.Slice.Pos.lt_slice_iff {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ : p₀ ≤ q} {h₁ : q ≤ p₁} : p < q.slice p₀ p₁ h₀ h₁ ↔ ofSlice p < q

theorem String.Slice.Pos.slice_lt_iff {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ : p₀ ≤ q} {h₁ : q ≤ p₁} : q.slice p₀ p₁ h₀ h₁ < p ↔ q < ofSlice p

theorem String.Slice.Pos.le_slice_iff {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ : p₀ ≤ q} {h₁ : q ≤ p₁} : p ≤ q.slice p₀ p₁ h₀ h₁ ↔ ofSlice p ≤ q

theorem String.Pos.slice_le_iff {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ : p₀ ≤ q} {h₁ : q ≤ p₁} : q.slice p₀ p₁ h₀ h₁ ≤ p ↔ q ≤ ofSlice p

theorem String.Pos.lt_slice_iff {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ : p₀ ≤ q} {h₁ : q ≤ p₁} : p < q.slice p₀ p₁ h₀ h₁ ↔ ofSlice p < q

theorem String.Pos.slice_lt_iff {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ : p₀ ≤ q} {h₁ : q ≤ p₁} : q.slice p₀ p₁ h₀ h₁ < p ↔ q < ofSlice p

theorem String.Pos.le_slice_iff {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ : p₀ ≤ q} {h₁ : q ≤ p₁} : p ≤ q.slice p₀ p₁ h₀ h₁ ↔ ofSlice p ≤ q

theorem String.Slice.Pos.ofSlice_ne_endPos {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} : p ≠ (s.slice p₀ p₁ h).endPos → ofSlice p ≠ s.endPos

theorem String.Slice.Pos.ne_endPos_of_slice_ne_endPos {s : Slice} {p p₀ p₁ : s.Pos} {h₁ : p₀ ≤ p} {h₂ : p ≤ p₁} (h : p.slice p₀ p₁ h₁ h₂ ≠ (s.slice p₀ p₁ ⋯).endPos) : p ≠ s.endPos

theorem String.Slice.Pos.ofSlice_ne_startPos {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} : p ≠ (s.slice p₀ p₁ h).startPos → ofSlice p ≠ s.startPos

theorem String.Slice.Pos.ne_startPos_of_slice_ne_startPos {s : Slice} {p p₀ p₁ : s.Pos} {h₁ : p₀ ≤ p} {h₂ : p ≤ p₁} (h : p.slice p₀ p₁ h₁ h₂ ≠ (s.slice p₀ p₁ ⋯).startPos) : p ≠ s.startPos

theorem String.Pos.ofSlice_ne_endPos {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} : p ≠ (s.slice p₀ p₁ h).endPos → ofSlice p ≠ s.endPos

theorem String.Pos.ne_endPos_of_slice_ne_endPos {s : String} {p p₀ p₁ : s.Pos} {h₁ : p₀ ≤ p} {h₂ : p ≤ p₁} (h : p.slice p₀ p₁ h₁ h₂ ≠ (s.slice p₀ p₁ ⋯).endPos) : p ≠ s.endPos

theorem String.Pos.ofSlice_ne_startPos {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} : p ≠ (s.slice p₀ p₁ h).startPos → ofSlice p ≠ s.startPos

theorem String.Pos.ne_startPos_of_slice_ne_startPos {s : String} {p p₀ p₁ : s.Pos} {h₁ : p₀ ≤ p} {h₂ : p ≤ p₁} (h : p.slice p₀ p₁ h₁ h₂ ≠ (s.slice p₀ p₁ ⋯).startPos) : p ≠ s.startPos

@[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

theorem String.Slice.Pos.get_eq_get_ofSliceTo {s : Slice} {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos} {h : pos ≠ (s.sliceTo p₀).endPos} : pos.get h = (ofSliceTo pos).get ⋯

theorem String.Slice.Pos.get_sliceTo {s : Slice} {p₀ p : s.Pos} {h : p ≤ p₀} {h' : p₀.sliceTo p h ≠ (s.sliceTo p₀).endPos} : (p₀.sliceTo p h).get h' = p.get ⋯

theorem String.Pos.get_eq_get_ofSliceTo {s : String} {p₀ : s.Pos} {pos : (s.sliceTo p₀).Pos} {h : pos ≠ (s.sliceTo p₀).endPos} : pos.get h = (ofSliceTo pos).get ⋯

theorem String.Pos.get_sliceTo {s : String} {p₀ p : s.Pos} {h : p ≤ p₀} {h' : p₀.sliceTo p h ≠ (s.sliceTo p₀).endPos} : (p₀.sliceTo p h).get h' = p.get ⋯

theorem String.Slice.Pos.get_eq_get_ofSlice {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {pos : (s.slice p₀ p₁ h).Pos} {h' : pos ≠ (s.slice p₀ p₁ h).endPos} : pos.get h' = (ofSlice pos).get ⋯

theorem String.Slice.Pos.get_slice {s : Slice} {p p₀ p₁ : s.Pos} {h₁ : p₀ ≤ p} {h₂ : p ≤ p₁} {h : p.slice p₀ p₁ h₁ h₂ ≠ (s.slice p₀ p₁ ⋯).endPos} : (p.slice p₀ p₁ h₁ h₂).get h = p.get ⋯

theorem String.Pos.get_eq_get_ofSlice {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {pos : (s.slice p₀ p₁ h).Pos} {h' : pos ≠ (s.slice p₀ p₁ h).endPos} : pos.get h' = (ofSlice pos).get ⋯

theorem String.Pos.get_slice {s : String} {p p₀ p₁ : s.Pos} {h₁ : p₀ ≤ p} {h₂ : p ≤ p₁} {h : p.slice p₀ p₁ h₁ h₂ ≠ (s.slice p₀ p₁ ⋯).endPos} : (p.slice p₀ p₁ h₁ h₂).get h = p.get ⋯

theorem String.Slice.Pos.ofSlice_next {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {h' : p ≠ (s.slice p₀ p₁ h).endPos} : ofSlice (p.next h') = (ofSlice p).next ⋯

theorem String.Pos.ofSlice_next {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {h' : p ≠ (s.slice p₀ p₁ h).endPos} : ofSlice (p.next h') = (ofSlice p).next ⋯