ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
⊢ join (intersperse [x] (splitOnP (fun x_1 => x_1 == x) xs)) = xs
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
⊢ intercalate [x] (splitOn x xs) = xs
simp only [intercalate, splitOn]
case nil
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
⊢ join (intersperse [x] (splitOnP (fun x_1 => x_1 == x) [])) = []

case cons
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
hd : α
tl : List α
ih : join (intersperse [x] (splitOnP (fun x_1 => x_1 == x) tl)) = tl
⊢ join (intersperse [x] (splitOnP (fun x_1 => x_1 == x) (hd :: tl))) = hd :: tl
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
⊢ join (intersperse [x] (splitOnP (fun x_1 => x_1 == x) xs)) = xs
induction' xs with hd tl ih
case cons.cons
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : join (intersperse [x] (hd' :: tl')) = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
⊢ join (intersperse [x] (splitOnP (fun x_1 => x_1 == x) (hd :: tl))) = hd :: tl
case cons.cons
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
hd : α
tl : List α
ih : join (intersperse [x] (splitOnP (fun x_1 => x_1 == x) tl)) = tl
hd' : List α
tl' : List (List α)
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
⊢ join (intersperse [x] (splitOnP (fun x_1 => x_1 == x) (hd :: tl))) = hd :: tl
rw [h'] at ih
case cons.cons
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : join (intersperse [x] (hd' :: tl')) = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
⊢ join
      (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))) =
    hd :: tl
case cons.cons
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : join (intersperse [x] (hd' :: tl')) = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
⊢ join (intersperse [x] (splitOnP (fun x_1 => x_1 == x) (hd :: tl))) = hd :: tl
rw [splitOnP_cons]
case cons.cons.inl
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : join (intersperse [x] (hd' :: tl')) = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
h : (hd == x) = true
⊢ join (intersperse [x] ([] :: splitOnP (fun x_1 => x_1 == x) tl)) = hd :: tl

case cons.cons.inr
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : join (intersperse [x] (hd' :: tl')) = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
h : ¬(hd == x) = true
⊢ join (intersperse [x] (modifyHead (cons hd) (splitOnP (fun x_1 => x_1 == x) tl))) = hd :: tl
case cons.cons
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : join (intersperse [x] (hd' :: tl')) = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
⊢ join
      (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))) =
    hd :: tl
split_ifs with h
no goals
case cons.cons.inr
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : join (intersperse [x] (hd' :: tl')) = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
h : ¬(hd == x) = true
⊢ join (intersperse [x] (modifyHead (cons hd) (splitOnP (fun x_1 => x_1 == x) tl))) = hd :: tl
cases tl' <;> simpa [join, h'] using ih
no goals
case nil
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
⊢ join (intersperse [x] (splitOnP (fun x_1 => x_1 == x) [])) = []
simp [join]
no goals
case cons.nil
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
hd : α
tl : List α
ih : join (intersperse [x] (splitOnP (fun x_1 => x_1 == x) tl)) = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = []
⊢ join (intersperse [x] (splitOnP (fun x_1 => x_1 == x) (hd :: tl))) = hd :: tl
exact (splitOnP_ne_nil _ tl h').elim
case cons.cons.inl
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : join (intersperse [x] (hd' :: tl')) = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
h : hd = x
⊢ join (intersperse [x] ([] :: splitOnP (fun x_1 => x_1 == x) tl)) = hd :: tl
case cons.cons.inl
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : join (intersperse [x] (hd' :: tl')) = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
h : (hd == x) = true
⊢ join (intersperse [x] ([] :: splitOnP (fun x_1 => x_1 == x) tl)) = hd :: tl
rw [beq_iff_eq] at h
case cons.cons.inl
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : join (intersperse [hd] (hd' :: tl')) = tl
h' : splitOnP (fun x => x == hd) tl = hd' :: tl'
⊢ join (intersperse [hd] ([] :: splitOnP (fun x => x == hd) tl)) = hd :: tl
case cons.cons.inl
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
x : α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : join (intersperse [x] (hd' :: tl')) = tl
h' : splitOnP (fun x_1 => x_1 == x) tl = hd' :: tl'
h : hd = x
⊢ join (intersperse [x] ([] :: splitOnP (fun x_1 => x_1 == x) tl)) = hd :: tl
subst h
no goals
case cons.cons.inl
ι : Type ?u.305889
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
hd : α
tl hd' : List α
tl' : List (List α)
ih : join (intersperse [hd] (hd' :: tl')) = tl
h' : splitOnP (fun x => x == hd) tl = hd' :: tl'
⊢ join (intersperse [hd] ([] :: splitOnP (fun x => x == hd) tl)) = hd :: tl
simp [ih, join, h']