case h.h.h.h
α : Type u_1
n m : Nat
l : List α
⊢ dropSlice n m l = dropSliceTR n m l
⊢ @dropSlice = @dropSliceTR
funext α n m l
case h.h.h.h
α : Type u_1
n m : Nat
l : List α
⊢ dropSlice n m l =
    match m with
    | 0 => l
    | succ m => dropSliceTR.go l m l n #[]
case h.h.h.h
α : Type u_1
n m : Nat
l : List α
⊢ dropSlice n m l = dropSliceTR n m l
simp [dropSliceTR]
case h.h.h.h.h_1
α : Type u_1
n : Nat
l : List α
m✝ : Nat
⊢ dropSlice n 0 l = l

case h.h.h.h.h_2
α : Type u_1
n : Nat
l : List α
m✝¹ m✝ : Nat
⊢ dropSlice n (succ m✝) l = dropSliceTR.go l m✝ l n #[]
case h.h.h.h
α : Type u_1
n m : Nat
l : List α
⊢ dropSlice n m l =
    match m with
    | 0 => l
    | succ m => dropSliceTR.go l m l n #[]
split
case h.h.h.h.h_2
α : Type u_1
n : Nat
l : List α
m✝¹ m✝ : Nat
⊢ dropSlice n (succ m✝) l = dropSliceTR.go l m✝ l n #[]
case h.h.h.h.h_1
α : Type u_1
n : Nat
l : List α
m✝ : Nat
⊢ dropSlice n 0 l = l

case h.h.h.h.h_2
α : Type u_1
n : Nat
l : List α
m✝¹ m✝ : Nat
⊢ dropSlice n (succ m✝) l = dropSliceTR.go l m✝ l n #[]
{ rw [dropSlice_zero₂] }
case h.h.h.h.h_2
α : Type u_1
n : Nat
l : List α
m✝ m : Nat
⊢ dropSlice n (succ m) l = dropSliceTR.go l m l n #[]
case h.h.h.h.h_2
α : Type u_1
n : Nat
l : List α
m✝¹ m✝ : Nat
⊢ dropSlice n (succ m✝) l = dropSliceTR.go l m✝ l n #[]
rename_i m
case h.h.h.h.h_2
α : Type u_1
n : Nat
l : List α
m✝ m : Nat
⊢ dropSlice n (succ m) l = dropSliceTR.go l m l n #[]
case h.h.h.h.h_2
α : Type u_1
n : Nat
l : List α
m✝ m : Nat
⊢ dropSlice n (succ m) l = dropSliceTR.go l m l n #[]
let rec go (acc) : ∀ xs n, l = acc.data ++ xs →
  dropSliceTR.go l m xs n acc = acc.data ++ xs.dropSlice n (m+1)
| [],    n
| _::xs, 0 => fun h => by simp [dropSliceTR.go, dropSlice, h]
| x::xs, n+1 => by simp [dropSliceTR.go, dropSlice]; intro h; rw [go _ xs]; {simp}; simp [h]
no goals
case h.h.h.h.h_2
α : Type u_1
n : Nat
l : List α
m✝ m : Nat
⊢ dropSlice n (succ m) l = dropSliceTR.go l m l n #[]
exact (go #[] _ _ rfl).symm
no goals
α : Type u_1
n : Nat
l : List α
m✝ m : Nat
acc : Array α
head✝ : α
xs : List α
h : l = acc.data ++ head✝ :: xs
⊢ dropSliceTR.go l m (head✝ :: xs) 0 acc = acc.data ++ dropSlice 0 (m + 1) (head✝ :: xs)
simp [dropSliceTR.go, dropSlice, h]
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
⊢ l = acc.data ++ x :: xs → dropSliceTR.go l m xs n (Array.push acc x) = acc.data ++ x :: dropSlice n (m + 1) xs
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
⊢ l = acc.data ++ x :: xs → dropSliceTR.go l m (x :: xs) (n + 1) acc = acc.data ++ dropSlice (n + 1) (m + 1) (x :: xs)
simp [dropSliceTR.go, dropSlice]
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.data ++ x :: xs
⊢ dropSliceTR.go l m xs n (Array.push acc x) = acc.data ++ x :: dropSlice n (m + 1) xs
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
⊢ l = acc.data ++ x :: xs → dropSliceTR.go l m xs n (Array.push acc x) = acc.data ++ x :: dropSlice n (m + 1) xs
intro h
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.data ++ x :: xs
⊢ (Array.push acc x).data ++ dropSlice n (m + 1) xs = acc.data ++ x :: dropSlice n (m + 1) xs

case a
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.data ++ x :: xs
⊢ dropSliceTR.go l m xs n (Array.push acc x) = acc.data ++ x :: dropSlice n (m + 1) xs
rw [go _ xs]
case a
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.data ++ x :: xs
⊢ (Array.push acc x).data ++ dropSlice n (m + 1) xs = acc.data ++ x :: dropSlice n (m + 1) xs

case a
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
{simp}
no goals
case a
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
simp [h]