-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem offsetOfPosAux_of_valid : ∀ l m r n,
    offsetOfPosAux ⟨l ++ m ++ r⟩ ⟨utf8Len l + utf8Len m⟩ ⟨utf8Len l⟩ n = n + m.length
  | l, [], r, n => by unfold offsetOfPosAux; simp
  | l, c::m, r, n => by
    unfold offsetOfPosAux
    rw [if_neg (by exact Nat.not_le.2 (Nat.lt_add_of_pos_right add_utf8Size_pos))]
    simp only [List.append_assoc, atEnd_of_valid l (c::m++r)]
    simp only [List.cons_append, utf8Len_cons, next_of_valid l c (m ++ r)]
    simpa [← Nat.add_assoc, Nat.add_right_comm] using
      offsetOfPosAux_of_valid (l++[c]) m r (n + 1)

Proof state:
l r : List Char
n : Nat
⊢ (if { byteIdx := utf8Len l } ≥ { byteIdx := utf8Len l + utf8Len [] } then n
    else
      if h : { data := l ++ [] ++ r }.atEnd { byteIdx := utf8Len l } = true then n
      else
        let_fun this := ⋯;
        { data := l ++ [] ++ r }.offsetOfPosAux { byteIdx := utf8Len l + utf8Len [] }
          ({ data := l ++ [] ++ r }.next { byteIdx := utf8Len l }) (n + 1)) =
    n + [].length

Tactic:
simp

Result:
no goals

Proof state:
l r : List Char
n : Nat
⊢ { data := l ++ [] ++ r }.offsetOfPosAux { byteIdx := utf8Len l + utf8Len [] } { byteIdx := utf8Len l } n =
    n + [].length

Tactic:
unfold offsetOfPosAux

Result:
l r : List Char
n : Nat
⊢ (if { byteIdx := utf8Len l } ≥ { byteIdx := utf8Len l + utf8Len [] } then n
    else
      if h : { data := l ++ [] ++ r }.atEnd { byteIdx := utf8Len l } = true then n
      else
        let_fun this := ⋯;
        { data := l ++ [] ++ r }.offsetOfPosAux { byteIdx := utf8Len l + utf8Len [] }
          ({ data := l ++ [] ++ r }.next { byteIdx := utf8Len l }) (n + 1)) =
    n + [].length

Proof state:
l : List Char
c : Char
m r : List Char
n : Nat
⊢ ¬{ byteIdx := utf8Len l } ≥ { byteIdx := utf8Len l + utf8Len (c :: m) }

Tactic:
exact Nat.not_le.2 (Nat.lt_add_of_pos_right add_utf8Size_pos)

Result:
no goals

Proof state:
l : List Char
c : Char
m r : List Char
n : Nat
⊢ { data := l ++ c :: m ++ r }.offsetOfPosAux { byteIdx := utf8Len l + utf8Len (c :: m) } { byteIdx := utf8Len l } n =
    n + (c :: m).length

Tactic:
unfold offsetOfPosAux

Result:
l : List Char
c : Char
m r : List Char
n : Nat
⊢ (if { byteIdx := utf8Len l } ≥ { byteIdx := utf8Len l + utf8Len (c :: m) } then n
    else
      if h : { data := l ++ c :: m ++ r }.atEnd { byteIdx := utf8Len l } = true then n
      else
        let_fun this := ⋯;
        { data := l ++ c :: m ++ r }.offsetOfPosAux { byteIdx := utf8Len l + utf8Len (c :: m) }
          ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l }) (n + 1)) =
    n + (c :: m).length

Proof state:
l : List Char
c : Char
m r : List Char
n : Nat
⊢ (if h : { data := l ++ c :: m ++ r }.atEnd { byteIdx := utf8Len l } = true then n
    else
      let_fun this := ⋯;
      { data := l ++ c :: m ++ r }.offsetOfPosAux { byteIdx := utf8Len l + utf8Len (c :: m) }
        ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l }) (n + 1)) =
    n + (c :: m).length

Tactic:
simp only [List.append_assoc, atEnd_of_valid l (c::m++r)]

Result:
l : List Char
c : Char
m r : List Char
n : Nat
⊢ (if h : c :: m ++ r = [] then n
    else
      { data := l ++ (c :: m ++ r) }.offsetOfPosAux { byteIdx := utf8Len l + utf8Len (c :: m) }
        ({ data := l ++ (c :: m ++ r) }.next { byteIdx := utf8Len l }) (n + 1)) =
    n + (c :: m).length

Proof state:
l : List Char
c : Char
m r : List Char
n : Nat
⊢ (if h : c :: m ++ r = [] then n
    else
      { data := l ++ (c :: m ++ r) }.offsetOfPosAux { byteIdx := utf8Len l + utf8Len (c :: m) }
        ({ data := l ++ (c :: m ++ r) }.next { byteIdx := utf8Len l }) (n + 1)) =
    n + (c :: m).length

Tactic:
simp only [List.cons_append, utf8Len_cons, next_of_valid l c (m ++ r)]

Result:
l : List Char
c : Char
m r : List Char
n : Nat
⊢ (if h : c :: (m ++ r) = [] then n
    else
      { data := l ++ c :: (m ++ r) }.offsetOfPosAux { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) }
        { byteIdx := utf8Len l + c.utf8Size } (n + 1)) =
    n + (c :: m).length

Proof state:
l : List Char
c : Char
m r : List Char
n : Nat
⊢ (if h : c :: (m ++ r) = [] then n
    else
      { data := l ++ c :: (m ++ r) }.offsetOfPosAux { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) }
        { byteIdx := utf8Len l + c.utf8Size } (n + 1)) =
    n + (c :: m).length

Tactic:
simpa [← Nat.add_assoc, Nat.add_right_comm] using
  offsetOfPosAux_of_valid (l++[c]) m r (n + 1)

Result:
no goals

Proof state:
l : List Char
c : Char
m r : List Char
n : Nat
⊢ (if { byteIdx := utf8Len l } ≥ { byteIdx := utf8Len l + utf8Len (c :: m) } then n
    else
      if h : { data := l ++ c :: m ++ r }.atEnd { byteIdx := utf8Len l } = true then n
      else
        let_fun this := ⋯;
        { data := l ++ c :: m ++ r }.offsetOfPosAux { byteIdx := utf8Len l + utf8Len (c :: m) }
          ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l }) (n + 1)) =
    n + (c :: m).length

Tactic:
rw [if_neg (by exact Nat.not_le.2 (Nat.lt_add_of_pos_right add_utf8Size_pos))]

Result:
l : List Char
c : Char
m r : List Char
n : Nat
⊢ (if h : { data := l ++ c :: m ++ r }.atEnd { byteIdx := utf8Len l } = true then n
    else
      let_fun this := ⋯;
      { data := l ++ c :: m ++ r }.offsetOfPosAux { byteIdx := utf8Len l + utf8Len (c :: m) }
        ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l }) (n + 1)) =
    n + (c :: m).length