-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem foldlAux_of_valid (f : α → Char → α) : ∀ l m r a,
    foldlAux f ⟨l ++ m ++ r⟩ ⟨utf8Len l + utf8Len m⟩ ⟨utf8Len l⟩ a = m.foldl f a
  | l, [], r, a => by unfold foldlAux; simp
  | l, c::m, r, a => by
    unfold foldlAux
    rw [dif_pos (by exact Nat.lt_add_of_pos_right add_utf8Size_pos)]
    simp only [List.append_assoc, List.cons_append, utf8Len_cons, next_of_valid l c (m ++ r),
      get_of_valid l (c :: (m ++ r)), Char.reduceDefault, List.headD_cons, List.foldl_cons]
    simpa [← Nat.add_assoc, Nat.add_right_comm] using foldlAux_of_valid f (l++[c]) m r (f a c)

Proof state:
α : 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 + c.utf8Size) }
      { byteIdx := utf8Len l + c.utf8Size } (f a c) =
    List.foldl f (f a c) m

Tactic:
simpa [← Nat.add_assoc, Nat.add_right_comm] using foldlAux_of_valid f (l++[c]) m r (f a c)

Result:
no goals

Proof state:
α : Type u_1
f : α → Char → α
l r : List Char
a : α
⊢ (if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len [] } then
      let_fun this := ⋯;
      foldlAux f { data := l ++ [] ++ r } { byteIdx := utf8Len l + utf8Len [] }
        ({ data := l ++ [] ++ r }.next { byteIdx := utf8Len l })
        (f a ({ data := l ++ [] ++ r }.get { byteIdx := utf8Len l }))
    else a) =
    List.foldl f a []

Tactic:
simp

Result:
no goals

Proof state:
α : 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 []

Tactic:
unfold foldlAux

Result:
α : Type u_1
f : α → Char → α
l r : List Char
a : α
⊢ (if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len [] } then
      let_fun this := ⋯;
      foldlAux f { data := l ++ [] ++ r } { byteIdx := utf8Len l + utf8Len [] }
        ({ data := l ++ [] ++ r }.next { byteIdx := utf8Len l })
        (f a ({ data := l ++ [] ++ r }.get { byteIdx := utf8Len l }))
    else a) =
    List.foldl f a []

Proof state:
α : Type u_1
f : α → Char → α
l : List Char
c : Char
m r : List Char
a : α
⊢ (let_fun this := ⋯;
    foldlAux f { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) }
      ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l })
      (f a ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }))) =
    List.foldl f a (c :: m)

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

Result:
α : 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 + c.utf8Size) }
      { byteIdx := utf8Len l + c.utf8Size } (f a c) =
    List.foldl f (f a c) m

Proof state:
α : 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 := ⋯;
      foldlAux f { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) }
        ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l })
        (f a ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }))
    else a) =
    List.foldl f a (c :: m)

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

Result:
α : Type u_1
f : α → Char → α
l : List Char
c : Char
m r : List Char
a : α
⊢ (let_fun this := ⋯;
    foldlAux f { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) }
      ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l })
      (f a ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }))) =
    List.foldl f a (c :: m)

Proof state:
α : 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)

Tactic:
unfold foldlAux

Result:
α : 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 := ⋯;
      foldlAux f { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) }
        ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l })
        (f a ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }))
    else a) =
    List.foldl f a (c :: m)

Proof state:
α : Type u_1
f : α → Char → α
l : List Char
c : Char
m r : List Char
a : α
⊢ { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len (c :: m) }

Tactic:
exact Nat.lt_add_of_pos_right add_utf8Size_pos

Result:
no goals