case h.h.h
α : Type u_1
P : α → Bool
l : List α
⊢ splitOnP P l = splitOnPTR P l
⊢ @splitOnP = @splitOnPTR
funext α P l
case h.h.h
α : Type u_1
P : α → Bool
l : List α
⊢ splitOnP P l = splitOnPTR.go P l #[] #[]
case h.h.h
α : Type u_1
P : α → Bool
l : List α
⊢ splitOnP P l = splitOnPTR P l
simp [splitOnPTR]
case h.h.h
α : Type u_1
P : α → Bool
l : List α
⊢ ∀ (xs : List α) (acc : Array α) (r : Array (List α)),
    splitOnPTR.go P xs acc r = r.data ++ splitOnP.go P xs (reverse acc.data)
case h.h.h
α : Type u_1
P : α → Bool
l : List α
⊢ splitOnP P l = splitOnPTR.go P l #[] #[]
suffices ∀ xs acc r, splitOnPTR.go P xs acc r = r.data ++ splitOnP.go P xs acc.data.reverse from
  (this l #[] #[]).symm
case h.h.h
α : Type u_1
P : α → Bool
l xs : List α
acc : Array α
r : Array (List α)
⊢ splitOnPTR.go P xs acc r = r.data ++ splitOnP.go P xs (reverse acc.data)
case h.h.h
α : Type u_1
P : α → Bool
l : List α
⊢ ∀ (xs : List α) (acc : Array α) (r : Array (List α)),
    splitOnPTR.go P xs acc r = r.data ++ splitOnP.go P xs (reverse acc.data)
intro xs acc r
no goals
case h.h.h
α : Type u_1
P : α → Bool
l xs : List α
acc : Array α
r : Array (List α)
⊢ splitOnPTR.go P xs acc r = r.data ++ splitOnP.go P xs (reverse acc.data)
induction xs generalizing acc r with simp [splitOnP.go, splitOnPTR.go]
| cons x xs IH => cases P x <;> simp [*]
no goals
case h.h.h.cons
α : Type u_1
P : α → Bool
l : List α
x : α
xs : List α
IH : ∀ (acc : Array α) (r : Array (List α)), splitOnPTR.go P xs acc r = r.data ++ splitOnP.go P xs (reverse acc.data)
acc : Array α
r : Array (List α)
⊢ (bif P x then splitOnPTR.go P xs #[] (Array.push r acc.data) else splitOnPTR.go P xs (Array.push acc x) r) =
    r.data ++ if P x = true then acc.data :: splitOnP.go P xs [] else splitOnP.go P xs (x :: reverse acc.data)
cases P x <;> simp [*]