no goals
α : Type u_1
l : List α
⊢ length (take 0 l) = min 0 (length l)
simp [Nat.zero_min]
no goals
α : Type u_1
n : Nat
⊢ length (take (succ n) []) = min (succ n) (length [])
simp [Nat.min_zero]
no goals
α : Type u_1
n : Nat
head✝ : α
l : List α
⊢ length (take (succ n) (head✝ :: l)) = min (succ n) (length (head✝ :: l))
simp [Nat.min_succ_succ, add_one, length_take]