-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem foldrAux_of_valid (f : Char → α → α) (l m r a) :
    foldrAux f a ⟨l ++ m ++ r⟩ ⟨utf8Len l + utf8Len m⟩ ⟨utf8Len l⟩ = m.foldr f a

Proof state:
α : Type u_1
f : Char → α → α
l m✝ : List Char
c : Char
m : List Char
IH :
  ∀ (r : List Char) (a : α),
    foldrAux f a { data := l ++ m.reverse ++ r } { byteIdx := utf8Len l + utf8Len m.reverse } { byteIdx := utf8Len l } =
      List.foldr f a m.reverse
r : List Char
a : α
⊢ ?m.156416

Tactic:
simpa using get_of_valid (l ++ m.reverse) (c :: r)

Result:
no goals

Proof state:
case cons
α : Type u_1
f : Char → α → α
l m✝ : List Char
c : Char
m : List Char
IH :
  ∀ (r : List Char) (a : α),
    foldrAux f a { data := l ++ m.reverse ++ r } { byteIdx := utf8Len l + utf8Len m.reverse } { byteIdx := utf8Len l } =
      List.foldr f a m.reverse
r : List Char
a : α
⊢ (if 0 < utf8Len m + c.utf8Size then
      foldrAux f
        (f
          ({ data := l ++ (m.reverse ++ c :: r) }.get
            ({ data := l ++ (m.reverse ++ c :: r) }.prev { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) }))
          a)
        { data := l ++ (m.reverse ++ c :: r) }
        ({ data := l ++ (m.reverse ++ c :: r) }.prev { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) })
        { byteIdx := utf8Len l }
    else a) =
    List.foldl (fun x y => f y x) (f c a) m

Tactic:
rw [if_pos add_utf8Size_pos]

Result:
case cons
α : Type u_1
f : Char → α → α
l m✝ : List Char
c : Char
m : List Char
IH :
  ∀ (r : List Char) (a : α),
    foldrAux f a { data := l ++ m.reverse ++ r } { byteIdx := utf8Len l + utf8Len m.reverse } { byteIdx := utf8Len l } =
      List.foldr f a m.reverse
r : List Char
a : α
⊢ foldrAux f
      (f
        ({ data := l ++ (m.reverse ++ c :: r) }.get
          ({ data := l ++ (m.reverse ++ c :: r) }.prev { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) }))
        a)
      { data := l ++ (m.reverse ++ c :: r) }
      ({ data := l ++ (m.reverse ++ c :: r) }.prev { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) })
      { byteIdx := utf8Len l } =
    List.foldl (fun x y => f y x) (f c a) m

Proof state:
case cons
α : Type u_1
f : Char → α → α
l m✝ : List Char
c : Char
m : List Char
IH :
  ∀ (r : List Char) (a : α),
    foldrAux f a { data := l ++ m.reverse ++ r } { byteIdx := utf8Len l + utf8Len m.reverse } { byteIdx := utf8Len l } =
      List.foldr f a m.reverse
r : List Char
a : α
⊢ foldrAux f
      (f
        ({ data := l ++ (m.reverse ++ c :: r) }.get
          ({ data := l ++ (m.reverse ++ c :: r) }.prev { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) }))
        a)
      { data := l ++ (m.reverse ++ c :: r) }
      ({ data := l ++ (m.reverse ++ c :: r) }.prev { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) })
      { byteIdx := utf8Len l } =
    List.foldl (fun x y => f y x) (f c a) m

Tactic:
simp only [← Nat.add_assoc, by simpa using prev_of_valid (l ++ m.reverse) c r]

Result:
case cons
α : Type u_1
f : Char → α → α
l m✝ : List Char
c : Char
m : List Char
IH :
  ∀ (r : List Char) (a : α),
    foldrAux f a { data := l ++ m.reverse ++ r } { byteIdx := utf8Len l + utf8Len m.reverse } { byteIdx := utf8Len l } =
      List.foldr f a m.reverse
r : List Char
a : α
⊢ foldrAux f (f ({ data := l ++ (m.reverse ++ c :: r) }.get { byteIdx := utf8Len l + utf8Len m }) a)
      { data := l ++ (m.reverse ++ c :: r) } { byteIdx := utf8Len l + utf8Len m } { byteIdx := utf8Len l } =
    List.foldl (fun x y => f y x) (f c a) m

Proof state:
case cons
α : Type u_1
f : Char → α → α
l m✝ : List Char
c : Char
m : List Char
IH :
  ∀ (r : List Char) (a : α),
    foldrAux f a { data := l ++ m.reverse ++ r } { byteIdx := utf8Len l + utf8Len m.reverse } { byteIdx := utf8Len l } =
      List.foldr f a m.reverse
r : List Char
a : α
⊢ foldrAux f (f ((c :: r).head?.getD 'A') a) { data := l ++ (m.reverse ++ c :: r) } { byteIdx := utf8Len l + utf8Len m }
      { byteIdx := utf8Len l } =
    List.foldl (fun x y => f y x) (f c a) m

