l r : List Char
n : Nat
⊢ (if { byteIdx := utf8Len l } ≥ { byteIdx := utf8Len l + utf8Len [] } then n
    else
      if h : atEnd { data := l ++ [] ++ r } { byteIdx := utf8Len l } = true then n
      else
        let_fun this :=
          (_ :
            utf8ByteSize { data := l ++ [] ++ r } - (next { data := l ++ [] ++ r } { byteIdx := utf8Len l }).byteIdx <
              utf8ByteSize { data := l ++ [] ++ r } - { byteIdx := utf8Len l }.byteIdx);
        offsetOfPosAux { data := l ++ [] ++ r } { byteIdx := utf8Len l + utf8Len [] }
          (next { data := l ++ [] ++ r } { byteIdx := utf8Len l }) (n + 1)) =
    n + List.length []
l r : List Char
n : Nat
⊢ offsetOfPosAux { data := l ++ [] ++ r } { byteIdx := utf8Len l + utf8Len [] } { byteIdx := utf8Len l } n =
    n + List.length []
unfold offsetOfPosAux
no goals
l r : List Char
n : Nat
⊢ (if { byteIdx := utf8Len l } ≥ { byteIdx := utf8Len l + utf8Len [] } then n
    else
      if h : atEnd { data := l ++ [] ++ r } { byteIdx := utf8Len l } = true then n
      else
        let_fun this :=
          (_ :
            utf8ByteSize { data := l ++ [] ++ r } - (next { data := l ++ [] ++ r } { byteIdx := utf8Len l }).byteIdx <
              utf8ByteSize { data := l ++ [] ++ r } - { byteIdx := utf8Len l }.byteIdx);
        offsetOfPosAux { data := l ++ [] ++ r } { byteIdx := utf8Len l + utf8Len [] }
          (next { data := l ++ [] ++ r } { byteIdx := utf8Len l }) (n + 1)) =
    n + List.length []
simp
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 : atEnd { data := l ++ c :: m ++ r } { byteIdx := utf8Len l } = true then n
      else
        let_fun this :=
          (_ :
            utf8ByteSize { data := l ++ c :: m ++ r } -
                (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }).byteIdx <
              utf8ByteSize { data := l ++ c :: m ++ r } - { byteIdx := utf8Len l }.byteIdx);
        offsetOfPosAux { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) }
          (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }) (n + 1)) =
    n + List.length (c :: m)
l : List Char
c : Char
m r : List Char
n : Nat
⊢ offsetOfPosAux { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) } { byteIdx := utf8Len l } n =
    n + List.length (c :: m)
unfold offsetOfPosAux
l : List Char
c : Char
m r : List Char
n : Nat
⊢ (if h : atEnd { data := l ++ c :: m ++ r } { byteIdx := utf8Len l } = true then n
    else
      let_fun this :=
        (_ :
          utf8ByteSize { data := l ++ c :: m ++ r } -
              (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }).byteIdx <
            utf8ByteSize { data := l ++ c :: m ++ r } - { byteIdx := utf8Len l }.byteIdx);
      offsetOfPosAux { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) }
        (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }) (n + 1)) =
    n + List.length (c :: m)
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 : atEnd { data := l ++ c :: m ++ r } { byteIdx := utf8Len l } = true then n
      else
        let_fun this :=
          (_ :
            utf8ByteSize { data := l ++ c :: m ++ r } -
                (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }).byteIdx <
              utf8ByteSize { data := l ++ c :: m ++ r } - { byteIdx := utf8Len l }.byteIdx);
        offsetOfPosAux { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) }
          (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }) (n + 1)) =
    n + List.length (c :: m)
rw [if_neg (by exact Nat.not_le.2 (Nat.lt_add_of_pos_right add_csize_pos))]
l : List Char
c : Char
m r : List Char
n : Nat
⊢ (if h : c :: m ++ r = [] then n
    else
      offsetOfPosAux { data := l ++ (c :: m ++ r) } { byteIdx := utf8Len l + utf8Len (c :: m) }
        (next { data := l ++ (c :: m ++ r) } { byteIdx := utf8Len l }) (n + 1)) =
    n + List.length (c :: m)
l : List Char
c : Char
m r : List Char
n : Nat
⊢ (if h : atEnd { data := l ++ c :: m ++ r } { byteIdx := utf8Len l } = true then n
    else
      let_fun this :=
        (_ :
          utf8ByteSize { data := l ++ c :: m ++ r } -
              (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }).byteIdx <
            utf8ByteSize { data := l ++ c :: m ++ r } - { byteIdx := utf8Len l }.byteIdx);
      offsetOfPosAux { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) }
        (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }) (n + 1)) =
    n + List.length (c :: m)
simp only [List.append_assoc, atEnd_of_valid l (c::m++r)]
l : List Char
c : Char
m r : List Char
n : Nat
⊢ offsetOfPosAux { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l + (utf8Len m + csize c) }
      { byteIdx := utf8Len l + csize c } (n + 1) =
    n + Nat.succ (List.length m)
l : List Char
c : Char
m r : List Char
n : Nat
⊢ (if h : c :: m ++ r = [] then n
    else
      offsetOfPosAux { data := l ++ (c :: m ++ r) } { byteIdx := utf8Len l + utf8Len (c :: m) }
        (next { data := l ++ (c :: m ++ r) } { byteIdx := utf8Len l }) (n + 1)) =
    n + List.length (c :: m)
simp [by simpa using next_of_valid l c (m++r)]
no goals
l : List Char
c : Char
m r : List Char
n : Nat
⊢ offsetOfPosAux { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l + (utf8Len m + csize c) }
      { byteIdx := utf8Len l + csize c } (n + 1) =
    n + Nat.succ (List.length m)
simpa [← Nat.add_assoc, Nat.add_right_comm, Nat.succ_eq_add_one] using
  offsetOfPosAux_of_valid (l++[c]) m r (n + 1)
no goals
l : List Char
c : Char
m r : List Char
n : Nat
⊢ ¬{ byteIdx := utf8Len l } ≥ { byteIdx := utf8Len l + utf8Len (c :: m) }
exact Nat.not_le.2 (Nat.lt_add_of_pos_right add_csize_pos)
no goals
l : List Char
c : Char
m r : List Char
n : Nat
⊢ ?m.163194
simpa using next_of_valid l c (m++r)