-- Mathlib/Data/List/SplitOn.lean
theorem intercalate_splitOn (x : α) [DecidableEq α] : [x].intercalate (xs.splitOn x) = xs

Proof state:
case pos
α : Type u_1
xs : List α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : (intersperse [hd] (hd' :: tl')).flatten = tl
h' : splitOnP (fun x => x == hd) tl = hd' :: tl'
⊢ (intersperse [hd] ([] :: splitOnP (fun x => x == hd) tl)).flatten = hd :: tl

Tactic:
simp [ih, flatten, h']

Result:
no goals

Proof state:
case pos
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : (intersperse [x] (hd' :: tl')).flatten = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
h : (hd == x) = true
⊢ (intersperse [x] ([] :: splitOnP (fun x_1 => x_1 == x) tl)).flatten = hd :: tl

Tactic:
rw [beq_iff_eq] at h

Result:
case pos
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : (intersperse [x] (hd' :: tl')).flatten = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
h : hd = x
⊢ (intersperse [x] ([] :: splitOnP (fun x_1 => x_1 == x) tl)).flatten = hd :: tl

Proof state:
case nil
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
⊢ (intersperse [x] (splitOnP (fun x_1 => x_1 == x) [])).flatten = []

Tactic:
simp [flatten]

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : (intersperse [x] (hd' :: tl')).flatten = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
⊢ (intersperse [x]
        (if (hd == x) = true then [] :: splitOnP (fun x_1 => x_1 == x) tl
        else modifyHead (cons hd) (splitOnP (fun x_1 => x_1 == x) tl))).flatten =
    hd :: tl

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : (intersperse [x] (hd' :: tl')).flatten = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
h : (hd == x) = true
⊢ (intersperse [x] ([] :: splitOnP (fun x_1 => x_1 == x) tl)).flatten = hd :: tl

case neg
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : (intersperse [x] (hd' :: tl')).flatten = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
h : ¬(hd == x) = true
⊢ (intersperse [x] (modifyHead (cons hd) (splitOnP (fun x_1 => x_1 == x) tl))).flatten = hd :: tl

Proof state:
case cons.cons
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
hd : α
tl : List α
ih : (intersperse [x] (splitOnP (fun x_1 => x_1 == x) tl)).flatten = tl
hd' : List α
tl' : List (List α)
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
⊢ (intersperse [x] (splitOnP (fun x_1 => x_1 == x) (hd :: tl))).flatten = hd :: tl

Tactic:
rw [h'] at ih

Result:
case cons.cons
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : (intersperse [x] (hd' :: tl')).flatten = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
⊢ (intersperse [x] (splitOnP (fun x_1 => x_1 == x) (hd :: tl))).flatten = hd :: tl

Proof state:
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
⊢ [x].intercalate (splitOn x xs) = xs

Tactic:
simp only [intercalate, splitOn]

Result:
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
⊢ (intersperse [x] (splitOnP (fun x_1 => x_1 == x) xs)).flatten = xs

Proof state:
case pos
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : (intersperse [x] (hd' :: tl')).flatten = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
h : hd = x
⊢ (intersperse [x] ([] :: splitOnP (fun x_1 => x_1 == x) tl)).flatten = hd :: tl

Tactic:
subst h

Result:
case pos
α : Type u_1
xs : List α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : (intersperse [hd] (hd' :: tl')).flatten = tl
h' : splitOnP (fun x => x == hd) tl = hd' :: tl'
⊢ (intersperse [hd] ([] :: splitOnP (fun x => x == hd) tl)).flatten = hd :: tl

Proof state:
case neg
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : (intersperse [x] (hd' :: tl')).flatten = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
h : ¬(hd == x) = true
⊢ (intersperse [x] (modifyHead (cons hd) (splitOnP (fun x_1 => x_1 == x) tl))).flatten = hd :: tl

Tactic:
cases tl' <;> simpa [flatten, h'] using ih

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : (intersperse [x] (hd' :: tl')).flatten = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
⊢ (intersperse [x] (splitOnP (fun x_1 => x_1 == x) (hd :: tl))).flatten = hd :: tl

Tactic:
rw [splitOnP_cons]

Result:
case cons.cons
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : (intersperse [x] (hd' :: tl')).flatten = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
⊢ (intersperse [x]
        (if (hd == x) = true then [] :: splitOnP (fun x_1 => x_1 == x) tl
        else modifyHead (cons hd) (splitOnP (fun x_1 => x_1 == x) tl))).flatten =
    hd :: tl

Proof state:
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
⊢ (intersperse [x] (splitOnP (fun x_1 => x_1 == x) xs)).flatten = xs

Tactic:
induction' xs with hd tl ih

Result:
case nil
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
⊢ (intersperse [x] (splitOnP (fun x_1 => x_1 == x) [])).flatten = []

case cons
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
hd : α
tl : List α
ih : (intersperse [x] (splitOnP (fun x_1 => x_1 == x) tl)).flatten = tl
⊢ (intersperse [x] (splitOnP (fun x_1 => x_1 == x) (hd :: tl))).flatten = hd :: tl

Proof state:
case cons.nil
α : Type u_1
xs : List α
x : α
inst✝ : DecidableEq α
hd : α
tl : List α
ih : (intersperse [x] (splitOnP (fun x_1 => x_1 == x) tl)).flatten = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = []
⊢ (intersperse [x] (splitOnP (fun x_1 => x_1 == x) (hd :: tl))).flatten = hd :: tl

Tactic:
exact (splitOnP_ne_nil _ tl h').elim

Result:
no goals