l m₁ : List Char
c : Char
m₂ r : List Char
⊢ (if
        { byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ } =
          { byteIdx := utf8Len l + (utf8Len m₁ + (utf8Len m₂ + csize c)) } then
      { byteIdx := utf8Len m₁ }
    else
      {
        byteIdx :=
          (String.next { data := l ++ (m₁ ++ c :: (m₂ ++ r)) }
                ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx -
            utf8Len l }) =
    { byteIdx := utf8Len m₁ + csize c }
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ Substring.next
      { str := { data := l ++ (m₁ ++ c :: m₂) ++ r }, startPos := { byteIdx := utf8Len l },
        stopPos := { byteIdx := utf8Len l + utf8Len (m₁ ++ c :: m₂) } }
      { byteIdx := utf8Len m₁ } =
    { byteIdx := utf8Len m₁ + csize c }
simp [Substring.next]
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ {
      byteIdx :=
        (String.next { data := l ++ (m₁ ++ c :: (m₂ ++ r)) }
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx -
          utf8Len l } =
    { byteIdx := utf8Len m₁ + csize c }

case a
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ ¬({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ }).byteIdx =
      { byteIdx := utf8Len l + (utf8Len m₁ + (utf8Len m₂ + csize c)) }.byteIdx
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ (if
        { byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ } =
          { byteIdx := utf8Len l + (utf8Len m₁ + (utf8Len m₂ + csize c)) } then
      { byteIdx := utf8Len m₁ }
    else
      {
        byteIdx :=
          (String.next { data := l ++ (m₁ ++ c :: (m₂ ++ r)) }
                ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx -
            utf8Len l }) =
    { byteIdx := utf8Len m₁ + csize c }
rw [if_neg (mt Pos.ext_iff.1 ?a)]
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ {
      byteIdx :=
        (String.next { data := l ++ (m₁ ++ c :: (m₂ ++ r)) }
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx -
          utf8Len l } =
    { byteIdx := utf8Len m₁ + csize c }
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ {
      byteIdx :=
        (String.next { data := l ++ (m₁ ++ c :: (m₂ ++ r)) }
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx -
          utf8Len l } =
    { byteIdx := utf8Len m₁ + csize c }

case a
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ ¬({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ }).byteIdx =
      { byteIdx := utf8Len l + (utf8Len m₁ + (utf8Len m₂ + csize c)) }.byteIdx
case a =>
  simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using
    @ne_add_csize_add_self (utf8Len l + utf8Len m₁) (utf8Len m₂) c
l m₁ : List Char
c : Char
m₂ r : List Char
this :
  String.next { data := l ++ m₁ ++ c :: (m₂ ++ r) } { byteIdx := utf8Len (l ++ m₁) } =
    { byteIdx := utf8Len (l ++ m₁) + csize c }
⊢ {
      byteIdx :=
        (String.next { data := l ++ (m₁ ++ c :: (m₂ ++ r)) }
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx -
          utf8Len l } =
    { byteIdx := utf8Len m₁ + csize c }
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ {
      byteIdx :=
        (String.next { data := l ++ (m₁ ++ c :: (m₂ ++ r)) }
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx -
          utf8Len l } =
    { byteIdx := utf8Len m₁ + csize c }
have := next_of_valid (l ++ m₁) c (m₂ ++ r)
l m₁ : List Char
c : Char
m₂ r : List Char
this :
  String.next { data := l ++ (m₁ ++ c :: (m₂ ++ r)) } { byteIdx := utf8Len l + utf8Len m₁ } =
    { byteIdx := utf8Len l + utf8Len m₁ + csize c }
⊢ {
      byteIdx :=
        (String.next { data := l ++ (m₁ ++ c :: (m₂ ++ r)) } { byteIdx := utf8Len l + utf8Len m₁ }).byteIdx -
          utf8Len l } =
    { byteIdx := utf8Len m₁ + csize c }
l m₁ : List Char
c : Char
m₂ r : List Char
this :
  String.next { data := l ++ m₁ ++ c :: (m₂ ++ r) } { byteIdx := utf8Len (l ++ m₁) } =
    { byteIdx := utf8Len (l ++ m₁) + csize c }
⊢ {
      byteIdx :=
        (String.next { data := l ++ (m₁ ++ c :: (m₂ ++ r)) }
              ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx -
          utf8Len l } =
    { byteIdx := utf8Len m₁ + csize c }
simp [Pos.add_eq] at this ⊢
l m₁ : List Char
c : Char
m₂ r : List Char
this :
  String.next { data := l ++ (m₁ ++ c :: (m₂ ++ r)) } { byteIdx := utf8Len l + utf8Len m₁ } =
    { byteIdx := utf8Len l + utf8Len m₁ + csize c }
⊢ { byteIdx := { byteIdx := utf8Len l + utf8Len m₁ + csize c }.byteIdx - utf8Len l } =
    { byteIdx := utf8Len m₁ + csize c }
l m₁ : List Char
c : Char
m₂ r : List Char
this :
  String.next { data := l ++ (m₁ ++ c :: (m₂ ++ r)) } { byteIdx := utf8Len l + utf8Len m₁ } =
    { byteIdx := utf8Len l + utf8Len m₁ + csize c }
⊢ {
      byteIdx :=
        (String.next { data := l ++ (m₁ ++ c :: (m₂ ++ r)) } { byteIdx := utf8Len l + utf8Len m₁ }).byteIdx -
          utf8Len l } =
    { byteIdx := utf8Len m₁ + csize c }
rw [this]
no goals
l m₁ : List Char
c : Char
m₂ r : List Char
this :
  String.next { data := l ++ (m₁ ++ c :: (m₂ ++ r)) } { byteIdx := utf8Len l + utf8Len m₁ } =
    { byteIdx := utf8Len l + utf8Len m₁ + csize c }
⊢ { byteIdx := { byteIdx := utf8Len l + utf8Len m₁ + csize c }.byteIdx - utf8Len l } =
    { byteIdx := utf8Len m₁ + csize c }
simp [Nat.add_assoc, Nat.add_sub_cancel_left]
no goals
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ ¬({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ }).byteIdx =
      { byteIdx := utf8Len l + (utf8Len m₁ + (utf8Len m₂ + csize c)) }.byteIdx
simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using
  @ne_add_csize_add_self (utf8Len l + utf8Len m₁) (utf8Len m₂) c