p : Char → Bool
l r : List Char
⊢ (if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len [] } then
      if p (get { data := l ++ [] ++ r } { byteIdx := utf8Len l }) = true then true
      else
        let_fun this :=
          (_ :
            { byteIdx := utf8Len l + utf8Len [] }.byteIdx -
                (next { data := l ++ [] ++ r } { byteIdx := utf8Len l }).byteIdx <
              { byteIdx := utf8Len l + utf8Len [] }.byteIdx - { byteIdx := utf8Len l }.byteIdx);
        anyAux { data := l ++ [] ++ r } { byteIdx := utf8Len l + utf8Len [] } p
          (next { data := l ++ [] ++ r } { byteIdx := utf8Len l })
    else false) =
    List.any [] p
p : Char → Bool
l r : List Char
⊢ anyAux { data := l ++ [] ++ r } { byteIdx := utf8Len l + utf8Len [] } p { byteIdx := utf8Len l } = List.any [] p
unfold anyAux
no goals
p : Char → Bool
l r : List Char
⊢ (if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len [] } then
      if p (get { data := l ++ [] ++ r } { byteIdx := utf8Len l }) = true then true
      else
        let_fun this :=
          (_ :
            { byteIdx := utf8Len l + utf8Len [] }.byteIdx -
                (next { data := l ++ [] ++ r } { byteIdx := utf8Len l }).byteIdx <
              { byteIdx := utf8Len l + utf8Len [] }.byteIdx - { byteIdx := utf8Len l }.byteIdx);
        anyAux { data := l ++ [] ++ r } { byteIdx := utf8Len l + utf8Len [] } p
          (next { data := l ++ [] ++ r } { byteIdx := utf8Len l })
    else false) =
    List.any [] p
simp
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 (get { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }) = true then true
      else
        let_fun this :=
          (_ :
            { byteIdx := utf8Len l + utf8Len (c :: m) }.byteIdx -
                (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }).byteIdx <
              { byteIdx := utf8Len l + utf8Len (c :: m) }.byteIdx - { byteIdx := utf8Len l }.byteIdx);
        anyAux { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) } p
          (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })
    else false) =
    List.any (c :: m) p
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ anyAux { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) } p { byteIdx := utf8Len l } =
    List.any (c :: m) p
unfold anyAux
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ (if p (get { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }) = true then true
    else
      let_fun this :=
        (_ :
          { byteIdx := utf8Len l + utf8Len (c :: m) }.byteIdx -
              (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }).byteIdx <
            { byteIdx := utf8Len l + utf8Len (c :: m) }.byteIdx - { byteIdx := utf8Len l }.byteIdx);
      anyAux { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) } p
        (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })) =
    List.any (c :: m) p
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 (get { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }) = true then true
      else
        let_fun this :=
          (_ :
            { byteIdx := utf8Len l + utf8Len (c :: m) }.byteIdx -
                (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }).byteIdx <
              { byteIdx := utf8Len l + utf8Len (c :: m) }.byteIdx - { byteIdx := utf8Len l }.byteIdx);
        anyAux { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) } p
          (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })
    else false) =
    List.any (c :: m) p
rw [dif_pos (by exact Nat.lt_add_of_pos_right add_csize_pos)]
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ (if p c = true then true
    else
      anyAux { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l + (utf8Len m + csize c) } p
        { byteIdx := utf8Len l + csize c }) =
    (p c || List.any m p)
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ (if p (get { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }) = true then true
    else
      let_fun this :=
        (_ :
          { byteIdx := utf8Len l + utf8Len (c :: m) }.byteIdx -
              (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }).byteIdx <
            { byteIdx := utf8Len l + utf8Len (c :: m) }.byteIdx - { byteIdx := utf8Len l }.byteIdx);
      anyAux { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) } p
        (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })) =
    List.any (c :: m) p
simp [by simpa using And.intro (get_of_valid l (c::(m++r))) (next_of_valid l c (m++r))]
case false
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ anyAux { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l + (utf8Len m + csize c) } p
      { byteIdx := utf8Len l + csize c } =
    List.any m p
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ (if p c = true then true
    else
      anyAux { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l + (utf8Len m + csize c) } p
        { byteIdx := utf8Len l + csize c }) =
    (p c || List.any m p)
cases p c <;> simp
no goals
case false
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ anyAux { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l + (utf8Len m + csize c) } p
      { byteIdx := utf8Len l + csize c } =
    List.any m p
simpa [← Nat.add_assoc, Nat.add_right_comm] using anyAux_of_valid p (l++[c]) m r
no goals
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len (c :: m) }
exact Nat.lt_add_of_pos_right add_csize_pos
no goals
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ ?m.170578
simpa using And.intro (get_of_valid l (c::(m++r))) (next_of_valid l c (m++r))