s : String
i : Pos
c : Char
h : ¬atEnd s i = true
this : (endPos (set s i c)).byteIdx - (next (set s i c) i).byteIdx = (endPos s).byteIdx - (next s i).byteIdx
⊢ (endPos s).byteIdx - (next s i).byteIdx < (endPos s).byteIdx - i.byteIdx
s : String
i : Pos
c : Char
h : ¬atEnd s i = true
this : (endPos (set s i c)).byteIdx - (next (set s i c) i).byteIdx = (endPos s).byteIdx - (next s i).byteIdx
⊢ (endPos (set s i c)).byteIdx - (next (set s i c) i).byteIdx < (endPos s).byteIdx - i.byteIdx
rw [this]
no goals
s : String
i : Pos
c : Char
h : ¬atEnd s i = true
this : (endPos (set s i c)).byteIdx - (next (set s i c) i).byteIdx = (endPos s).byteIdx - (next s i).byteIdx
⊢ (endPos s).byteIdx - (next s i).byteIdx < (endPos s).byteIdx - i.byteIdx
apply Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (lt_next ..)
s : String
i : Pos
c : Char
h✝ : ¬atEnd s i = true
h : (endPos s).byteIdx < (next s i).byteIdx
k : Nat
e : Nat.succ (endPos s).byteIdx + k = (next s i).byteIdx
⊢ (fun x => (endPos (set s i c)).byteIdx - (next (set s i c) i).byteIdx = x) 0
s : String
i : Pos
c : Char
h✝ : ¬atEnd s i = true
h : (endPos s).byteIdx < (next s i).byteIdx
⊢ (fun x => (endPos (set s i c)).byteIdx - (next (set s i c) i).byteIdx = x) 0
have ⟨k, e⟩ := Nat.le.dest h
s : String
i : Pos
c : Char
h✝ : ¬atEnd s i = true
h : (endPos s).byteIdx < (next s i).byteIdx
k : Nat
e : Nat.succ ((endPos s).byteIdx + k) = (next s i).byteIdx
⊢ (fun x => (endPos (set s i c)).byteIdx - (next (set s i c) i).byteIdx = x) 0
s : String
i : Pos
c : Char
h✝ : ¬atEnd s i = true
h : (endPos s).byteIdx < (next s i).byteIdx
k : Nat
e : Nat.succ (endPos s).byteIdx + k = (next s i).byteIdx
⊢ (fun x => (endPos (set s i c)).byteIdx - (next (set s i c) i).byteIdx = x) 0
rw [Nat.succ_add] at e
s : String
i : Pos
c : Char
h✝ : ¬atEnd s i = true
h : (endPos s).byteIdx < (next s i).byteIdx
k : Nat
e : Nat.succ ((endPos s).byteIdx + k) = (next s i).byteIdx
this : (next (set s i c) i).byteIdx = (endPos (set s i c)).byteIdx + Nat.succ k
⊢ (fun x => (endPos (set s i c)).byteIdx - (next (set s i c) i).byteIdx = x) 0
s : String
i : Pos
c : Char
h✝ : ¬atEnd s i = true
h : (endPos s).byteIdx < (next s i).byteIdx
k : Nat
e : Nat.succ ((endPos s).byteIdx + k) = (next s i).byteIdx
⊢ (fun x => (endPos (set s i c)).byteIdx - (next (set s i c) i).byteIdx = x) 0
have : ((s.set i c).next i).1 = _ := set_next_add _ _ c 0 k.succ e.symm
no goals
s : String
i : Pos
c : Char
h✝ : ¬atEnd s i = true
h : (endPos s).byteIdx < (next s i).byteIdx
k : Nat
e : Nat.succ ((endPos s).byteIdx + k) = (next s i).byteIdx
this : (next (set s i c) i).byteIdx = (endPos (set s i c)).byteIdx + Nat.succ k
⊢ (fun x => (endPos (set s i c)).byteIdx - (next (set s i c) i).byteIdx = x) 0
exact Nat.sub_eq_zero_of_le (this ▸ Nat.le_add_right ..)