-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem mapAux_lemma (s : String) (i : Pos) (c : Char) (h : ¬s.atEnd i) :
    (s.set i c).endPos.1 - ((s.set i c).next i).1 < s.endPos.1 - i.1 :=
  suffices (s.set i c).endPos.1 - ((s.set i c).next i).1 = s.endPos.1 - (s.next i).1 by
    rw [this]
    apply Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (lt_next ..)
  Nat.sub.elim (motive := (_ = ·)) _ _
    (fun _ k e =>
      have := set_next_add _ _ _ k 0 e.symm
      Nat.sub_eq_of_eq_add <| this.symm.trans <| Nat.add_comm ..)
    (fun h => by
      have ⟨k, e⟩ := Nat.le.dest h
      rw [Nat.succ_add] at e
      have : ((s.set i c).next i).1 = _ := set_next_add _ _ c 0 k.succ e.symm
      exact Nat.sub_eq_zero_of_le (this ▸ Nat.le_add_right ..))

Proof state:
s : String
i : Pos
c : Char
h : ¬s.atEnd i = true
this : (s.set i c).endPos.byteIdx - ((s.set i c).next i).byteIdx = s.endPos.byteIdx - (s.next i).byteIdx
⊢ s.endPos.byteIdx - (s.next i).byteIdx < s.endPos.byteIdx - i.byteIdx

Tactic:
apply Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (lt_next ..)

Result:
no goals

Proof state:
s : String
i : Pos
c : Char
h✝ : ¬s.atEnd i = true
h : s.endPos.byteIdx < (s.next i).byteIdx
k : Nat
e : (s.endPos.byteIdx + k).succ = (s.next i).byteIdx
⊢ (fun x => (s.set i c).endPos.byteIdx - ((s.set i c).next i).byteIdx = x) 0

Tactic:
have : ((s.set i c).next i).1 = _ := set_next_add _ _ c 0 k.succ e.symm

Result:
s : String
i : Pos
c : Char
h✝ : ¬s.atEnd i = true
h : s.endPos.byteIdx < (s.next i).byteIdx
k : Nat
e : (s.endPos.byteIdx + k).succ = (s.next i).byteIdx
this : ((s.set i c).next i).byteIdx = (s.set i c).endPos.byteIdx + k.succ
⊢ (fun x => (s.set i c).endPos.byteIdx - ((s.set i c).next i).byteIdx = x) 0

Proof state:
s : String
i : Pos
c : Char
h✝ : ¬s.atEnd i = true
h : s.endPos.byteIdx < (s.next i).byteIdx
k : Nat
e : s.endPos.byteIdx.succ + k = (s.next i).byteIdx
⊢ (fun x => (s.set i c).endPos.byteIdx - ((s.set i c).next i).byteIdx = x) 0

Tactic:
rw [Nat.succ_add] at e

Result:
s : String
i : Pos
c : Char
h✝ : ¬s.atEnd i = true
h : s.endPos.byteIdx < (s.next i).byteIdx
k : Nat
e : (s.endPos.byteIdx + k).succ = (s.next i).byteIdx
⊢ (fun x => (s.set i c).endPos.byteIdx - ((s.set i c).next i).byteIdx = x) 0

Proof state:
s : String
i : Pos
c : Char
h✝ : ¬s.atEnd i = true
h : s.endPos.byteIdx < (s.next i).byteIdx
k : Nat
e : (s.endPos.byteIdx + k).succ = (s.next i).byteIdx
this : ((s.set i c).next i).byteIdx = (s.set i c).endPos.byteIdx + k.succ
⊢ (fun x => (s.set i c).endPos.byteIdx - ((s.set i c).next i).byteIdx = x) 0

Tactic:
exact Nat.sub_eq_zero_of_le (this ▸ Nat.le_add_right ..)

Result:
no goals

Proof state:
s : String
i : Pos
c : Char
h : ¬s.atEnd i = true
this : (s.set i c).endPos.byteIdx - ((s.set i c).next i).byteIdx = s.endPos.byteIdx - (s.next i).byteIdx
⊢ (s.set i c).endPos.byteIdx - ((s.set i c).next i).byteIdx < s.endPos.byteIdx - i.byteIdx

Tactic:
rw [this]

Result:
s : String
i : Pos
c : Char
h : ¬s.atEnd i = true
this : (s.set i c).endPos.byteIdx - ((s.set i c).next i).byteIdx = s.endPos.byteIdx - (s.next i).byteIdx
⊢ s.endPos.byteIdx - (s.next i).byteIdx < s.endPos.byteIdx - i.byteIdx

Proof state:
s : String
i : Pos
c : Char
h✝ : ¬s.atEnd i = true
h : s.endPos.byteIdx < (s.next i).byteIdx
⊢ (fun x => (s.set i c).endPos.byteIdx - ((s.set i c).next i).byteIdx = x) 0

Tactic:
have ⟨k, e⟩ := Nat.le.dest h

Result:
s : String
i : Pos
c : Char
h✝ : ¬s.atEnd i = true
h : s.endPos.byteIdx < (s.next i).byteIdx
k : Nat
e : s.endPos.byteIdx.succ + k = (s.next i).byteIdx
⊢ (fun x => (s.set i c).endPos.byteIdx - ((s.set i c).next i).byteIdx = x) 0