-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem splitAux_of_valid (p l m r acc) :
    splitAux ⟨l ++ m ++ r⟩ p ⟨utf8Len l⟩ ⟨utf8Len l + utf8Len m⟩ acc =
      acc.reverse ++ (List.splitOnP.go p r m.reverse).map mk

Proof state:
case isFalse.intro.intro.isFalse
p : Char → Bool
l m : List Char
acc : List String
c : Char
r : List Char
h✝ : ¬c :: r = []
h : ¬p c = true
⊢ { data := l ++ (m ++ c :: r) }.splitAux p { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m + c.utf8Size }
      acc =
    acc.reverse ++
      List.map mk (if false = true then m :: List.splitOnP.go p r [] else List.splitOnP.go p r (c :: m.reverse))

Tactic:
simpa [Nat.add_assoc] using splitAux_of_valid p l (m++[c]) r acc

Result:
no goals

Proof state:
case isTrue
p : Char → Bool
l m : List Char
acc : List String
⊢ acc.reverse ++ [{ data := l ++ (m ++ []) }.extract { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m }] =
    acc.reverse ++ List.map mk (List.splitOnP.go p [] m.reverse)

Tactic:
simpa [List.splitOnP.go] using extract_of_valid l m []

Result:
no goals

Proof state:
case isFalse.intro.intro
p : Char → Bool
l m : List Char
acc : List String
c : Char
r : List Char
h✝ : ¬c :: r = []
⊢ (if p ((c :: r).head?.getD 'A') = true then
      { data := l ++ (m ++ c :: r) }.splitAux p { byteIdx := utf8Len l + utf8Len m + c.utf8Size }
        { byteIdx := utf8Len l + utf8Len m + c.utf8Size } ({ data := m } :: acc)
    else
      { data := l ++ (m ++ c :: r) }.splitAux p { byteIdx := utf8Len l }
        { byteIdx := utf8Len l + utf8Len m + c.utf8Size } acc) =
    acc.reverse ++
      List.map mk (if p c = true then m :: List.splitOnP.go p r [] else List.splitOnP.go p r (c :: m.reverse))

Tactic:
split <;> rename_i h

Result:
case isFalse.intro.intro.isTrue
p : Char → Bool
l m : List Char
acc : List String
c : Char
r : List Char
h✝ : ¬c :: r = []
h : p ((c :: r).head?.getD 'A') = true
⊢ { data := l ++ (m ++ c :: r) }.splitAux p { byteIdx := utf8Len l + utf8Len m + c.utf8Size }
      { byteIdx := utf8Len l + utf8Len m + c.utf8Size } ({ data := m } :: acc) =
    acc.reverse ++
      List.map mk (if p c = true then m :: List.splitOnP.go p r [] else List.splitOnP.go p r (c :: m.reverse))

case isFalse.intro.intro.isFalse
p : Char → Bool
l m : List Char
acc : List String
c : Char
r : List Char
h✝ : ¬c :: r = []
h : ¬p ((c :: r).head?.getD 'A') = true
⊢ { data := l ++ (m ++ c :: r) }.splitAux p { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m + c.utf8Size }
      acc =
    acc.reverse ++
      List.map mk (if p c = true then m :: List.splitOnP.go p r [] else List.splitOnP.go p r (c :: m.reverse))

Proof state:
p : Char → Bool
l m r : List Char
acc : List String
⊢ ?m.86169

Tactic:
simpa using atEnd_of_valid (l ++ m) r

Result:
no goals

Proof state:
case isFalse.intro.intro
p : Char → Bool
l m : List Char
acc : List String
c : Char
r : List Char
h✝ : ¬c :: r = []
⊢ (if p ({ data := l ++ (m ++ c :: r) }.get { byteIdx := utf8Len l + utf8Len m }) = true then
      { data := l ++ (m ++ c :: r) }.splitAux p
        ({ data := l ++ (m ++ c :: r) }.next { byteIdx := utf8Len l + utf8Len m })
        ({ data := l ++ (m ++ c :: r) }.next { byteIdx := utf8Len l + utf8Len m })
        ({ data := l ++ (m ++ c :: r) }.extract { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } :: acc)
    else
      { data := l ++ (m ++ c :: r) }.splitAux p { byteIdx := utf8Len l }
        ({ data := l ++ (m ++ c :: r) }.next { byteIdx := utf8Len l + utf8Len m }) acc) =
    acc.reverse ++ List.map mk (List.splitOnP.go p (c :: r) m.reverse)

