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 { byteIdx := utf8Len l }
      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);
        findAux { data := l ++ [] ++ r } p { byteIdx := utf8Len l + utf8Len [] }
          (next { data := l ++ [] ++ r } { byteIdx := utf8Len l })
    else { byteIdx := utf8Len l }) =
    { byteIdx := utf8Len l + utf8Len [] }
p : Char → Bool
l r : List Char
⊢ findAux { data := l ++ [] ++ r } p { byteIdx := utf8Len l + utf8Len [] } { byteIdx := utf8Len l } =
    { byteIdx := utf8Len l + utf8Len (List.takeWhile (fun x => !p x) []) }
unfold findAux List.takeWhile
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 { byteIdx := utf8Len l }
      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);
        findAux { data := l ++ [] ++ r } p { byteIdx := utf8Len l + utf8Len [] }
          (next { data := l ++ [] ++ r } { byteIdx := utf8Len l })
    else { byteIdx := utf8Len l }) =
    { byteIdx := utf8Len l + utf8Len [] }
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 { byteIdx := utf8Len l }
      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);
        findAux { data := l ++ c :: m ++ r } p { byteIdx := utf8Len l + utf8Len (c :: m) }
          (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })
    else { byteIdx := utf8Len l }) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match !p c with
            | true => c :: List.takeWhile (fun x => !p x) m
            | false => []) }
p : Char → Bool
l : List Char
c : Char
m r : List Char
⊢ findAux { data := l ++ c :: m ++ r } p { byteIdx := utf8Len l + utf8Len (c :: m) } { byteIdx := utf8Len l } =
    { byteIdx := utf8Len l + utf8Len (List.takeWhile (fun x => !p x) (c :: m)) }
unfold findAux List.takeWhile
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 { byteIdx := utf8Len l }
    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);
      findAux { data := l ++ c :: m ++ r } p { byteIdx := utf8Len l + utf8Len (c :: m) }
        (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match !p c with
            | true => c :: List.takeWhile (fun x => !p x) m
            | false => []) }
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 { byteIdx := utf8Len l }
      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);
        findAux { data := l ++ c :: m ++ r } p { byteIdx := utf8Len l + utf8Len (c :: m) }
          (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })
    else { byteIdx := utf8Len l }) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match !p c with
            | true => c :: List.takeWhile (fun x => !p x) m
            | false => []) }
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
h1 : get { data := l ++ (c :: m ++ r) } { byteIdx := utf8Len l } = List.headD (c :: m ++ r) default
⊢ (if p (get { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }) = true then { byteIdx := utf8Len l }
    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);
      findAux { data := l ++ c :: m ++ r } p { byteIdx := utf8Len l + utf8Len (c :: m) }
        (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match !p c with
            | true => c :: List.takeWhile (fun x => !p x) m
            | false => []) }
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 { byteIdx := utf8Len l }
    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);
      findAux { data := l ++ c :: m ++ r } p { byteIdx := utf8Len l + utf8Len (c :: m) }
        (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match !p c with
            | true => c :: List.takeWhile (fun x => !p x) m
            | false => []) }
have h1 := get_of_valid l (c::m++r)
p : Char → Bool
l : List Char
c : Char
m r : List Char
h1 : get { data := l ++ (c :: m ++ r) } { byteIdx := utf8Len l } = List.headD (c :: m ++ r) default
h2 : next { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = { byteIdx := utf8Len l + csize c }
⊢ (if p (get { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }) = true then { byteIdx := utf8Len l }
    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);
      findAux { data := l ++ c :: m ++ r } p { byteIdx := utf8Len l + utf8Len (c :: m) }
        (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match !p c with
            | true => c :: List.takeWhile (fun x => !p x) m
            | false => []) }
p : Char → Bool
l : List Char
c : Char
m r : List Char
h1 : get { data := l ++ (c :: m ++ r) } { byteIdx := utf8Len l } = List.headD (c :: m ++ r) default
⊢ (if p (get { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }) = true then { byteIdx := utf8Len l }
    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);
      findAux { data := l ++ c :: m ++ r } p { byteIdx := utf8Len l + utf8Len (c :: m) }
        (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match !p c with
            | true => c :: List.takeWhile (fun x => !p x) m
            | false => []) }
