ι : Type ?u.295105
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs✝ ys : List α
ls : List (List α)
f : List α → List α
x : α
xs : List α
⊢ (if p x = true then reverse [] :: splitOnP.go p xs [] else splitOnP.go p xs [x]) =
    if p x = true then [] :: splitOnP p xs else modifyHead (cons x) (splitOnP p xs)
ι : Type ?u.295105
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs✝ ys : List α
ls : List (List α)
f : List α → List α
x : α
xs : List α
⊢ splitOnP p (x :: xs) = if p x = true then [] :: splitOnP p xs else modifyHead (cons x) (splitOnP p xs)
rw [splitOnP, splitOnP.go]
no goals
ι : Type ?u.295105
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs✝ ys : List α
ls : List (List α)
f : List α → List α
x : α
xs : List α
⊢ (if p x = true then reverse [] :: splitOnP.go p xs [] else splitOnP.go p xs [x]) =
    if p x = true then [] :: splitOnP p xs else modifyHead (cons x) (splitOnP p xs)
split <;> [rfl; simp [splitOnP.go_acc]]