Theorem: LoVe.take_take (LoVe/Labs/Lab4Solution.lean)

State before:
α : Type
x✝ : List α
⊢ take 0 (take 0 x✝) = take 0 x✝
Tactic:
rfl
State after:
no goals

State before:
α : Type
n✝ : ℕ
⊢ take (n✝ + 1) (take (n✝ + 1) []) = take (n✝ + 1) []
Tactic:
rfl
State after:
no goals

State before:
α : Type
m : ℕ
x : α
xs : List α
⊢ take (m + 1) (take (m + 1) (x :: xs)) = take (m + 1) (x :: xs)
Tactic:
simp [take, take_take m xs]
State after:
no goals