-- Mathlib/Data/List/SplitOn.lean
theorem splitOnP_spec (as : List α) :
    flatten (zipWith (· ++ ·) (splitOnP p as) (((as.filter p).map fun x => [x]) ++ [[]])) = as

Proof state:
case cons
α : Type u_1
p : α → Bool
as : List α
ys : List (List α)
a : α
hys : ys ≠ []
head✝ : List α
tail✝ : List (List α)
hxs : head✝ :: tail✝ ≠ []
⊢ (zipWith (fun x x_1 => x ++ x_1) (modifyHead (cons a) (head✝ :: tail✝)) ys).flatten =
    a :: (zipWith (fun x x_1 => x ++ x_1) (head✝ :: tail✝) ys).flatten

Tactic:
cases ys with | nil => contradiction | cons => rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
a : α
as' : List α
ih : (zipWith (fun x1 x2 => x1 ++ x2) (splitOnP p as') (map (fun x => [x]) (filter p as') ++ [[]])).flatten = as'
⊢ (zipWith (fun x1 x2 => x1 ++ x2) (if p a = true then [] :: splitOnP p as' else modifyHead (cons a) (splitOnP p as'))
        (map (fun x => [x])
            (match p a with
            | true => a :: filter p as'
            | false => filter p as') ++
          [[]])).flatten =
    a :: as'

Tactic:
by_cases h : p a

Result:
case pos
α : Type u_1
p : α → Bool
a : α
as' : List α
ih : (zipWith (fun x1 x2 => x1 ++ x2) (splitOnP p as') (map (fun x => [x]) (filter p as') ++ [[]])).flatten = as'
h : p a = true
⊢ (zipWith (fun x1 x2 => x1 ++ x2) (if p a = true then [] :: splitOnP p as' else modifyHead (cons a) (splitOnP p as'))
        (map (fun x => [x])
            (match p a with
            | true => a :: filter p as'
            | false => filter p as') ++
          [[]])).flatten =
    a :: as'

case neg
α : Type u_1
p : α → Bool
a : α
as' : List α
ih : (zipWith (fun x1 x2 => x1 ++ x2) (splitOnP p as') (map (fun x => [x]) (filter p as') ++ [[]])).flatten = as'
h : ¬p a = true
⊢ (zipWith (fun x1 x2 => x1 ++ x2) (if p a = true then [] :: splitOnP p as' else modifyHead (cons a) (splitOnP p as'))
        (map (fun x => [x])
            (match p a with
            | true => a :: filter p as'
            | false => filter p as') ++
          [[]])).flatten =
    a :: as'

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ (zipWith (fun x1 x2 => x1 ++ x2) (splitOnP p []) (map (fun x => [x]) (filter p []) ++ [[]])).flatten = []

Tactic:
rfl

Result:
no goals

Proof state:
case pos
α : Type u_1
p : α → Bool
a : α
as' : List α
ih : (zipWith (fun x1 x2 => x1 ++ x2) (splitOnP p as') (map (fun x => [x]) (filter p as') ++ [[]])).flatten = as'
h : p a = true
⊢ (zipWith (fun x1 x2 => x1 ++ x2) (if p a = true then [] :: splitOnP p as' else modifyHead (cons a) (splitOnP p as'))
        (map (fun x => [x])
            (match p a with
            | true => a :: filter p as'
            | false => filter p as') ++
          [[]])).flatten =
    a :: as'

Tactic:
rw [if_pos h, h, map, cons_append, zipWith, nil_append, flatten, cons_append, cons_inj_right]

Result:
case pos
α : Type u_1
p : α → Bool
a : α
as' : List α
ih : (zipWith (fun x1 x2 => x1 ++ x2) (splitOnP p as') (map (fun x => [x]) (filter p as') ++ [[]])).flatten = as'
h : p a = true
⊢ [] ++ (zipWith (fun x1 x2 => x1 ++ x2) (splitOnP p as') (map (fun x => [x]) (filter p as') ++ [[]])).flatten = as'

Proof state:
α : Type u_1
p : α → Bool
as : List α
xs ys : List (List α)
a : α
hxs : xs ≠ []
hys : ys ≠ []
⊢ (zipWith (fun x x_1 => x ++ x_1) (modifyHead (cons a) xs) ys).flatten =
    a :: (zipWith (fun x x_1 => x ++ x_1) xs ys).flatten

Tactic:
cases xs with | nil => contradiction | cons =>
  cases ys with | nil => contradiction | cons => rfl

Result:
no goals

Proof state:
case pos
α : Type u_1
p : α → Bool
a : α
as' : List α
ih : (zipWith (fun x1 x2 => x1 ++ x2) (splitOnP p as') (map (fun x => [x]) (filter p as') ++ [[]])).flatten = as'
h : p a = true
⊢ [] ++ (zipWith (fun x1 x2 => x1 ++ x2) (splitOnP p as') (map (fun x => [x]) (filter p as') ++ [[]])).flatten = as'

