α : Type u_1
f : α → Char → α
l r : List Char
a : α
⊢ (if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len [] } then
      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);
      foldlAux f { data := l ++ [] ++ r } { byteIdx := utf8Len l + utf8Len [] }
        (next { data := l ++ [] ++ r } { byteIdx := utf8Len l })
        (f a (get { data := l ++ [] ++ r } { byteIdx := utf8Len l }))
    else a) =
    List.foldl f a []
α : Type u_1
f : α → Char → α
l r : List Char
a : α
⊢ foldlAux f { data := l ++ [] ++ r } { byteIdx := utf8Len l + utf8Len [] } { byteIdx := utf8Len l } a =
    List.foldl f a []
unfold foldlAux
no goals
α : Type u_1
f : α → Char → α
l r : List Char
a : α
⊢ (if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len [] } then
      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);
      foldlAux f { data := l ++ [] ++ r } { byteIdx := utf8Len l + utf8Len [] }
        (next { data := l ++ [] ++ r } { byteIdx := utf8Len l })
        (f a (get { data := l ++ [] ++ r } { byteIdx := utf8Len l }))
    else a) =
    List.foldl f a []
simp
α : Type u_1
f : α → Char → α
l : List Char
c : Char
m r : List Char
a : α
⊢ (if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len (c :: m) } then
      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);
      foldlAux f { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) }
        (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })
        (f a (get { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }))
    else a) =
    List.foldl f a (c :: m)
α : Type u_1
f : α → Char → α
l : List Char
c : Char
m r : List Char
a : α
⊢ foldlAux f { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) } { byteIdx := utf8Len l } a =
    List.foldl f a (c :: m)
unfold foldlAux
α : Type u_1
f : α → Char → α
l : List Char
c : Char
m r : List Char
a : α
⊢ (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);
    foldlAux f { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) }
      (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })
      (f a (get { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }))) =
    List.foldl f a (c :: m)
α : Type u_1
f : α → Char → α
l : List Char
c : Char
m r : List Char
a : α
⊢ (if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len (c :: m) } then
      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);
      foldlAux f { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) }
        (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })
        (f a (get { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }))
    else a) =
    List.foldl f a (c :: m)
rw [dif_pos (by exact Nat.lt_add_of_pos_right add_csize_pos)]
α : Type u_1
f : α → Char → α
l : List Char
c : Char
m r : List Char
a : α
⊢ foldlAux f { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l + (utf8Len m + csize c) }
      { byteIdx := utf8Len l + csize c } (f a c) =
    List.foldl f (f a c) m
α : Type u_1
f : α → Char → α
l : List Char
c : Char
m r : List Char
a : α
⊢ (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);
    foldlAux f { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) }
      (next { data := l ++ c :: m ++ r } { byteIdx := utf8Len l })
      (f a (get { data := l ++ c :: m ++ r } { byteIdx := utf8Len l }))) =
    List.foldl f a (c :: m)
simp [by simpa using And.intro (get_of_valid l (c::(m++r))) (next_of_valid l c (m++r))]
no goals
α : Type u_1
f : α → Char → α
l : List Char
c : Char
m r : List Char
a : α
⊢ foldlAux f { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l + (utf8Len m + csize c) }
      { byteIdx := utf8Len l + csize c } (f a c) =
    List.foldl f (f a c) m
simpa [← Nat.add_assoc, Nat.add_right_comm] using foldlAux_of_valid f (l++[c]) m r (f a c)
no goals
α : Type u_1
f : α → Char → α
l : List Char
c : Char
m r : List Char
a : α
⊢ { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len (c :: m) }
exact Nat.lt_add_of_pos_right add_csize_pos
no goals
α : Type u_1
f : α → Char → α
l : List Char
c : Char
m r : List Char
a : α
⊢ ?m.165545
simpa using And.intro (get_of_valid l (c::(m++r))) (next_of_valid l c (m++r))