@[simp]

theorem String.Slice.le_offset_posGE {s : Slice} {p : Pos.Raw} {h : p ≤ s.rawEndPos} : p ≤ (s.posGE p h).offset

@[simp]

theorem String.Slice.posGE_le_iff {s : Slice} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} : s.posGE p h ≤ q ↔ p ≤ q.offset

@[simp]

theorem String.Slice.lt_posGE_iff {s : Slice} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} : q < s.posGE p h ↔ q.offset < p

theorem String.Slice.posGE_eq_iff {s : Slice} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} : s.posGE p h = q ↔ p ≤ q.offset ∧ ∀ (q' : s.Pos), p ≤ q'.offset → q ≤ q'

theorem String.Slice.posGT_eq_posGE {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} : s.posGT p h = s.posGE p.inc ⋯

@[simp]

theorem String.Slice.posGE_inc {s : Slice} {p : Pos.Raw} {h : p.inc ≤ s.rawEndPos} : s.posGE p.inc h = s.posGT p h

@[simp]

theorem String.Slice.lt_offset_posGT {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} : p < (s.posGT p h).offset

@[simp]

theorem String.Slice.posGT_le_iff {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} : s.posGT p h ≤ q ↔ p < q.offset

@[simp]

theorem String.Slice.lt_posGT_iff {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} : q < s.posGT p h ↔ q.offset ≤ p

theorem String.Slice.posGT_eq_iff {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} : s.posGT p h = q ↔ p < q.offset ∧ ∀ (q' : s.Pos), p < q'.offset → q ≤ q'

@[simp]

theorem String.Slice.Pos.posGE_offset {s : Slice} {p : s.Pos} : s.posGE p.offset ⋯ = p

@[simp]

theorem String.Slice.offset_posGE_eq_self_iff {s : Slice} {p : Pos.Raw} {h : p ≤ s.rawEndPos} : (s.posGE p h).offset = p ↔ Pos.Raw.IsValidForSlice s p

theorem String.Slice.posGE_eq_pos {s : Slice} {p : Pos.Raw} (h : Pos.Raw.IsValidForSlice s p) : s.posGE p ⋯ = s.pos p h

theorem String.Slice.pos_eq_posGE {s : Slice} {p : Pos.Raw} {h : Pos.Raw.IsValidForSlice s p} : s.pos p h = s.posGE p ⋯

@[simp]

theorem String.Slice.Pos.posGT_offset {s : Slice} {p : s.Pos} {h : p.offset < s.rawEndPos} : s.posGT p.offset h = p.next ⋯

theorem String.Slice.posGT_eq_next {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} (h' : Pos.Raw.IsValidForSlice s p) : s.posGT p h = (s.pos p h').next ⋯

theorem String.Slice.Pos.next_eq_posGT {s : Slice} {p : s.Pos} {h : p ≠ s.endPos} : p.next h = s.posGT p.offset ⋯

@[simp]

theorem String.Slice.offset_posLE_le {s : Slice} {p : Pos.Raw} : (s.posLE p).offset ≤ p

@[simp]

theorem String.Slice.le_posLE_iff {s : Slice} {p : s.Pos} {q : Pos.Raw} : p ≤ s.posLE q ↔ p.offset ≤ q

@[simp]

theorem String.Slice.posLE_lt_iff {s : Slice} {p : s.Pos} {q : Pos.Raw} : s.posLE q < p ↔ q < p.offset

theorem String.Slice.posLE_eq_iff {s : Slice} {p : Pos.Raw} {q : s.Pos} : s.posLE p = q ↔ q.offset ≤ p ∧ ∀ (q' : s.Pos), q'.offset ≤ p → q' ≤ q

theorem String.Slice.posLT_eq_posLE {s : Slice} {p : Pos.Raw} {h : 0 < p} : s.posLT p h = s.posLE p.dec

theorem String.Slice.posLE_dec {s : Slice} {p : Pos.Raw} (h : 0 < p) : s.posLE p.dec = s.posLT p h

@[simp]

theorem String.Slice.offset_posLT_lt {s : Slice} {p : Pos.Raw} {h : 0 < p} : (s.posLT p h).offset < p

@[simp]

theorem String.Slice.le_posLT_iff {s : Slice} {p : Pos.Raw} {h : 0 < p} {q : s.Pos} : q ≤ s.posLT p h ↔ q.offset < p

@[simp]

theorem String.Slice.posLT_lt_iff {s : Slice} {p : Pos.Raw} {h : 0 < p} {q : s.Pos} : s.posLT p h < q ↔ p ≤ q.offset

theorem String.Slice.posLT_eq_iff {s : Slice} {p : Pos.Raw} {h : 0 < p} {q : s.Pos} : s.posLT p h = q ↔ q.offset < p ∧ ∀ (q' : s.Pos), q'.offset < p → q' ≤ q

@[simp]

theorem String.Slice.Pos.posLE_offset {s : Slice} {p : s.Pos} : s.posLE p.offset = p

@[simp]

theorem String.Slice.offset_posLE_eq_self_iff {s : Slice} {p : Pos.Raw} : (s.posLE p).offset = p ↔ Pos.Raw.IsValidForSlice s p

theorem String.Slice.posLE_eq_pos {s : Slice} {p : Pos.Raw} (h : Pos.Raw.IsValidForSlice s p) : s.posLE p = s.pos p h

theorem String.Slice.pos_eq_posLE {s : Slice} {p : Pos.Raw} {h : Pos.Raw.IsValidForSlice s p} : s.pos p h = s.posLE p

@[simp]

theorem String.Slice.Pos.posLT_offset {s : Slice} {p : s.Pos} {h : 0 < p.offset} : s.posLT p.offset h = p.prev ⋯

theorem String.Slice.posLT_eq_prev {s : Slice} {p : Pos.Raw} {h : 0 < p} (h' : Pos.Raw.IsValidForSlice s p) : s.posLT p h = (s.pos p h').prev ⋯

theorem String.Slice.Pos.prev_eq_posLT {s : Slice} {p : s.Pos} {h : p ≠ s.startPos} : p.prev h = s.posLT p.offset ⋯

@[simp]

theorem String.Slice.Pos.le_prev_iff_lt {s : Slice} {p q : s.Pos} {h : q ≠ s.startPos} : p ≤ q.prev h ↔ p < q

@[simp]

theorem String.Slice.Pos.prev_lt_iff_le {s : Slice} {p q : s.Pos} {h : p ≠ s.startPos} : p.prev h < q ↔ p ≤ q

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

@[simp]

theorem String.Slice.Pos.prev_lt {s : Slice} {p : s.Pos} {h : p ≠ s.startPos} : p.prev h < p

@[simp]

theorem String.Slice.Pos.prev_le {s : Slice} {p : s.Pos} {h : p ≠ s.startPos} : p.prev h ≤ p

@[simp]

theorem String.Slice.Pos.prev_ne_endPos {s : Slice} {p : s.Pos} {h : p ≠ s.startPos} : p.prev h ≠ s.endPos

theorem String.Slice.Pos.prevn_le {s : Slice} {p : s.Pos} {n : Nat} : p.prevn n ≤ p

theorem String.Slice.Pos.ofSliceTo_prev {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h : p ≠ (s.sliceTo p₀).startPos} : ofSliceTo (p.prev h) = (ofSliceTo p).prev ⋯

theorem String.Slice.Pos.prev_ofSliceTo {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h : ofSliceTo p ≠ s.startPos} : (ofSliceTo p).prev h = ofSliceTo (p.prev ⋯)

theorem String.Slice.Pos.ofSliceFrom_prev {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h : p ≠ (s.sliceFrom p₀).startPos} : ofSliceFrom (p.prev h) = (ofSliceFrom p).prev ⋯

theorem String.Slice.Pos.ofSlice_prev {s : Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {h' : p ≠ (s.slice p₀ p₁ h).startPos} : ofSlice (p.prev h') = (ofSlice p).prev ⋯

@[simp]

theorem String.Slice.Pos.prev_next {s : Slice} {p : s.Pos} {h : p ≠ s.endPos} : (p.next h).prev ⋯ = p

@[simp]

theorem String.Slice.Pos.next_prev {s : Slice} {p : s.Pos} {h : p ≠ s.startPos} : (p.prev h).next ⋯ = p

theorem String.Slice.Pos.prev?_eq_dif {s : Slice} {p : s.Pos} : p.prev? = if h : p = s.startPos then none else some (p.prev h)

theorem String.Slice.Pos.prev?_eq_some_prev {s : Slice} {p : s.Pos} (h : p ≠ s.startPos) : p.prev? = some (p.prev h)

@[simp]

theorem String.Slice.Pos.prev?_eq_none_iff {s : Slice} {p : s.Pos} : p.prev? = none ↔ p = s.startPos

theorem String.Slice.Pos.prev?_eq_none {s : Slice} {p : s.Pos} (h : p = s.startPos) : p.prev? = none

@[simp]

theorem String.Slice.Pos.prev?_startPos {s : Slice} : s.startPos.prev? = none

@[simp]

theorem String.le_offset_posGE {s : String} {p : Pos.Raw} {h : p ≤ s.rawEndPos} : p ≤ (s.posGE p h).offset

@[simp]

theorem String.posGE_le_iff {s : String} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} : s.posGE p h ≤ q ↔ p ≤ q.offset

@[simp]

theorem String.lt_posGE_iff {s : String} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} : q < s.posGE p h ↔ q.offset < p

theorem String.posGE_eq_iff {s : String} {p : Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos} : s.posGE p h = q ↔ p ≤ q.offset ∧ ∀ (q' : s.Pos), p ≤ q'.offset → q ≤ q'

theorem String.posGT_eq_posGE {s : String} {p : Pos.Raw} {h : p < s.rawEndPos} : s.posGT p h = s.posGE p.inc ⋯

@[simp]

theorem String.posGE_inc {s : String} {p : Pos.Raw} {h : p.inc ≤ s.rawEndPos} : s.posGE p.inc h = s.posGT p h

@[simp]

theorem String.lt_offset_posGT {s : String} {p : Pos.Raw} {h : p < s.rawEndPos} : p < (s.posGT p h).offset

@[simp]

theorem String.posGT_le_iff {s : String} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} : s.posGT p h ≤ q ↔ p < q.offset

@[simp]

theorem String.lt_posGT_iff {s : String} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} : q < s.posGT p h ↔ q.offset ≤ p

theorem String.posGT_eq_iff {s : String} {p : Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos} : s.posGT p h = q ↔ p < q.offset ∧ ∀ (q' : s.Pos), p < q'.offset → q ≤ q'

theorem String.posGE_toSlice {s : String} {p : Pos.Raw} (h : p ≤ s.toSlice.rawEndPos) : s.toSlice.posGE p h = (s.posGE p h).toSlice

theorem String.posGE_eq_posGE_toSlice {s : String} {p : Pos.Raw} (h : p ≤ s.rawEndPos) : s.posGE p h = Pos.ofToSlice (s.toSlice.posGE p ⋯)

theorem String.posGT_toSlice {s : String} {p : Pos.Raw} (h : p < s.toSlice.rawEndPos) : s.toSlice.posGT p h = (s.posGT p h).toSlice

theorem String.posGT_eq_posGT_toSlice {s : String} {p : Pos.Raw} (h : p < s.rawEndPos) : s.posGT p h = Pos.ofToSlice (s.toSlice.posGT p ⋯)

@[simp]

theorem String.Pos.posGE_offset {s : String} {p : s.Pos} : s.posGE p.offset ⋯ = p

@[simp]

theorem String.offset_posGE_eq_self_iff {s : String} {p : Pos.Raw} {h : p ≤ s.rawEndPos} : (s.posGE p h).offset = p ↔ Pos.Raw.IsValid s p

theorem String.posGE_eq_pos {s : String} {p : Pos.Raw} (h : Pos.Raw.IsValid s p) : s.posGE p ⋯ = s.pos p h

theorem String.pos_eq_posGE {s : String} {p : Pos.Raw} {h : Pos.Raw.IsValid s p} : s.pos p h = s.posGE p ⋯

@[simp]

theorem String.Pos.posGT_offset {s : String} {p : s.Pos} {h : p.offset < s.rawEndPos} : s.posGT p.offset h = p.next ⋯

theorem String.posGT_eq_next {s : String} {p : Pos.Raw} {h : p < s.rawEndPos} (h' : Pos.Raw.IsValid s p) : s.posGT p h = (s.pos p h').next ⋯

theorem String.next_eq_posGT {s : String} {p : s.Pos} {h : p ≠ s.endPos} : p.next h = s.posGT p.offset ⋯

@[simp]

theorem String.offset_posLE_le {s : String} {p : Pos.Raw} : (s.posLE p).offset ≤ p

@[simp]

theorem String.le_posLE_iff {s : String} {p : s.Pos} {q : Pos.Raw} : p ≤ s.posLE q ↔ p.offset ≤ q

@[simp]

theorem String.posLE_lt_iff {s : String} {p : s.Pos} {q : Pos.Raw} : s.posLE q < p ↔ q < p.offset

theorem String.posLE_eq_iff {s : String} {p : Pos.Raw} {q : s.Pos} : s.posLE p = q ↔ q.offset ≤ p ∧ ∀ (q' : s.Pos), q'.offset ≤ p → q' ≤ q

theorem String.posLT_eq_posLE {s : String} {p : Pos.Raw} {h : 0 < p} : s.posLT p h = s.posLE p.dec

theorem String.posLE_dec {s : String} {p : Pos.Raw} (h : 0 < p) : s.posLE p.dec = s.posLT p h

@[simp]

theorem String.offset_posLT_lt {s : String} {p : Pos.Raw} {h : 0 < p} : (s.posLT p h).offset < p

@[simp]

theorem String.le_posLT_iff {s : String} {p : Pos.Raw} {h : 0 < p} {q : s.Pos} : q ≤ s.posLT p h ↔ q.offset < p

@[simp]

theorem String.posLT_lt_iff {s : String} {p : Pos.Raw} {h : 0 < p} {q : s.Pos} : s.posLT p h < q ↔ p ≤ q.offset

theorem String.posLT_eq_iff {s : String} {p : Pos.Raw} {h : 0 < p} {q : s.Pos} : s.posLT p h = q ↔ q.offset < p ∧ ∀ (q' : s.Pos), q'.offset < p → q' ≤ q

theorem String.posLE_toSlice {s : String} {p : Pos.Raw} : s.toSlice.posLE p = (s.posLE p).toSlice

theorem String.posLE_eq_posLE_toSlice {s : String} {p : Pos.Raw} : s.posLE p = Pos.ofToSlice (s.toSlice.posLE p)

theorem String.posLT_toSlice {s : String} {p : Pos.Raw} (h : 0 < p) : s.toSlice.posLT p h = (s.posLT p h).toSlice

theorem String.posLT_eq_posLT_toSlice {s : String} {p : Pos.Raw} (h : 0 < p) : s.posLT p h = Pos.ofToSlice (s.toSlice.posLT p h)

@[simp]

theorem String.Pos.posLE_offset {s : String} {p : s.Pos} : s.posLE p.offset = p

@[simp]

theorem String.offset_posLE_eq_self_iff {s : String} {p : Pos.Raw} : (s.posLE p).offset = p ↔ Pos.Raw.IsValid s p

theorem String.posLE_eq_pos {s : String} {p : Pos.Raw} (h : Pos.Raw.IsValid s p) : s.posLE p = s.pos p h

theorem String.pos_eq_posLE {s : String} {p : Pos.Raw} {h : Pos.Raw.IsValid s p} : s.pos p h = s.posLE p

@[simp]

theorem String.Pos.posLT_offset {s : String} {p : s.Pos} {h : 0 < p.offset} : s.posLT p.offset h = p.prev ⋯

theorem String.posLT_eq_prev {s : String} {p : Pos.Raw} {h : 0 < p} (h' : Pos.Raw.IsValid s p) : s.posLT p h = (s.pos p h').prev ⋯

theorem String.Pos.prev_eq_posLT {s : String} {p : s.Pos} {h : p ≠ s.startPos} : p.prev h = s.posLT p.offset ⋯

@[simp]

theorem String.Pos.le_prev_iff_lt {s : String} {p q : s.Pos} {h : q ≠ s.startPos} : p ≤ q.prev h ↔ p < q

@[simp]

theorem String.Pos.prev_lt_iff_le {s : String} {p q : s.Pos} {h : p ≠ s.startPos} : p.prev h < q ↔ p ≤ q

theorem String.Pos.prev_eq_iff {s : String} {p q : s.Pos} {h : p ≠ s.startPos} : p.prev h = q ↔ q < p ∧ ∀ (q' : s.Pos), q' < p → q' ≤ q

@[simp]

theorem String.Pos.prev_lt {s : String} {p : s.Pos} {h : p ≠ s.startPos} : p.prev h < p

@[simp]

theorem String.Pos.prev_le {s : String} {p : s.Pos} {h : p ≠ s.startPos} : p.prev h ≤ p

@[simp]

theorem String.Pos.prev_ne_endPos {s : String} {p : s.Pos} {h : p ≠ s.startPos} : p.prev h ≠ s.endPos

theorem String.Pos.toSlice_prev {s : String} {p : s.Pos} {h : p ≠ s.startPos} : (p.prev h).toSlice = p.toSlice.prev ⋯

theorem String.Pos.ofToSlice_prev {s : String} {p : s.toSlice.Pos} {h : p ≠ s.toSlice.startPos} : ofToSlice (p.prev h) = (ofToSlice p).prev ⋯

theorem String.Pos.prev_toSlice {s : String} {p : s.Pos} {h : p.toSlice ≠ s.toSlice.startPos} : p.toSlice.prev h = (p.prev ⋯).toSlice

theorem String.Pos.prev_ofToSlice {s : String} {p : s.toSlice.Pos} {h : ofToSlice p ≠ s.startPos} : (ofToSlice p).prev h = ofToSlice (p.prev ⋯)

theorem String.Pos.prevn_le {s : String} {p : s.Pos} {n : Nat} : p.prevn n ≤ p

theorem String.Pos.ofSliceTo_prev {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h : p ≠ (s.sliceTo p₀).startPos} : ofSliceTo (p.prev h) = (ofSliceTo p).prev ⋯

theorem String.Pos.prev_ofSliceTo {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h : ofSliceTo p ≠ s.startPos} : (ofSliceTo p).prev h = ofSliceTo (p.prev ⋯)

theorem String.Pos.ofSliceFrom_prev {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h : p ≠ (s.sliceFrom p₀).startPos} : ofSliceFrom (p.prev h) = (ofSliceFrom p).prev ⋯

theorem String.Pos.ofSlice_prev {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {h' : p ≠ (s.slice p₀ p₁ h).startPos} : ofSlice (p.prev h') = (ofSlice p).prev ⋯

@[simp]

theorem String.Pos.prev_next {s : String} {p : s.Pos} {h : p ≠ s.endPos} : (p.next h).prev ⋯ = p

@[simp]

theorem String.Pos.next_prev {s : String} {p : s.Pos} {h : p ≠ s.startPos} : (p.prev h).next ⋯ = p

theorem String.Pos.prev?_eq_prev?_toSlice {s : String} {p : s.Pos} : p.prev? = Option.map ofToSlice p.toSlice.prev?

theorem String.Pos.prev?_toSlice {s : String} {p : s.Pos} : p.toSlice.prev? = Option.map toSlice p.prev?

theorem String.Pos.prev?_eq_dif {s : String} {p : s.Pos} : p.prev? = if h : p = s.startPos then none else some (p.prev h)

theorem String.Pos.prev?_eq_some_prev {s : String} {p : s.Pos} (h : p ≠ s.startPos) : p.prev? = some (p.prev h)

@[simp]

theorem String.Pos.prev?_eq_none_iff {s : String} {p : s.Pos} : p.prev? = none ↔ p = s.startPos

theorem String.Pos.prev?_eq_none {s : String} {p : s.Pos} (h : p = s.startPos) : p.prev? = none

@[simp]

theorem String.Pos.prev?_startPos {s : String} : s.startPos.prev? = none

@[simp]

theorem String.Slice.Pos.prevn_zero {s : Slice} {p : s.Pos} : p.prevn 0 = p

theorem String.Slice.Pos.prevn_add_one {n : Nat} {s : Slice} {p : s.Pos} : p.prevn (n + 1) = if h : p = s.startPos then p else (p.prev h).prevn n

@[simp]

theorem String.Slice.Pos.prevn_startPos {n : Nat} {s : Slice} : s.startPos.prevn n = s.startPos

theorem String.Pos.prevn_eq_prevn_toSlice {n : Nat} {s : String} {p : s.Pos} : p.prevn n = ofToSlice (p.toSlice.prevn n)

@[simp]

theorem String.Pos.prevn_zero {s : String} {p : s.Pos} : p.prevn 0 = p

theorem String.Pos.prevn_add_one {n : Nat} {s : String} {p : s.Pos} : p.prevn (n + 1) = if h : p = s.startPos then p else (p.prev h).prevn n

theorem String.Pos.prevn_toSlice {n : Nat} {s : String} {p : s.Pos} : p.toSlice.prevn n = (p.prevn n).toSlice

theorem String.Pos.toSlice_prevn {n : Nat} {s : String} {p : s.Pos} : (p.prevn n).toSlice = p.toSlice.prevn n

@[simp]

theorem String.Pos.prevn_startPos {n : Nat} {s : String} : s.startPos.prevn n = s.startPos