Tactic:
exact ih

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
as : List α
ys : List (List α)
a : α
hys : ys ≠ []
hxs : [] ≠ []
⊢ (zipWith (fun x x_1 => x ++ x_1) (modifyHead (cons a) []) ys).flatten =
    a :: (zipWith (fun x x_1 => x ++ x_1) [] ys).flatten

Tactic:
contradiction

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
a : α
as' : List α
ih : (zipWith (fun x1 x2 => x1 ++ x2) (splitOnP p as') (map (fun x => [x]) (filter p as') ++ [[]])).flatten = as'
⊢ (zipWith (fun x1 x2 => x1 ++ x2) (splitOnP p (a :: as')) (map (fun x => [x]) (filter p (a :: as')) ++ [[]])).flatten =
    a :: as'

Tactic:
rw [splitOnP_cons, filter]

Result:
case cons
α : Type u_1
p : α → Bool
a : α
as' : List α
ih : (zipWith (fun x1 x2 => x1 ++ x2) (splitOnP p as') (map (fun x => [x]) (filter p as') ++ [[]])).flatten = as'
⊢ (zipWith (fun x1 x2 => x1 ++ x2) (if p a = true then [] :: splitOnP p as' else modifyHead (cons a) (splitOnP p as'))
        (map (fun x => [x])
            (match p a with
            | true => a :: filter p as'
            | false => filter p as') ++
          [[]])).flatten =
    a :: as'

Proof state:
case cons.cons
α : Type u_1
p : α → Bool
as : List α
a : α
head✝¹ : List α
tail✝¹ : List (List α)
hxs : head✝¹ :: tail✝¹ ≠ []
head✝ : List α
tail✝ : List (List α)
hys : head✝ :: tail✝ ≠ []
⊢ (zipWith (fun x x_1 => x ++ x_1) (modifyHead (cons a) (head✝¹ :: tail✝¹)) (head✝ :: tail✝)).flatten =
    a :: (zipWith (fun x x_1 => x ++ x_1) (head✝¹ :: tail✝¹) (head✝ :: tail✝)).flatten

Tactic:
rfl

Result:
no goals

Proof state:
case neg
α : Type u_1
p : α → Bool
a : α
as' : List α
ih : (zipWith (fun x1 x2 => x1 ++ x2) (splitOnP p as') (map (fun x => [x]) (filter p as') ++ [[]])).flatten = as'
h : ¬p a = true
⊢ (zipWith (fun x1 x2 => x1 ++ x2) (if p a = true then [] :: splitOnP p as' else modifyHead (cons a) (splitOnP p as'))
        (map (fun x => [x])
            (match p a with
            | true => a :: filter p as'
            | false => filter p as') ++
          [[]])).flatten =
    a :: as'

Tactic:
rw [if_neg h, eq_false_of_ne_true h, flatten_zipWith (splitOnP_ne_nil _ _)
  (append_ne_nil_of_right_ne_nil _ (cons_ne_nil [] [])), cons_inj_right]

Result:
case neg
α : Type u_1
p : α → Bool
a : α
as' : List α
ih : (zipWith (fun x1 x2 => x1 ++ x2) (splitOnP p as') (map (fun x => [x]) (filter p as') ++ [[]])).flatten = as'
h : ¬p a = true
⊢ (zipWith (fun x x_1 => x ++ x_1) (splitOnP p as')
        (map (fun x => [x])
            (match false with
            | true => a :: filter p as'
            | false => filter p as') ++
          [[]])).flatten =
    as'

Proof state:
case neg
α : Type u_1
p : α → Bool
a : α
as' : List α
ih : (zipWith (fun x1 x2 => x1 ++ x2) (splitOnP p as') (map (fun x => [x]) (filter p as') ++ [[]])).flatten = as'
h : ¬p a = true
⊢ (zipWith (fun x x_1 => x ++ x_1) (splitOnP p as')
        (map (fun x => [x])
            (match false with
            | true => a :: filter p as'
            | false => filter p as') ++
          [[]])).flatten =
    as'

Tactic:
exact ih

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
p : α → Bool
as : List α
a : α
head✝ : List α
tail✝ : List (List α)
hxs : head✝ :: tail✝ ≠ []
hys : [] ≠ []
⊢ (zipWith (fun x x_1 => x ++ x_1) (modifyHead (cons a) (head✝ :: tail✝)) []).flatten =
    a :: (zipWith (fun x x_1 => x ++ x_1) (head✝ :: tail✝) []).flatten

Tactic:
contradiction

Result:
no goals