-- Mathlib/Data/List/SplitOn.lean
theorem splitOn_intercalate [DecidableEq α] (x : α) (hx : ∀ l ∈ ls, x ∉ l) (hls : ls ≠ []) :
    ([x].intercalate ls).splitOn x = ls

Proof state:
case cons.nil
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (intersperse [x] []).flatten = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
⊢ ∀ (x_1 : α), x_1 ∈ hd → ¬(x_1 == x) = true

Tactic:
intro y hy H

Result:
case cons.nil
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (intersperse [x] []).flatten = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
y : α
hy : y ∈ hd
H : (y == x) = true
⊢ False

Proof state:
case cons.nil
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (intersperse [x] []).flatten = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
y : α
hy : x ∈ hd
H : (y == x) = true
⊢ False

Tactic:
refine hx hd ?_ hy

Result:
case cons.nil
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (intersperse [x] []).flatten = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
y : α
hy : x ∈ hd
H : (y == x) = true
⊢ hd ∈ [hd]

Proof state:
case cons.nil
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (intersperse [x] []).flatten = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
⊢ splitOn x hd = [hd]

Tactic:
refine splitOnP_eq_single _ _ ?_

Result:
case cons.nil
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (intersperse [x] []).flatten = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
⊢ ∀ (x_1 : α), x_1 ∈ hd → ¬(x_1 == x) = true

Proof state:
case cons.nil
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (intersperse [x] []).flatten = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
y : α
hy : y ∈ hd
H : (y == x) = true
⊢ False

Tactic:
rw [eq_of_beq H] at hy

Result:
case cons.nil
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (intersperse [x] []).flatten = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
y : α
hy : x ∈ hd
H : (y == x) = true
⊢ False

Proof state:
case cons
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd : List α
tl : List (List α)
ih : (∀ (l : List α), l ∈ tl → ¬x ∈ l) → tl ≠ [] → splitOn x (intersperse [x] tl).flatten = tl
hx : ∀ (l : List α), l ∈ hd :: tl → ¬x ∈ l
hls : hd :: tl ≠ []
⊢ splitOn x (intersperse [x] (hd :: tl)).flatten = hd :: tl

Tactic:
cases tl

Result:
case cons.nil
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (intersperse [x] []).flatten = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
⊢ splitOn x (intersperse [x] [hd]).flatten = [hd]

case cons.cons
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (intersperse [x] (head✝ :: tail✝)).flatten = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
⊢ splitOn x (intersperse [x] (hd :: head✝ :: tail✝)).flatten = hd :: head✝ :: tail✝

Proof state:
case cons.cons
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd head✝ : List α
tail✝ : List (List α)
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
ih : splitOn x (intersperse [x] (head✝ :: tail✝)).flatten = head✝ :: tail✝
this : ∀ (as : List α), splitOnP (fun x_1 => x_1 == x) (hd ++ x :: as) = hd :: splitOnP (fun x_1 => x_1 == x) as
⊢ splitOn x (hd ++ x :: (intersperse [x] (head✝ :: tail✝)).flatten) = hd :: head✝ :: tail✝

Tactic:
simp only [splitOn] at ih ⊢

Result:
case cons.cons
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd head✝ : List α
tail✝ : List (List α)
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
ih : splitOnP (fun x_1 => x_1 == x) (intersperse [x] (head✝ :: tail✝)).flatten = head✝ :: tail✝
this : ∀ (as : List α), splitOnP (fun x_1 => x_1 == x) (hd ++ x :: as) = hd :: splitOnP (fun x_1 => x_1 == x) as
⊢ splitOnP (fun x_1 => x_1 == x) (hd ++ x :: (intersperse [x] (head✝ :: tail✝)).flatten) = hd :: head✝ :: tail✝

Proof state:
case cons.cons
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd head✝ : List α
tail✝ : List (List α)
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
ih : splitOnP (fun x_1 => x_1 == x) (intersperse [x] (head✝ :: tail✝)).flatten = head✝ :: tail✝
this : ∀ (as : List α), splitOnP (fun x_1 => x_1 == x) (hd ++ x :: as) = hd :: splitOnP (fun x_1 => x_1 == x) as
⊢ splitOnP (fun x_1 => x_1 == x) (hd ++ x :: (intersperse [x] (head✝ :: tail✝)).flatten) = hd :: head✝ :: tail✝

Tactic:
rw [this, ih]

Result:
no goals

Proof state:
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hx : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls : ls ≠ []
⊢ splitOn x (intersperse [x] ls).flatten = ls

Tactic:
induction' ls with hd tl ih

Result:
case nil
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hx : ∀ (l : List α), l ∈ [] → ¬x ∈ l
hls : [] ≠ []
⊢ splitOn x (intersperse [x] []).flatten = []

case cons
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd : List α
tl : List (List α)
ih : (∀ (l : List α), l ∈ tl → ¬x ∈ l) → tl ≠ [] → splitOn x (intersperse [x] tl).flatten = tl
hx : ∀ (l : List α), l ∈ hd :: tl → ¬x ∈ l
hls : hd :: tl ≠ []
⊢ splitOn x (intersperse [x] (hd :: tl)).flatten = hd :: tl

Proof state:
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd head✝ : List α
tail✝ : List (List α)
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
ih : splitOn x (intersperse [x] (head✝ :: tail✝)).flatten = head✝ :: tail✝
y : α
hy : y ∈ hd
H : (fun x_1 => x_1 == x) y = true
⊢ False

Tactic:
rw [eq_of_beq H] at hy

Result:
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd head✝ : List α
tail✝ : List (List α)
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
ih : splitOn x (intersperse [x] (head✝ :: tail✝)).flatten = head✝ :: tail✝
y : α
hy : x ∈ hd
H : (fun x_1 => x_1 == x) y = true
⊢ False

Proof state:
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd head✝ : List α
tail✝ : List (List α)
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
ih : splitOn x (intersperse [x] (head✝ :: tail✝)).flatten = head✝ :: tail✝
y : α
hy : x ∈ hd
H : (fun x_1 => x_1 == x) y = true
⊢ False

Tactic:
exact hx hd (.head _) hy

Result:
no goals

Proof state:
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (intersperse [x] []).flatten = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
this : splitOn x hd = [hd]
⊢ splitOn x (intersperse [x] [hd]).flatten = [hd]

Tactic:
simpa [flatten]

Result:
no goals

Proof state:
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hx : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls : ls ≠ []
⊢ splitOn x ([x].intercalate ls) = ls

Tactic:
simp only [intercalate]

Result:
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hx : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls : ls ≠ []
⊢ splitOn x (intersperse [x] ls).flatten = ls