Tactic:
simp only [by
  simpa using
    (⟨get_of_valid (l ++ m) (c :: r), next_of_valid (l ++ m) c r,
        extract_of_valid l m (c :: r)⟩ :
      _ ∧ _ ∧ _),
  List.splitOnP.go, List.reverse_reverse]

Result:
case isFalse.intro.intro
p : Char → Bool
l m : List Char
acc : List String
c : Char
r : List Char
h✝ : ¬c :: r = []
⊢ (if p ((c :: r).head?.getD 'A') = true then
      { data := l ++ (m ++ c :: r) }.splitAux p { byteIdx := utf8Len l + utf8Len m + c.utf8Size }
        { byteIdx := utf8Len l + utf8Len m + c.utf8Size } ({ data := m } :: acc)
    else
      { data := l ++ (m ++ c :: r) }.splitAux p { byteIdx := utf8Len l }
        { byteIdx := utf8Len l + utf8Len m + c.utf8Size } acc) =
    acc.reverse ++
      List.map mk (if p c = true then m :: List.splitOnP.go p r [] else List.splitOnP.go p r (c :: m.reverse))

Proof state:
p : Char → Bool
l m : List Char
acc : List String
c : Char
r : List Char
h✝ : ¬c :: r = []
⊢ ?m.88026

Tactic:
simpa using
  (⟨get_of_valid (l ++ m) (c :: r), next_of_valid (l ++ m) c r,
      extract_of_valid l m (c :: r)⟩ :
    _ ∧ _ ∧ _)

Result:
no goals

Proof state:
p : Char → Bool
l m r : List Char
acc : List String
⊢ (if h : { data := l ++ m ++ r }.atEnd { byteIdx := utf8Len l + utf8Len m } = true then
      let r := { data := l ++ m ++ r }.extract { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } :: acc;
      r.reverse
    else
      let_fun this := ⋯;
      if p ({ data := l ++ m ++ r }.get { byteIdx := utf8Len l + utf8Len m }) = true then
        let i' := { data := l ++ m ++ r }.next { byteIdx := utf8Len l + utf8Len m };
        { data := l ++ m ++ r }.splitAux p i' i'
          ({ data := l ++ m ++ r }.extract { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } :: acc)
      else
        { data := l ++ m ++ r }.splitAux p { byteIdx := utf8Len l }
          ({ data := l ++ m ++ r }.next { byteIdx := utf8Len l + utf8Len m }) acc) =
    acc.reverse ++ List.map mk (List.splitOnP.go p r m.reverse)

Tactic:
simp only [List.append_assoc, atEnd_iff, endPos_eq, utf8Len_append, Pos.mk_le_mk,
  Nat.add_le_add_iff_left, by simpa using atEnd_of_valid (l ++ m) r, List.reverse_cons,
  dite_eq_ite]

Result:
p : Char → Bool
l m r : List Char
acc : List String
⊢ (if r = [] then
      acc.reverse ++ [{ data := l ++ (m ++ r) }.extract { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m }]
    else
      if p ({ data := l ++ (m ++ r) }.get { byteIdx := utf8Len l + utf8Len m }) = true then
        { data := l ++ (m ++ r) }.splitAux p ({ data := l ++ (m ++ r) }.next { byteIdx := utf8Len l + utf8Len m })
          ({ data := l ++ (m ++ r) }.next { byteIdx := utf8Len l + utf8Len m })
          ({ data := l ++ (m ++ r) }.extract { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } :: acc)
      else
        { data := l ++ (m ++ r) }.splitAux p { byteIdx := utf8Len l }
          ({ data := l ++ (m ++ r) }.next { byteIdx := utf8Len l + utf8Len m }) acc) =
    acc.reverse ++ List.map mk (List.splitOnP.go p r m.reverse)