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

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

@[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_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.prev_toSlice {s : String} {p : s.Pos} {h : p.toSlice ≠ s.toSlice.startPos} : p.toSlice.prev h = (p.prev ⋯).toSlice

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

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