l m r : List Char
p : Char → Bool
⊢ ValidFor (l ++ List.takeWhile p m) (List.dropWhile p m) r
    { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l + utf8Len (List.takeWhile p m) },
      stopPos := { byteIdx := utf8Len l + utf8Len m } }
l m r : List Char
p : Char → Bool
⊢ ValidFor (l ++ List.takeWhile p m) (List.dropWhile p m) r
    (Substring.dropWhile
      { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
        stopPos := { byteIdx := utf8Len l + utf8Len m } }
      p)
simp only [Substring.dropWhile, takeWhileAux_of_valid]
case refine'_3
l m r : List Char
p : Char → Bool
⊢ utf8Len l + utf8Len m = utf8Len l + utf8Len (List.takeWhile p m) + utf8Len (List.dropWhile p m)
l m r : List Char
p : Char → Bool
⊢ ValidFor (l ++ List.takeWhile p m) (List.dropWhile p m) r
    { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l + utf8Len (List.takeWhile p m) },
      stopPos := { byteIdx := utf8Len l + utf8Len m } }
refine' .of_eq .. <;> simp
no goals
case refine'_3
l m r : List Char
p : Char → Bool
⊢ utf8Len l + utf8Len m = utf8Len l + utf8Len (List.takeWhile p m) + utf8Len (List.dropWhile p m)
rw [Nat.add_assoc, ← utf8Len_append (m.takeWhile p), List.takeWhile_append_dropWhile]