Tactic:
simpa using IH (c::r) (f c a)

Result:
no goals

Proof state:
α : Type u_1
f : Char → α → α
l m✝ : List Char
c : Char
m : List Char
IH :
  ∀ (r : List Char) (a : α),
    foldrAux f a { data := l ++ m.reverse ++ r } { byteIdx := utf8Len l + utf8Len m.reverse } { byteIdx := utf8Len l } =
      List.foldr f a m.reverse
r : List Char
a : α
⊢ ?m.156277

Tactic:
simpa using prev_of_valid (l ++ m.reverse) c r

Result:
no goals

Proof state:
case nil
α : Type u_1
f : Char → α → α
l m r : List Char
a : α
⊢ (if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len [].reverse } then
      let_fun this := ⋯;
      let i := { data := l ++ [].reverse ++ r }.prev { byteIdx := utf8Len l + utf8Len [].reverse };
      let a := f ({ data := l ++ [].reverse ++ r }.get i) a;
      foldrAux f a { data := l ++ [].reverse ++ r } i { byteIdx := utf8Len l }
    else a) =
    List.foldr f a [].reverse

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
f : Char → α → α
l m r : List Char
a : α
⊢ foldrAux f a { data := l ++ m.reverse.reverse ++ r } { byteIdx := utf8Len l + utf8Len m.reverse.reverse }
      { byteIdx := utf8Len l } =
    List.foldr f a m.reverse.reverse

Tactic:
induction m.reverse generalizing r a with (unfold foldrAux; simp)
| cons c m IH =>
  rw [if_pos add_utf8Size_pos]
  simp only [← Nat.add_assoc, by simpa using prev_of_valid (l ++ m.reverse) c r]
  simp only [by simpa using get_of_valid (l ++ m.reverse) (c :: r)]
  simpa using IH (c::r) (f c a)

Result:
no goals

Proof state:
case cons
α : Type u_1
f : Char → α → α
l m✝ : List Char
c : Char
m : List Char
IH :
  ∀ (r : List Char) (a : α),
    foldrAux f a { data := l ++ m.reverse ++ r } { byteIdx := utf8Len l + utf8Len m.reverse } { byteIdx := utf8Len l } =
      List.foldr f a m.reverse
r : List Char
a : α
⊢ foldrAux f (f ({ data := l ++ (m.reverse ++ c :: r) }.get { byteIdx := utf8Len l + utf8Len m }) a)
      { data := l ++ (m.reverse ++ c :: r) } { byteIdx := utf8Len l + utf8Len m } { byteIdx := utf8Len l } =
    List.foldl (fun x y => f y x) (f c a) m

Tactic:
simp only [by simpa using get_of_valid (l ++ m.reverse) (c :: r)]

Result:
case cons
α : Type u_1
f : Char → α → α
l m✝ : List Char
c : Char
m : List Char
IH :
  ∀ (r : List Char) (a : α),
    foldrAux f a { data := l ++ m.reverse ++ r } { byteIdx := utf8Len l + utf8Len m.reverse } { byteIdx := utf8Len l } =
      List.foldr f a m.reverse
r : List Char
a : α
⊢ foldrAux f (f ((c :: r).head?.getD 'A') a) { data := l ++ (m.reverse ++ c :: r) } { byteIdx := utf8Len l + utf8Len m }
      { byteIdx := utf8Len l } =
    List.foldl (fun x y => f y x) (f c a) m

Proof state:
α : Type u_1
f : Char → α → α
l m r : List Char
a : α
⊢ foldrAux f a { data := l ++ m ++ r } { byteIdx := utf8Len l + utf8Len m } { byteIdx := utf8Len l } = List.foldr f a m

Tactic:
rw [← m.reverse_reverse]

Result:
α : Type u_1
f : Char → α → α
l m r : List Char
a : α
⊢ foldrAux f a { data := l ++ m.reverse.reverse ++ r } { byteIdx := utf8Len l + utf8Len m.reverse.reverse }
      { byteIdx := utf8Len l } =
    List.foldr f a m.reverse.reverse

Proof state:
case nil
α : Type u_1
f : Char → α → α
l m r : List Char
a : α
⊢ foldrAux f a { data := l ++ [].reverse ++ r } { byteIdx := utf8Len l + utf8Len [].reverse } { byteIdx := utf8Len l } =
    List.foldr f a [].reverse

Tactic:
unfold foldrAux

Result:
case nil
α : Type u_1
f : Char → α → α
l m r : List Char
a : α
⊢ (if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len [].reverse } then
      let_fun this := ⋯;
      let i := { data := l ++ [].reverse ++ r }.prev { byteIdx := utf8Len l + utf8Len [].reverse };
      let a := f ({ data := l ++ [].reverse ++ r }.get i) a;
      foldrAux f a { data := l ++ [].reverse ++ r } i { byteIdx := utf8Len l }
    else a) =
    List.foldr f a [].reverse