ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls : ls ≠ []
⊢ splitOn x (join (intersperse [x] ls)) = ls
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls : ls ≠ []
⊢ splitOn x (intercalate [x] ls) = ls
simp only [intercalate]
case nil
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hx : ∀ (l : List α), l ∈ [] → ¬x ∈ l
hls : [] ≠ []
⊢ splitOn x (join (intersperse [x] [])) = []

case cons
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd : List α
tl : List (List α)
ih : (∀ (l : List α), l ∈ tl → ¬x ∈ l) → tl ≠ [] → splitOn x (join (intersperse [x] tl)) = tl
hx : ∀ (l : List α), l ∈ hd :: tl → ¬x ∈ l
hls : hd :: tl ≠ []
⊢ splitOn x (join (intersperse [x] (hd :: tl))) = hd :: tl
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls : ls ≠ []
⊢ splitOn x (join (intersperse [x] ls)) = ls
induction' ls with hd tl ih
case cons.nil
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (join (intersperse [x] [])) = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
⊢ splitOn x (join (intersperse [x] [hd])) = [hd]

case cons.cons
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
⊢ splitOn x (join (intersperse [x] (hd :: head✝ :: tail✝))) = hd :: head✝ :: tail✝
case cons
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd : List α
tl : List (List α)
ih : (∀ (l : List α), l ∈ tl → ¬x ∈ l) → tl ≠ [] → splitOn x (join (intersperse [x] tl)) = tl
hx : ∀ (l : List α), l ∈ hd :: tl → ¬x ∈ l
hls : hd :: tl ≠ []
⊢ splitOn x (join (intersperse [x] (hd :: tl))) = hd :: tl
cases tl
no goals
case nil
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hx : ∀ (l : List α), l ∈ [] → ¬x ∈ l
hls : [] ≠ []
⊢ splitOn x (join (intersperse [x] [])) = []
contradiction
case cons.nil
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (join (intersperse [x] [])) = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
⊢ splitOn x hd = [hd]
case cons.nil
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (join (intersperse [x] [])) = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
⊢ splitOn x (join (intersperse [x] [hd])) = [hd]
suffices hd.splitOn x = [hd] by simpa [join]
case cons.nil
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (join (intersperse [x] [])) = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
⊢ ∀ (x_1 : α), x_1 ∈ hd → ¬(x_1 == x) = true
case cons.nil
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (join (intersperse [x] [])) = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
⊢ splitOn x hd = [hd]
refine' splitOnP_eq_single _ _ _
case cons.nil
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (join (intersperse [x] [])) = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
y : α
hy : y ∈ hd
H : (y == x) = true
⊢ False
case cons.nil
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (join (intersperse [x] [])) = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
⊢ ∀ (x_1 : α), x_1 ∈ hd → ¬(x_1 == x) = true
intro y hy H
case cons.nil
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (join (intersperse [x] [])) = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
y : α
hy : x ∈ hd
H : (y == x) = true
⊢ False
case cons.nil
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (join (intersperse [x] [])) = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
y : α
hy : y ∈ hd
H : (y == x) = true
⊢ False
rw [eq_of_beq H] at hy
case cons.nil
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (join (intersperse [x] [])) = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
y : α
hy : x ∈ hd
H : (y == x) = true
⊢ hd ∈ [hd]
case cons.nil
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (join (intersperse [x] [])) = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
y : α
hy : x ∈ hd
H : (y == x) = true
⊢ False
refine' hx hd _ hy
no goals
case cons.nil
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (join (intersperse [x] [])) = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
y : α
hy : x ∈ hd
H : (y == x) = true
⊢ hd ∈ [hd]
simp
no goals
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd : List α
ih : (∀ (l : List α), l ∈ [] → ¬x ∈ l) → [] ≠ [] → splitOn x (join (intersperse [x] [])) = []
hx : ∀ (l : List α), l ∈ [hd] → ¬x ∈ l
hls : [hd] ≠ []
this : splitOn x hd = [hd]
⊢ splitOn x (join (intersperse [x] [hd])) = [hd]
simpa [join]
case cons.cons
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
⊢ splitOn x (hd ++ x :: join (intersperse [x] (head✝ :: tail✝))) = hd :: head✝ :: tail✝
case cons.cons
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
⊢ splitOn x (join (intersperse [x] (hd :: head✝ :: tail✝))) = hd :: head✝ :: tail✝
simp only [intersperse_cons_cons, singleton_append, join]
case cons.cons.specialize_1
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
⊢ ∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l

