-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem next : ∀ {s}, ValidFor l (m₁ ++ c :: m₂) r s →
    s.next ⟨utf8Len m₁⟩ = ⟨utf8Len m₁ + c.utf8Size⟩
  | _, ⟨⟩ => by
    simp only [Substring.next, utf8Len_append, utf8Len_cons, List.append_assoc, List.cons_append]
    rw [if_neg (mt Pos.ext_iff.1 ?a)]
    case a =>
      simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using
        @ne_add_utf8Size_add_self (utf8Len l + utf8Len m₁) (utf8Len m₂) c
    have := next_of_valid (l ++ m₁) c (m₂ ++ r)
    simp only [List.append_assoc, utf8Len_append, Pos.add_eq] at this ⊢; rw [this]
    simp [Nat.add_assoc, Nat.add_sub_cancel_left]

Proof state:
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ (if
        { byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ } =
          { byteIdx := utf8Len l + (utf8Len m₁ + (utf8Len m₂ + c.utf8Size)) } then
      { byteIdx := utf8Len m₁ }
    else
      {
        byteIdx :=
          ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next
                ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx -
            utf8Len l }) =
    { byteIdx := utf8Len m₁ + c.utf8Size }

Tactic:
rw [if_neg (mt Pos.ext_iff.1 ?a)]

Result:
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ {
      byteIdx :=
        ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx -
          utf8Len l } =
    { byteIdx := utf8Len m₁ + c.utf8Size }

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₂ + c.utf8Size)) }.byteIdx

Proof state:
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ ¬({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ }).byteIdx =
      { byteIdx := utf8Len l + (utf8Len m₁ + (utf8Len m₂ + c.utf8Size)) }.byteIdx

Tactic:
simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using
  @ne_add_utf8Size_add_self (utf8Len l + utf8Len m₁) (utf8Len m₂) c

Result:
no goals

Proof state:
l m₁ : List Char
c : Char
m₂ r : List Char
this :
  { data := l ++ m₁ ++ c :: (m₂ ++ r) }.next { byteIdx := utf8Len (l ++ m₁) } =
    { byteIdx := utf8Len (l ++ m₁) + c.utf8Size }
⊢ {
      byteIdx :=
        ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx -
          utf8Len l } =
    { byteIdx := utf8Len m₁ + c.utf8Size }

Tactic:
simp only [List.append_assoc, utf8Len_append, Pos.add_eq] at this ⊢

Result:
l m₁ : List Char
c : Char
m₂ r : List Char
this :
  { data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next { byteIdx := utf8Len l + utf8Len m₁ } =
    { byteIdx := utf8Len l + utf8Len m₁ + c.utf8Size }
⊢ {
      byteIdx :=
        ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next { byteIdx := utf8Len l + utf8Len m₁ }).byteIdx - utf8Len l } =
    { byteIdx := utf8Len m₁ + c.utf8Size }

Proof state:
l m₁ : List Char
c : Char
m₂ r : List Char
this :
  { data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next { byteIdx := utf8Len l + utf8Len m₁ } =
    { byteIdx := utf8Len l + utf8Len m₁ + c.utf8Size }
⊢ {
      byteIdx :=
        ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next { byteIdx := utf8Len l + utf8Len m₁ }).byteIdx - utf8Len l } =
    { byteIdx := utf8Len m₁ + c.utf8Size }

Tactic:
rw [this]

Result:
l m₁ : List Char
c : Char
m₂ r : List Char
this :
  { data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next { byteIdx := utf8Len l + utf8Len m₁ } =
    { byteIdx := utf8Len l + utf8Len m₁ + c.utf8Size }
⊢ { byteIdx := { byteIdx := utf8Len l + utf8Len m₁ + c.utf8Size }.byteIdx - utf8Len l } =
    { byteIdx := utf8Len m₁ + c.utf8Size }

Proof state:
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ { str := { data := l ++ (m₁ ++ c :: m₂) ++ r }, startPos := { byteIdx := utf8Len l },
          stopPos := { byteIdx := utf8Len l + utf8Len (m₁ ++ c :: m₂) } }.next
      { byteIdx := utf8Len m₁ } =
    { byteIdx := utf8Len m₁ + c.utf8Size }

Tactic:
simp only [Substring.next, utf8Len_append, utf8Len_cons, List.append_assoc, List.cons_append]

Result:
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ (if
        { byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ } =
          { byteIdx := utf8Len l + (utf8Len m₁ + (utf8Len m₂ + c.utf8Size)) } then
      { byteIdx := utf8Len m₁ }
    else
      {
        byteIdx :=
          ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next
                ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx -
            utf8Len l }) =
    { byteIdx := utf8Len m₁ + c.utf8Size }

Proof state:
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ {
      byteIdx :=
        ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx -
          utf8Len l } =
    { byteIdx := utf8Len m₁ + c.utf8Size }

Tactic:
have := next_of_valid (l ++ m₁) c (m₂ ++ r)

Result:
l m₁ : List Char
c : Char
m₂ r : List Char
this :
  { data := l ++ m₁ ++ c :: (m₂ ++ r) }.next { byteIdx := utf8Len (l ++ m₁) } =
    { byteIdx := utf8Len (l ++ m₁) + c.utf8Size }
⊢ {
      byteIdx :=
        ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx -
          utf8Len l } =
    { byteIdx := utf8Len m₁ + c.utf8Size }

Proof state:
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ {
      byteIdx :=
        ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx -
          utf8Len l } =
    { byteIdx := utf8Len m₁ + c.utf8Size }

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₂ + c.utf8Size)) }.byteIdx

Tactic:
case a =>
  simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using
    @ne_add_utf8Size_add_self (utf8Len l + utf8Len m₁) (utf8Len m₂) c

Result:
l m₁ : List Char
c : Char
m₂ r : List Char
⊢ {
      byteIdx :=
        ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx -
          utf8Len l } =
    { byteIdx := utf8Len m₁ + c.utf8Size }

Proof state:
l m₁ : List Char
c : Char
m₂ r : List Char
this :
  { data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next { byteIdx := utf8Len l + utf8Len m₁ } =
    { byteIdx := utf8Len l + utf8Len m₁ + c.utf8Size }
⊢ { byteIdx := { byteIdx := utf8Len l + utf8Len m₁ + c.utf8Size }.byteIdx - utf8Len l } =
    { byteIdx := utf8Len m₁ + c.utf8Size }

Tactic:
simp [Nat.add_assoc, Nat.add_sub_cancel_left]

Result:
no goals