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 },
      stopPos := { byteIdx := utf8Len l + utf8Len (List.takeWhile p m) } }
l m r : List Char
p : Char → Bool
⊢ ValidFor l (List.takeWhile p m) (List.dropWhile p m ++ r)
    (Substring.takeWhile
      { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
        stopPos := { byteIdx := utf8Len l + utf8Len m } }
      p)
simp only [Substring.takeWhile, takeWhileAux_of_valid]
case refine'_1
l m r : List Char
p : Char → Bool
⊢ m ++ r = List.takeWhile p m ++ (List.dropWhile p m ++ r)
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 },
      stopPos := { byteIdx := utf8Len l + utf8Len (List.takeWhile p m) } }
refine' .of_eq .. <;> simp
no goals
case refine'_1
l m r : List Char
p : Char → Bool
⊢ m ++ r = List.takeWhile p m ++ (List.dropWhile p m ++ r)
rw [← List.append_assoc, List.takeWhile_append_dropWhile]