-- Mathlib/Data/List/SplitOn.lean
theorem splitOnP.go_acc (xs acc : List α) :
    splitOnP.go p xs acc = modifyHead (acc.reverse ++ ·) (splitOnP p xs)

Proof state:
case cons.isTrue
α : Type u_1
p : α → Bool
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => acc.reverse ++ x) (splitOnP p tl)
acc : List α
h✝ : p hd = true
⊢ acc.reverse :: go p tl [] = modifyHead (fun x => acc.reverse ++ x) ([].reverse :: go p tl [])

Tactic:
simp only [modifyHead, reverse_nil, append_nil]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
acc : List α
⊢ go p [] acc = modifyHead (fun x => acc.reverse ++ x) (splitOnP p [])

Tactic:
simp only [go, modifyHead, splitOnP_nil, append_nil]

Result:
no goals

Proof state:
case cons.isFalse
α : Type u_1
p : α → Bool
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => acc.reverse ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
⊢ modifyHead (fun x => (hd :: acc).reverse ++ x) (splitOnP p tl) =
    modifyHead ((fun x => acc.reverse ++ x) ∘ fun x => [hd].reverse ++ x) (splitOnP p tl)

Tactic:
congr

Result:
case cons.isFalse.e_f
α : Type u_1
p : α → Bool
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => acc.reverse ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
⊢ (fun x => (hd :: acc).reverse ++ x) = (fun x => acc.reverse ++ x) ∘ fun x => [hd].reverse ++ x

Proof state:
case cons.isFalse
α : Type u_1
p : α → Bool
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => acc.reverse ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
⊢ go p tl (hd :: acc) = modifyHead (fun x => acc.reverse ++ x) (go p tl [hd])

Tactic:
rw [ih [hd], modifyHead_modifyHead, ih]

Result:
case cons.isFalse
α : Type u_1
p : α → Bool
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => acc.reverse ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
⊢ modifyHead (fun x => (hd :: acc).reverse ++ x) (splitOnP p tl) =
    modifyHead ((fun x => acc.reverse ++ x) ∘ fun x => [hd].reverse ++ x) (splitOnP p tl)

Proof state:
case cons
α : Type u_1
p : α → Bool
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => acc.reverse ++ x) (splitOnP p tl)
acc : List α
⊢ go p (hd :: tl) acc = modifyHead (fun x => acc.reverse ++ x) (splitOnP p (hd :: tl))

Tactic:
simp only [splitOnP, go]

Result:
case cons
α : Type u_1
p : α → Bool
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => acc.reverse ++ x) (splitOnP p tl)
acc : List α
⊢ (if p hd = true then acc.reverse :: go p tl [] else go p tl (hd :: acc)) =
    modifyHead (fun x => acc.reverse ++ x) (if p hd = true then [].reverse :: go p tl [] else go p tl [hd])

Proof state:
case cons.isFalse.e_f.h
α : Type u_1
p : α → Bool
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => acc.reverse ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
x : List α
⊢ acc.reverse ++ ([hd] ++ x) = ((fun x => acc.reverse ++ x) ∘ fun x => [].reverse ++ ([hd] ++ x)) x

Tactic:
rfl

Result:
no goals

Proof state:
case cons.isFalse.e_f.h
α : Type u_1
p : α → Bool
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => acc.reverse ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
x : List α
⊢ (hd :: acc).reverse ++ x = ((fun x => acc.reverse ++ x) ∘ fun x => [hd].reverse ++ x) x

Tactic:
simp only [reverse_cons, append_assoc]

Result:
case cons.isFalse.e_f.h
α : Type u_1
p : α → Bool
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => acc.reverse ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
x : List α
⊢ acc.reverse ++ ([hd] ++ x) = ((fun x => acc.reverse ++ x) ∘ fun x => [].reverse ++ ([hd] ++ x)) x

Proof state:
case cons
α : Type u_1
p : α → Bool
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => acc.reverse ++ x) (splitOnP p tl)
acc : List α
⊢ (if p hd = true then acc.reverse :: go p tl [] else go p tl (hd :: acc)) =
    modifyHead (fun x => acc.reverse ++ x) (if p hd = true then [].reverse :: go p tl [] else go p tl [hd])

Tactic:
split

Result:
case cons.isTrue
α : Type u_1
p : α → Bool
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => acc.reverse ++ x) (splitOnP p tl)
acc : List α
h✝ : p hd = true
⊢ acc.reverse :: go p tl [] = modifyHead (fun x => acc.reverse ++ x) ([].reverse :: go p tl [])

case cons.isFalse
α : Type u_1
p : α → Bool
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => acc.reverse ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
⊢ go p tl (hd :: acc) = modifyHead (fun x => acc.reverse ++ x) (go p tl [hd])

Proof state:
case cons.isFalse.e_f
α : Type u_1
p : α → Bool
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => acc.reverse ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
⊢ (fun x => (hd :: acc).reverse ++ x) = (fun x => acc.reverse ++ x) ∘ fun x => [hd].reverse ++ x

Tactic:
funext x

Result:
case cons.isFalse.e_f.h
α : Type u_1
p : α → Bool
hd : α
tl : List α
ih : ∀ (acc : List α), go p tl acc = modifyHead (fun x => acc.reverse ++ x) (splitOnP p tl)
acc : List α
h✝ : ¬p hd = true
x : List α
⊢ (hd :: acc).reverse ++ x = ((fun x => acc.reverse ++ x) ∘ fun x => [hd].reverse ++ x) x