no goals
case nil
ι : Type ?u.293492
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
acc : List α
⊢ go p [] acc = modifyHead (fun x => reverse acc ++ x) (splitOnP p [])
simp only [go, modifyHead, splitOnP_nil, append_nil]
case cons
ι : Type ?u.293492
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => reverse acc ++ x) (splitOnP p tl)
acc : List α
⊢ (if p hd = true then reverse acc :: go p tl [] else go p tl (hd :: acc)) =
    modifyHead (fun x => reverse acc ++ x) (if p hd = true then reverse [] :: go p tl [] else go p tl [hd])
case cons
ι : Type ?u.293492
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => reverse acc ++ x) (splitOnP p tl)
acc : List α
⊢ go p (hd :: tl) acc = modifyHead (fun x => reverse acc ++ x) (splitOnP p (hd :: tl))
simp only [splitOnP, go]
case cons.inl
ι : Type ?u.293492
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => reverse acc ++ x) (splitOnP p tl)
acc : List α
h✝ : p hd = true
⊢ reverse acc :: go p tl [] = modifyHead (fun x => reverse acc ++ x) (reverse [] :: go p tl [])

case cons.inr
ι : Type ?u.293492
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => reverse acc ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
⊢ go p tl (hd :: acc) = modifyHead (fun x => reverse acc ++ x) (go p tl [hd])
case cons
ι : Type ?u.293492
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => reverse acc ++ x) (splitOnP p tl)
acc : List α
⊢ (if p hd = true then reverse acc :: go p tl [] else go p tl (hd :: acc)) =
    modifyHead (fun x => reverse acc ++ x) (if p hd = true then reverse [] :: go p tl [] else go p tl [hd])
split
no goals
case cons.inl
ι : Type ?u.293492
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => reverse acc ++ x) (splitOnP p tl)
acc : List α
h✝ : p hd = true
⊢ reverse acc :: go p tl [] = modifyHead (fun x => reverse acc ++ x) (reverse [] :: go p tl [])
simp only [modifyHead, reverse_nil, append_nil]
case cons.inr
ι : Type ?u.293492
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => reverse acc ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
⊢ modifyHead (fun x => reverse (hd :: acc) ++ x) (splitOnP p tl) =
    modifyHead ((fun x => reverse acc ++ x) ∘ fun x => reverse [hd] ++ x) (splitOnP p tl)
case cons.inr
ι : Type ?u.293492
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => reverse acc ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
⊢ go p tl (hd :: acc) = modifyHead (fun x => reverse acc ++ x) (go p tl [hd])
rw [ih [hd], modifyHead_modifyHead, ih]
case cons.inr.e_f
ι : Type ?u.293492
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => reverse acc ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
⊢ (fun x => reverse (hd :: acc) ++ x) = (fun x => reverse acc ++ x) ∘ fun x => reverse [hd] ++ x
case cons.inr
ι : Type ?u.293492
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => reverse acc ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
⊢ modifyHead (fun x => reverse (hd :: acc) ++ x) (splitOnP p tl) =
    modifyHead ((fun x => reverse acc ++ x) ∘ fun x => reverse [hd] ++ x) (splitOnP p tl)
congr
case cons.inr.e_f.h
ι : Type ?u.293492
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => reverse acc ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
x : List α
⊢ reverse (hd :: acc) ++ x = ((fun x => reverse acc ++ x) ∘ fun x => reverse [hd] ++ x) x
case cons.inr.e_f
ι : Type ?u.293492
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => reverse acc ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
⊢ (fun x => reverse (hd :: acc) ++ x) = (fun x => reverse acc ++ x) ∘ fun x => reverse [hd] ++ x
funext x
case cons.inr.e_f.h
ι : Type ?u.293492
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => reverse acc ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
x : List α
⊢ reverse acc ++ ([hd] ++ x) = ((fun x => reverse acc ++ x) ∘ fun x => reverse [] ++ ([hd] ++ x)) x
case cons.inr.e_f.h
ι : Type ?u.293492
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => reverse acc ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
x : List α
⊢ reverse (hd :: acc) ++ x = ((fun x => reverse acc ++ x) ∘ fun x => reverse [hd] ++ x) x
simp only [reverse_cons, append_assoc]
no goals
case cons.inr.e_f.h
ι : Type ?u.293492
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => reverse acc ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
x : List α
⊢ reverse acc ++ ([hd] ++ x) = ((fun x => reverse acc ++ x) ∘ fun x => reverse [] ++ ([hd] ++ x)) x
rfl