l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
this :
  Substring.nextn { str := s.str, startPos := s.startPos, stopPos := s.stopPos } n { byteIdx := utf8Len [] } =
    { byteIdx := utf8Len [] + utf8Len (List.take n m) }
⊢ ValidFor (l ++ List.take n m) (List.drop n m) r (Substring.drop s n)
l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
⊢ ValidFor (l ++ List.take n m) (List.drop n m) r (Substring.drop s n)
have : Substring.nextn {..} .. = _ := h.nextn (m₁ := []) n
l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
this :
  Substring.nextn { str := s.str, startPos := s.startPos, stopPos := s.stopPos } n 0 =
    { byteIdx := utf8Len (List.take n m) }
⊢ ValidFor (l ++ List.take n m) (List.drop n m) r (Substring.drop s n)
l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
this :
  Substring.nextn { str := s.str, startPos := s.startPos, stopPos := s.stopPos } n { byteIdx := utf8Len [] } =
    { byteIdx := utf8Len [] + utf8Len (List.take n m) }
⊢ ValidFor (l ++ List.take n m) (List.drop n m) r (Substring.drop s n)
simp at this
l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
this :
  Substring.nextn { str := s.str, startPos := s.startPos, stopPos := s.stopPos } n 0 =
    { byteIdx := utf8Len (List.take n m) }
⊢ ValidFor (l ++ List.take n m) (List.drop n m) r
    { str := s.str, startPos := s.startPos + { byteIdx := utf8Len (List.take n m) }, stopPos := s.stopPos }
l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
this :
  Substring.nextn { str := s.str, startPos := s.startPos, stopPos := s.stopPos } n 0 =
    { byteIdx := utf8Len (List.take n m) }
⊢ ValidFor (l ++ List.take n m) (List.drop n m) r (Substring.drop s n)
simp [Substring.drop, this]
l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
this :
  Substring.nextn { str := s.str, startPos := s.startPos, stopPos := s.stopPos } n 0 =
    { byteIdx := utf8Len (List.take n m) }
⊢ ValidFor (l ++ List.take n m) (List.drop n m) r
    { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) },
      stopPos := { byteIdx := utf8Len l + utf8Len m } }
l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
this :
  Substring.nextn { str := s.str, startPos := s.startPos, stopPos := s.stopPos } n 0 =
    { byteIdx := utf8Len (List.take n m) }
⊢ ValidFor (l ++ List.take n m) (List.drop n m) r
    { str := s.str, startPos := s.startPos + { byteIdx := utf8Len (List.take n m) }, stopPos := s.stopPos }
simp [h.str, h.startPos, h.stopPos]
l m r : List Char
s : Substring
n : Nat
h : ValidFor l (List.take n m ++ List.drop n m) r s
this :
  Substring.nextn { str := s.str, startPos := s.startPos, stopPos := s.stopPos } n 0 =
    { byteIdx := utf8Len (List.take n m) }
⊢ ValidFor (l ++ List.take n m) (List.drop n m) r
    { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) },
      stopPos := { byteIdx := utf8Len l + utf8Len m } }
l m r : List Char
s : Substring
h : ValidFor l m r s
n : Nat
this :
  Substring.nextn { str := s.str, startPos := s.startPos, stopPos := s.stopPos } n 0 =
    { byteIdx := utf8Len (List.take n m) }
⊢ ValidFor (l ++ List.take n m) (List.drop n m) r
    { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) },
      stopPos := { byteIdx := utf8Len l + utf8Len m } }
rw [← List.take_append_drop n m] at h
l m r : List Char
s : Substring
n : Nat
h : ValidFor l (List.take n m ++ List.drop n m) r s
this :
  Substring.nextn { str := s.str, startPos := s.startPos, stopPos := s.stopPos } n 0 =
    { byteIdx := utf8Len (List.take n m) }
⊢ { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) },
          stopPos := { byteIdx := utf8Len l + utf8Len m } }.stopPos.byteIdx =
    utf8Len (l ++ List.take n m) + utf8Len (List.drop n m)
l m r : List Char
s : Substring
n : Nat
h : ValidFor l (List.take n m ++ List.drop n m) r s
this :
  Substring.nextn { str := s.str, startPos := s.startPos, stopPos := s.stopPos } n 0 =
    { byteIdx := utf8Len (List.take n m) }
⊢ ValidFor (l ++ List.take n m) (List.drop n m) r
    { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) },
      stopPos := { byteIdx := utf8Len l + utf8Len m } }
refine .of_eq _ (by simp) (by simp) ?_
l m r : List Char
s : Substring
n : Nat
h : ValidFor l (List.take n m ++ List.drop n m) r s
this :
  Substring.nextn { str := s.str, startPos := s.startPos, stopPos := s.stopPos } n 0 =
    { byteIdx := utf8Len (List.take n m) }
⊢ { str := { data := l ++ (List.take n m ++ List.drop n m ++ r) },
          startPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n (List.take n m ++ List.drop n m)) },
          stopPos := { byteIdx := utf8Len l + utf8Len (List.take n m ++ List.drop n m) } }.stopPos.byteIdx =
    utf8Len (l ++ List.take n m) + utf8Len (List.drop n m)
l m r : List Char
s : Substring
n : Nat
h : ValidFor l (List.take n m ++ List.drop n m) r s
this :
  Substring.nextn { str := s.str, startPos := s.startPos, stopPos := s.stopPos } n 0 =
    { byteIdx := utf8Len (List.take n m) }
⊢ { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) },
          stopPos := { byteIdx := utf8Len l + utf8Len m } }.stopPos.byteIdx =
    utf8Len (l ++ List.take n m) + utf8Len (List.drop n m)
conv => lhs; rw [← List.take_append_drop n m]
no goals
l m r : List Char
s : Substring
n : Nat
h : ValidFor l (List.take n m ++ List.drop n m) r s
this :
  Substring.nextn { str := s.str, startPos := s.startPos, stopPos := s.stopPos } n 0 =
    { byteIdx := utf8Len (List.take n m) }
⊢ { str := { data := l ++ (List.take n m ++ List.drop n m ++ r) },
          startPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n (List.take n m ++ List.drop n m)) },
          stopPos := { byteIdx := utf8Len l + utf8Len (List.take n m ++ List.drop n m) } }.stopPos.byteIdx =
    utf8Len (l ++ List.take n m) + utf8Len (List.drop n m)
simp [-List.take_append_drop, Nat.add_assoc]
no goals
l m r : List Char
s : Substring
n : Nat
h : ValidFor l (List.take n m ++ List.drop n m) r s
this :
  Substring.nextn { str := s.str, startPos := s.startPos, stopPos := s.stopPos } n 0 =
    { byteIdx := utf8Len (List.take n m) }
⊢ { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) },
          stopPos := { byteIdx := utf8Len l + utf8Len m } }.str.data =
    l ++ List.take n m ++ List.drop n m ++ r
simp
no goals
l m r : List Char
s : Substring
n : Nat
h : ValidFor l (List.take n m ++ List.drop n m) r s
this :
  Substring.nextn { str := s.str, startPos := s.startPos, stopPos := s.stopPos } n 0 =
    { byteIdx := utf8Len (List.take n m) }
⊢ { str := { data := l ++ (m ++ r) }, startPos := { byteIdx := utf8Len l } + { byteIdx := utf8Len (List.take n m) },
          stopPos := { byteIdx := utf8Len l + utf8Len m } }.startPos.byteIdx =
    utf8Len (l ++ List.take n m)
simp