case h.h.h
α : Type u_1
sep : List α
l : List (List α)
⊢ intercalate sep l = intercalateTR sep l
⊢ @intercalate = @intercalateTR
funext α sep l
case h.h.h
α : Type u_1
sep : List α
l : List (List α)
⊢ join (intersperse sep l) =
    match l with
    | [] => []
    | [x] => x
    | x :: xs => intercalateTR.go (toArray sep) x xs #[]
case h.h.h
α : Type u_1
sep : List α
l : List (List α)
⊢ intercalate sep l = intercalateTR sep l
simp [intercalate, intercalateTR]
no goals
case h.h.h
α : Type u_1
sep : List α
l : List (List α)
⊢ join (intersperse sep l) =
    match l with
    | [] => []
    | [x] => x
    | x :: xs => intercalateTR.go (toArray sep) x xs #[]
match l with
| [] => rfl
| [_] => simp
| x::y::xs =>
  let rec go {acc x} : ∀ xs,
    intercalateTR.go sep.toArray x xs acc = acc.data ++ join (intersperse sep (x::xs))
  | [] => by simp [intercalateTR.go]
  | _::_ => by simp [intercalateTR.go, go]
  simp [intersperse, go]
no goals
α : Type u_1
sep : List α
l : List (List α)
⊢ join (intersperse sep []) =
    match [] with
    | [] => []
    | [x] => x
    | x :: xs => intercalateTR.go (toArray sep) x xs #[]
rfl
no goals
α : Type u_1
sep : List α
l : List (List α)
head✝ : List α
⊢ join (intersperse sep [head✝]) =
    match [head✝] with
    | [] => []
    | [x] => x
    | x :: xs => intercalateTR.go (toArray sep) x xs #[]
simp
α : Type u_1
sep : List α
l : List (List α)
x y : List α
xs : List (List α)
⊢ join (intersperse sep (x :: y :: xs)) =
    match x :: y :: xs with
    | [] => []
    | [x] => x
    | x :: xs => intercalateTR.go (toArray sep) x xs #[]
α : Type u_1
sep : List α
l : List (List α)
x y : List α
xs : List (List α)
⊢ join (intersperse sep (x :: y :: xs)) =
    match x :: y :: xs with
    | [] => []
    | [x] => x
    | x :: xs => intercalateTR.go (toArray sep) x xs #[]
let rec go {acc x} : ∀ xs,
  intercalateTR.go sep.toArray x xs acc = acc.data ++ join (intersperse sep (x::xs))
| [] => by simp [intercalateTR.go]
| _::_ => by simp [intercalateTR.go, go]
no goals
α : Type u_1
sep : List α
l : List (List α)
x y : List α
xs : List (List α)
⊢ join (intersperse sep (x :: y :: xs)) =
    match x :: y :: xs with
    | [] => []
    | [x] => x
    | x :: xs => intercalateTR.go (toArray sep) x xs #[]
simp [intersperse, go]
no goals
α : Type u_1
sep : List α
l : List (List α)
x✝ y : List α
xs : List (List α)
acc : Array α
x : List α
⊢ intercalateTR.go (toArray sep) x [] acc = acc.data ++ join (intersperse sep [x])
simp [intercalateTR.go]
no goals
α : Type u_1
sep : List α
l : List (List α)
x✝ y : List α
xs : List (List α)
acc : Array α
x head✝ : List α
tail✝ : List (List α)
⊢ intercalateTR.go (toArray sep) x (head✝ :: tail✝) acc = acc.data ++ join (intersperse sep (x :: head✝ :: tail✝))
simp [intercalateTR.go, go]