case cons.cons.specialize_2
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
⊢ head✝ :: tail✝ ≠ []

case cons.cons
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
ih : splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
⊢ splitOn x (hd ++ x :: join (intersperse [x] (head✝ :: tail✝))) = hd :: head✝ :: tail✝
case cons.cons
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
⊢ splitOn x (hd ++ x :: join (intersperse [x] (head✝ :: tail✝))) = hd :: head✝ :: tail✝
specialize ih _ _
case cons.cons
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
ih : splitOn x (join (intersperse [x] (head✝ :: tail✝))) = 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 :: join (intersperse [x] (head✝ :: tail✝))) = hd :: head✝ :: tail✝
case cons.cons
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
ih : splitOn x (join (intersperse [x] (head✝ :: tail✝))) = 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 :: join (intersperse [x] (head✝ :: tail✝))) = hd :: head✝ :: tail✝

case h
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
ih : splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
⊢ ∀ (x_1 : α), x_1 ∈ hd → ¬(fun x_2 => x_2 == x) x_1 = true
case h =>
  intro y hy H
  rw [eq_of_beq H] at hy
  exact hx hd (.head _) hy
case cons.cons
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
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) (join (intersperse [x] (head✝ :: tail✝))) = 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 :: join (intersperse [x] (head✝ :: tail✝))) = hd :: head✝ :: tail✝
case cons.cons
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
ih : splitOn x (join (intersperse [x] (head✝ :: tail✝))) = 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 :: join (intersperse [x] (head✝ :: tail✝))) = hd :: head✝ :: tail✝
simp only [splitOn] at ih⊢
no goals
case cons.cons
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
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) (join (intersperse [x] (head✝ :: tail✝))) = 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 :: join (intersperse [x] (head✝ :: tail✝))) = hd :: head✝ :: tail✝
rw [this, ih]
case cons.cons.specialize_1
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
l : List α
hl : l ∈ head✝ :: tail✝
⊢ ¬x ∈ l
case cons.cons.specialize_1
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
⊢ ∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l
intro l hl
case cons.cons.specialize_1
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
l : List α
hl : l ∈ head✝ :: tail✝
⊢ l ∈ hd :: head✝ :: tail✝
case cons.cons.specialize_1
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
l : List α
hl : l ∈ head✝ :: tail✝
⊢ ¬x ∈ l
apply hx l
case cons.cons.specialize_1
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
l : List α
hl : l = head✝ ∨ l ∈ tail✝
⊢ l = hd ∨ l = head✝ ∨ l ∈ tail✝
case cons.cons.specialize_1
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
l : List α
hl : l ∈ head✝ :: tail✝
⊢ l ∈ hd :: head✝ :: tail✝
simp at hl⊢
no goals
case cons.cons.specialize_1
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
l : List α
hl : l = head✝ ∨ l ∈ tail✝
⊢ l = hd ∨ l = head✝ ∨ l ∈ tail✝
exact Or.inr hl
no goals
case cons.cons.specialize_2
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
⊢ head✝ :: tail✝ ≠ []
exact List.noConfusion
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
ih : splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
y : α
hy : y ∈ hd
H : (fun x_1 => x_1 == x) y = true
⊢ False
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
ih : splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
⊢ ∀ (x_1 : α), x_1 ∈ hd → ¬(fun x_2 => x_2 == x) x_1 = true
intro y hy H
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
ih : splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
y : α
hy : x ∈ hd
H : (fun x_1 => x_1 == x) y = true
⊢ False
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
ih : splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
y : α
hy : y ∈ hd
H : (fun x_1 => x_1 == x) y = true
⊢ False
rw [eq_of_beq H] at hy
no goals
ι : Type ?u.310123
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Bool
xs ys : List α
ls : List (List α)
f : List α → List α
inst✝ : DecidableEq α
x : α
hx✝ : ∀ (l : List α), l ∈ ls → ¬x ∈ l
hls✝ : ls ≠ []
hd head✝ : List α
tail✝ : List (List α)
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
ih : splitOn x (join (intersperse [x] (head✝ :: tail✝))) = head✝ :: tail✝
y : α
hy : x ∈ hd
H : (fun x_1 => x_1 == x) y = true
⊢ False
exact hx hd (.head _) hy