-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem takeWhileAux_of_valid (p : Char → Bool) : ∀ l m r,
    Substring.takeWhileAux ⟨l ++ m ++ r⟩ ⟨utf8Len l + utf8Len m⟩ p ⟨utf8Len l⟩ =
      ⟨utf8Len l + utf8Len (m.takeWhile p)⟩
  | l, [], r => by unfold Substring.takeWhileAux List.takeWhile; simp
  | l, c::m, r => by
    unfold Substring.takeWhileAux List.takeWhile
    rw [dif_pos (by exact Nat.lt_add_of_pos_right add_utf8Size_pos)]
    simp only [List.append_assoc, List.cons_append, get_of_valid l (c :: (m ++ r)),
      Char.reduceDefault, List.headD_cons, utf8Len_cons, next_of_valid l c (m ++ r)]
    cases p c <;> simp
    simpa [← Nat.add_assoc, Nat.add_right_comm] using takeWhileAux_of_valid p (l++[c]) m r

Proof state:
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ Substring.takeWhileAux { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) } p
      { byteIdx := utf8Len l } =
    { byteIdx := utf8Len l + utf8Len (List.takeWhile p (c :: m)) }

Tactic:
unfold Substring.takeWhileAux List.takeWhile

Result:
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ (if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len (c :: m) } then
      if p ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }) = true then
        let_fun this := ⋯;
        Substring.takeWhileAux { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) } p
          ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l })
      else { byteIdx := utf8Len l }
    else { byteIdx := utf8Len l }) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match p c with
            | true => c :: List.takeWhile p m
            | false => []) }

Proof state:
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ (if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len (c :: m) } then
      if p ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }) = true then
        let_fun this := ⋯;
        Substring.takeWhileAux { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) } p
          ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l })
      else { byteIdx := utf8Len l }
    else { byteIdx := utf8Len l }) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match p c with
            | true => c :: List.takeWhile p m
            | false => []) }

Tactic:
rw [dif_pos (by exact Nat.lt_add_of_pos_right add_utf8Size_pos)]

Result:
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ (if p ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }) = true then
      let_fun this := ⋯;
      Substring.takeWhileAux { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) } p
        ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l })
    else { byteIdx := utf8Len l }) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match p c with
            | true => c :: List.takeWhile p m
            | false => []) }

Proof state:
p : Char → Bool
l r : List Char
⊢ (if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len [] } then
      if p ({ data := l ++ [] ++ r }.get { byteIdx := utf8Len l }) = true then
        let_fun this := ⋯;
        Substring.takeWhileAux { data := l ++ [] ++ r } { byteIdx := utf8Len l + utf8Len [] } p
          ({ data := l ++ [] ++ r }.next { byteIdx := utf8Len l })
      else { byteIdx := utf8Len l }
    else { byteIdx := utf8Len l }) =
    { byteIdx := utf8Len l + utf8Len [] }

Tactic:
simp

Result:
no goals

Proof state:
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ (if p c = true then
      Substring.takeWhileAux { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) } p
        { byteIdx := utf8Len l + c.utf8Size }
    else { byteIdx := utf8Len l }) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match p c with
            | true => c :: List.takeWhile p m
            | false => []) }

Tactic:
cases p c <;> simp

Result:
case true
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ Substring.takeWhileAux { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) } p
      { byteIdx := utf8Len l + c.utf8Size } =
    { byteIdx := utf8Len l + (utf8Len (List.takeWhile p m) + c.utf8Size) }

Proof state:
p : Char → Bool
l r : List Char
⊢ Substring.takeWhileAux { data := l ++ [] ++ r } { byteIdx := utf8Len l + utf8Len [] } p { byteIdx := utf8Len l } =
    { byteIdx := utf8Len l + utf8Len (List.takeWhile p []) }

Tactic:
unfold Substring.takeWhileAux List.takeWhile

Result:
p : Char → Bool
l r : List Char
⊢ (if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len [] } then
      if p ({ data := l ++ [] ++ r }.get { byteIdx := utf8Len l }) = true then
        let_fun this := ⋯;
        Substring.takeWhileAux { data := l ++ [] ++ r } { byteIdx := utf8Len l + utf8Len [] } p
          ({ data := l ++ [] ++ r }.next { byteIdx := utf8Len l })
      else { byteIdx := utf8Len l }
    else { byteIdx := utf8Len l }) =
    { byteIdx := utf8Len l + utf8Len [] }

Proof state:
case true
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ Substring.takeWhileAux { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) } p
      { byteIdx := utf8Len l + c.utf8Size } =
    { byteIdx := utf8Len l + (utf8Len (List.takeWhile p m) + c.utf8Size) }

Tactic:
simpa [← Nat.add_assoc, Nat.add_right_comm] using takeWhileAux_of_valid p (l++[c]) m r

Result:
no goals

Proof state:
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ (if p ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }) = true then
      let_fun this := ⋯;
      Substring.takeWhileAux { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) } p
        ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l })
    else { byteIdx := utf8Len l }) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match p c with
            | true => c :: List.takeWhile p m
            | false => []) }

Tactic:
simp only [List.append_assoc, List.cons_append, get_of_valid l (c :: (m ++ r)),
  Char.reduceDefault, List.headD_cons, utf8Len_cons, next_of_valid l c (m ++ r)]

Result:
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ (if p c = true then
      Substring.takeWhileAux { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) } p
        { byteIdx := utf8Len l + c.utf8Size }
    else { byteIdx := utf8Len l }) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match p c with
            | true => c :: List.takeWhile p m
            | false => []) }

Proof state:
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len (c :: m) }

Tactic:
exact Nat.lt_add_of_pos_right add_utf8Size_pos

Result:
no goals