have h2 := next_of_valid l c (m++r)
p : Char → Bool
l : List Char
c : Char
m r : List Char
h1 : get { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = c
h2 : next { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = { byteIdx := utf8Len l + csize c }
⊢ (if p (get { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }) = true then { byteIdx := utf8Len l }
    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);
      findAux { data := l ++ c :: m ++ r } p { byteIdx := utf8Len l + utf8Len (c :: m) }
        (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match !p c with
            | true => c :: List.takeWhile (fun x => !p x) m
            | false => []) }
p : Char → Bool
l : List Char
c : Char
m r : List Char
h1 : get { data := l ++ (c :: m ++ r) } { byteIdx := utf8Len l } = List.headD (c :: m ++ r) default
h2 : next { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = { byteIdx := utf8Len l + csize c }
⊢ (if p (get { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }) = true then { byteIdx := utf8Len l }
    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);
      findAux { data := l ++ c :: m ++ r } p { byteIdx := utf8Len l + utf8Len (c :: m) }
        (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match !p c with
            | true => c :: List.takeWhile (fun x => !p x) m
            | false => []) }
simp at h1 h2
p : Char → Bool
l : List Char
c : Char
m r : List Char
h1 : get { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = c
h2 : next { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = { byteIdx := utf8Len l + csize c }
⊢ (if p c = true then { byteIdx := utf8Len l }
    else
      findAux { data := l ++ c :: (m ++ r) } p { byteIdx := utf8Len l + (utf8Len m + csize c) }
        { byteIdx := utf8Len l + csize c }) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match !p c with
            | true => c :: List.takeWhile (fun x => !p x) m
            | false => []) }
p : Char → Bool
l : List Char
c : Char
m r : List Char
h1 : get { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = c
h2 : next { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = { byteIdx := utf8Len l + csize c }
⊢ (if p (get { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }) = true then { byteIdx := utf8Len l }
    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);
      findAux { data := l ++ c :: m ++ r } p { byteIdx := utf8Len l + utf8Len (c :: m) }
        (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match !p c with
            | true => c :: List.takeWhile (fun x => !p x) m
            | false => []) }
simp [h1, h2]
case false
p : Char → Bool
l : List Char
c : Char
m r : List Char
h1 : get { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = c
h2 : next { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = { byteIdx := utf8Len l + csize c }
⊢ findAux { data := l ++ c :: (m ++ r) } p { byteIdx := utf8Len l + (utf8Len m + csize c) }
      { byteIdx := utf8Len l + csize c } =
    { byteIdx := utf8Len l + (utf8Len (List.takeWhile (fun x => !p x) m) + csize c) }
p : Char → Bool
l : List Char
c : Char
m r : List Char
h1 : get { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = c
h2 : next { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = { byteIdx := utf8Len l + csize c }
⊢ (if p c = true then { byteIdx := utf8Len l }
    else
      findAux { data := l ++ c :: (m ++ r) } p { byteIdx := utf8Len l + (utf8Len m + csize c) }
        { byteIdx := utf8Len l + csize c }) =
    {
      byteIdx :=
        utf8Len l +
          utf8Len
            (match !p c with
            | true => c :: List.takeWhile (fun x => !p x) m
            | false => []) }
cases p c <;> simp
case false
p : Char → Bool
l : List Char
c : Char
m r : List Char
h1 : get { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = c
h2 : next { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = { byteIdx := utf8Len l + csize c }
foo :
  findAux { data := l ++ [c] ++ m ++ r } p { byteIdx := utf8Len (l ++ [c]) + utf8Len m }
      { byteIdx := utf8Len (l ++ [c]) } =
    { byteIdx := utf8Len (l ++ [c]) + utf8Len (List.takeWhile (fun x => !p x) m) }
⊢ findAux { data := l ++ c :: (m ++ r) } p { byteIdx := utf8Len l + (utf8Len m + csize c) }
      { byteIdx := utf8Len l + csize c } =
    { byteIdx := utf8Len l + (utf8Len (List.takeWhile (fun x => !p x) m) + csize c) }
case false
p : Char → Bool
l : List Char
c : Char
m r : List Char
h1 : get { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = c
h2 : next { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = { byteIdx := utf8Len l + csize c }
⊢ findAux { data := l ++ c :: (m ++ r) } p { byteIdx := utf8Len l + (utf8Len m + csize c) }
      { byteIdx := utf8Len l + csize c } =
    { byteIdx := utf8Len l + (utf8Len (List.takeWhile (fun x => !p x) m) + csize c) }
have foo := findAux_of_valid p (l++[c]) m r
case false
p : Char → Bool
l : List Char
c : Char
m r : List Char
h1 : get { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = c
h2 : next { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = { byteIdx := utf8Len l + csize c }
foo :
  findAux { data := l ++ c :: (m ++ r) } p { byteIdx := utf8Len l + csize c + utf8Len m }
      { byteIdx := utf8Len l + csize c } =
    { byteIdx := utf8Len l + csize c + utf8Len (List.takeWhile (fun x => !p x) m) }
⊢ findAux { data := l ++ c :: (m ++ r) } p { byteIdx := utf8Len l + (utf8Len m + csize c) }
      { byteIdx := utf8Len l + csize c } =
    { byteIdx := utf8Len l + (utf8Len (List.takeWhile (fun x => !p x) m) + csize c) }
case false
p : Char → Bool
l : List Char
c : Char
m r : List Char
h1 : get { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = c
h2 : next { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = { byteIdx := utf8Len l + csize c }
foo :
  findAux { data := l ++ [c] ++ m ++ r } p { byteIdx := utf8Len (l ++ [c]) + utf8Len m }
      { byteIdx := utf8Len (l ++ [c]) } =
    { byteIdx := utf8Len (l ++ [c]) + utf8Len (List.takeWhile (fun x => !p x) m) }
⊢ findAux { data := l ++ c :: (m ++ r) } p { byteIdx := utf8Len l + (utf8Len m + csize c) }
      { byteIdx := utf8Len l + csize c } =
    { byteIdx := utf8Len l + (utf8Len (List.takeWhile (fun x => !p x) m) + csize c) }
simp at foo
case false
p : Char → Bool
l : List Char
c : Char
m r : List Char
h1 : get { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = c
h2 : next { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = { byteIdx := utf8Len l + csize c }
foo :
  findAux { data := l ++ c :: (m ++ r) } p { byteIdx := utf8Len l + (utf8Len m + csize c) }
      { byteIdx := utf8Len l + csize c } =
    { byteIdx := utf8Len l + csize c + utf8Len (List.takeWhile (fun x => !p x) m) }
⊢ findAux { data := l ++ c :: (m ++ r) } p { byteIdx := utf8Len l + (utf8Len m + csize c) }
      { byteIdx := utf8Len l + csize c } =
    { byteIdx := utf8Len l + (utf8Len (List.takeWhile (fun x => !p x) m) + csize c) }
case false
p : Char → Bool
l : List Char
c : Char
m r : List Char
h1 : get { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = c
h2 : next { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = { byteIdx := utf8Len l + csize c }
foo :
  findAux { data := l ++ c :: (m ++ r) } p { byteIdx := utf8Len l + csize c + utf8Len m }
      { byteIdx := utf8Len l + csize c } =
    { byteIdx := utf8Len l + csize c + utf8Len (List.takeWhile (fun x => !p x) m) }
⊢ findAux { data := l ++ c :: (m ++ r) } p { byteIdx := utf8Len l + (utf8Len m + csize c) }
      { byteIdx := utf8Len l + csize c } =
    { byteIdx := utf8Len l + (utf8Len (List.takeWhile (fun x => !p x) m) + csize c) }
rw [Nat.add_right_comm, Nat.add_assoc] at foo
no goals
case false
p : Char → Bool
l : List Char
c : Char
m r : List Char
h1 : get { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = c
h2 : next { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l } = { byteIdx := utf8Len l + csize c }
foo :
  findAux { data := l ++ c :: (m ++ r) } p { byteIdx := utf8Len l + (utf8Len m + csize c) }
      { byteIdx := utf8Len l + csize c } =
    { byteIdx := utf8Len l + csize c + utf8Len (List.takeWhile (fun x => !p x) m) }
⊢ findAux { data := l ++ c :: (m ++ r) } p { byteIdx := utf8Len l + (utf8Len m + csize c) }
      { byteIdx := utf8Len l + csize c } =
    { byteIdx := utf8Len l + (utf8Len (List.takeWhile (fun x => !p x) m) + csize c) }
rw [foo, Nat.add_right_comm, Nat.add_assoc]
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