-- 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 :: 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))

Tactic:
simp_all only [List.head?_cons, Option.getD_some]

Result:
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))

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

Tactic:
simp_all only [List.head?_cons, Option.getD_some]

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 = 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 True then m :: List.splitOnP.go p r [] else List.splitOnP.go p r (c :: m.reverse))

Proof state:
case isFalse
p : Char → Bool
l m r : List Char
acc : List String
h✝ : ¬r = []
⊢ (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)

Tactic:
obtain ⟨c, r, rfl⟩ := r.exists_cons_of_ne_nil ‹_›

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 ({ 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)

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

Tactic:
split

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

case isFalse
p : Char → Bool
l m r : List Char
acc : List String
h✝ : ¬r = []
⊢ (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)

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

Tactic:
unfold splitAux

Result:
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)

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

Tactic:
subst r

Result:
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)

Proof state:
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 = 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 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 (⟨m⟩::acc)

Result:
no goals