case h.h.h
α : Type u_1
xs : List α
ns : List Nat
⊢ takeList xs ns = takeListTR xs ns
⊢ @takeList = @takeListTR
funext α xs ns
case h.h.h
α : Type u_1
xs : List α
ns : List Nat
⊢ takeList xs ns = takeListTR.go ns xs #[]
case h.h.h
α : Type u_1
xs : List α
ns : List Nat
⊢ takeList xs ns = takeListTR xs ns
simp [takeListTR]
case h.h.h
α : Type u_1
xs : List α
ns : List Nat
⊢ takeList xs ns = takeListTR.go ns xs #[]
case h.h.h
α : Type u_1
xs : List α
ns : List Nat
⊢ takeList xs ns = takeListTR.go ns xs #[]
let rec go (acc) : ∀ ns xs, @takeListTR.go α ns xs acc =
    let (l, r) := xs.takeList ns; (acc.toList ++ l, r)
| [], xs => by simp [takeListTR.go, takeList]
| n::ns, xs => by simp [takeListTR.go, takeList, go _ ns]
no goals
case h.h.h
α : Type u_1
xs : List α
ns : List Nat
⊢ takeList xs ns = takeListTR.go ns xs #[]
simp [takeListTR, go]
no goals
α : Type u_1
xs✝ : List α
ns : List Nat
acc : Array (List α)
xs : List α
⊢ takeListTR.go [] xs acc =
    match takeList xs [] with
    | (l, r) => (Array.toList acc ++ l, r)
simp [takeListTR.go, takeList]
no goals
α : Type u_1
xs✝ : List α
ns✝ : List Nat
acc : Array (List α)
n : Nat
ns : List Nat
xs : List α
⊢ takeListTR.go (n :: ns) xs acc =
    match takeList xs (n :: ns) with
    | (l, r) => (Array.toList acc ++ l, r)
simp [takeListTR.go, takeList, go _ ns]