-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem take_eq_takeTR : @take = @takeTR

Proof state:
case h.h.h
α : Type u_1
n : Nat
l : List α
⊢ take n l = takeTR.go l l n #[]

Tactic:
suffices ∀ xs acc, l = acc.toList ++ xs → takeTR.go l xs n acc = acc.toList ++ xs.take n from
  (this l #[] (by simp)).symm

Result:
case h.h.h
α : Type u_1
n : Nat
l : List α
⊢ ∀ (xs : List α) (acc : Array α), l = acc.toList ++ xs → takeTR.go l xs n acc = acc.toList ++ take n xs

Proof state:
case h.h.h.cons.succ
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → takeTR.go l xs n acc = acc.toList ++ take n xs
acc : Array α
n : Nat
⊢ l = acc.toList ++ x :: xs → takeTR.go l xs n (acc.push x) = acc.toList ++ x :: take n xs

Tactic:
intro h

Result:
case h.h.h.cons.succ
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → takeTR.go l xs n acc = acc.toList ++ take n xs
acc : Array α
n : Nat
h : l = acc.toList ++ x :: xs
⊢ takeTR.go l xs n (acc.push x) = acc.toList ++ x :: take n xs

Proof state:
case h.h.h
α : Type u_1
n : Nat
l : List α
⊢ ∀ (xs : List α) (acc : Array α), l = acc.toList ++ xs → takeTR.go l xs n acc = acc.toList ++ take n xs

Tactic:
intro xs

Result:
case h.h.h
α : Type u_1
n : Nat
l xs : List α
⊢ ∀ (acc : Array α), l = acc.toList ++ xs → takeTR.go l xs n acc = acc.toList ++ take n xs

Proof state:
case h.h.h.cons.zero
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → takeTR.go l xs n acc = acc.toList ++ take n xs
acc : Array α
⊢ l = acc.toList ++ x :: xs → acc.toList = acc.toList ++ []

Tactic:
simp

Result:
no goals

Proof state:
case h.h.h
α : Type u_1
n : Nat
l xs : List α
⊢ ∀ (acc : Array α), l = acc.toList ++ xs → takeTR.go l xs n acc = acc.toList ++ take n xs

Tactic:
induction xs generalizing n with intro acc
| nil => cases n <;> simp [take, takeTR.go]
| cons x xs IH =>
cases n with simp only [take, takeTR.go]
| zero => simp
| succ n => intro h; rw [IH] <;> simp_all

Result:
no goals

Proof state:
⊢ @take = @takeTR

Tactic:
funext α n l

Result:
case h.h.h
α : Type u_1
n : Nat
l : List α
⊢ take n l = takeTR n l

Proof state:
case h.h.h
α : Type u_1
n : Nat
l : List α
⊢ take n l = takeTR n l

Tactic:
simp [takeTR]

Result:
case h.h.h
α : Type u_1
n : Nat
l : List α
⊢ take n l = takeTR.go l l n #[]

Proof state:
case h.h.h.cons.succ
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → takeTR.go l xs n acc = acc.toList ++ take n xs
acc : Array α
n : Nat
h : l = acc.toList ++ x :: xs
⊢ takeTR.go l xs n (acc.push x) = acc.toList ++ x :: take n xs

Tactic:
rw [IH] <;> simp_all

Result:
no goals

Proof state:
case h.h.h.cons
α : Type u_1
l : List α
x : α
xs : List α
IH : ∀ (n : Nat) (acc : Array α), l = acc.toList ++ xs → takeTR.go l xs n acc = acc.toList ++ take n xs
n : Nat
acc : Array α
⊢ l = acc.toList ++ x :: xs → takeTR.go l (x :: xs) n acc = acc.toList ++ take n (x :: xs)

Tactic:
cases n with simp only [take, takeTR.go]
| zero => simp
| succ n => intro h; rw [IH] <;> simp_all

Result:
no goals

Proof state:
case h.h.h.nil
α : Type u_1
l : List α
n : Nat
acc : Array α
⊢ l = acc.toList ++ [] → takeTR.go l [] n acc = acc.toList ++ take n []

Tactic:
cases n <;> simp [take, takeTR.go]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
this : ∀ (xs : List α) (acc : Array α), l = acc.toList ++ xs → takeTR.go l xs n acc = acc.toList ++ take n xs
⊢ l = #[].toList ++ l

Tactic:
simp

Result:
no goals