-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem dropSlice_eq_dropSliceTR : @dropSlice = @dropSliceTR

Proof state:
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 m✝.succ l = dropSliceTR.go l m✝ l n #[]

Tactic:
{ rw [dropSlice_zero₂] }

Result:
case h.h.h.h.h_2
α : Type u_1
n : Nat
l : List α
m✝¹ m✝ : Nat
⊢ dropSlice n m✝.succ l = dropSliceTR.go l m✝ l n #[]

Proof state:
⊢ @dropSlice = @dropSliceTR

Tactic:
funext α n m l

Result:
case h.h.h.h
α : Type u_1
n m : Nat
l : List α
⊢ dropSlice n m l = dropSliceTR n m l

Proof state:
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
⊢ l = acc.toList ++ x :: xs → dropSliceTR.go l m xs n (acc.push x) = acc.toList ++ x :: dropSlice n (m + 1) xs

Tactic:
intro h

Result:
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.toList ++ x :: xs
⊢ dropSliceTR.go l m xs n (acc.push x) = acc.toList ++ x :: dropSlice n (m + 1) xs

Proof state:
case a
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.toList ++ x :: xs
⊢ l = (acc.push x).toList ++ xs

Tactic:
simp [h]

Result:
no goals

Proof state:
case h.h.h.h.h_2
α : Type u_1
n : Nat
l : List α
m✝¹ m✝ : Nat
⊢ dropSlice n m✝.succ l = dropSliceTR.go l m✝ l n #[]

Tactic:
rename_i m

Result:
case h.h.h.h.h_2
α : Type u_1
n : Nat
l : List α
m✝ m : Nat
⊢ dropSlice n m.succ l = dropSliceTR.go l m l n #[]

Proof state:
case h.h.h.h.h_2
α : Type u_1
n : Nat
l : List α
m✝ m : Nat
⊢ dropSlice n m.succ l = dropSliceTR.go l m l n #[]

Tactic:
exact (go #[] _ _ rfl).symm

Result:
no goals

Proof state:
case h.h.h.h
α : Type u_1
n m : Nat
l : List α
⊢ dropSlice n m l =
    match m with
    | 0 => l
    | m.succ => dropSliceTR.go l m l n #[]

Tactic:
split

Result:
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 m✝.succ l = dropSliceTR.go l m✝ l n #[]

Proof state:
case h.h.h.h
α : Type u_1
n m : Nat
l : List α
⊢ dropSlice n m l = dropSliceTR n m l

Tactic:
simp [dropSliceTR]

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

Proof state:
case h.h.h.h.h_1
α : Type u_1
n : Nat
l : List α
m✝ : Nat
⊢ dropSlice n 0 l = l

Tactic:
rw [dropSlice_zero₂]

Result:
no goals

Proof state:
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.toList ++ x :: xs
⊢ (acc.push x).toList ++ dropSlice n (m + 1) xs = acc.toList ++ x :: dropSlice n (m + 1) xs

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
⊢ l = acc.toList ++ x :: xs →
    dropSliceTR.go l m (x :: xs) (n + 1) acc = acc.toList ++ dropSlice (n + 1) (m + 1) (x :: xs)

Tactic:
simp [dropSliceTR.go, dropSlice]

Result:
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
⊢ l = acc.toList ++ x :: xs → dropSliceTR.go l m xs n (acc.push x) = acc.toList ++ x :: dropSlice n (m + 1) xs

Proof state:
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.toList ++ x :: xs
⊢ dropSliceTR.go l m xs n (acc.push x) = acc.toList ++ x :: dropSlice n (m + 1) xs

Tactic:
rw [go _ xs]

Result:
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.toList ++ x :: xs
⊢ (acc.push x).toList ++ dropSlice n (m + 1) xs = acc.toList ++ 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.toList ++ x :: xs
⊢ l = (acc.push x).toList ++ xs

Proof state:
α : Type u_1
n : Nat
l : List α
m✝ m : Nat
acc : Array α
head✝ : α
xs : List α
h : l = acc.toList ++ head✝ :: xs
⊢ dropSliceTR.go l m (head✝ :: xs) 0 acc = acc.toList ++ dropSlice 0 (m + 1) (head✝ :: xs)

Tactic:
simp [dropSliceTR.go, dropSlice, h]

Result:
no goals

Proof state:
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.toList ++ x :: xs
⊢ (acc.push x).toList ++ dropSlice n (m + 1) xs = acc.toList ++ 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.toList ++ x :: xs
⊢ l = (acc.push x).toList ++ xs

Tactic:
{simp}

Result:
case a
α : Type u_1
n✝ : Nat
l : List α
m✝ m : Nat
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.toList ++ x :: xs
⊢ l = (acc.push x).toList ++ xs