Theorem: list_take_nil (Katydid/Std/Lists.lean)

State before:
α : Type u
n : ℕ
⊢ take n [] = []
Tactic:
cases n with
| zero => rfl
| succ => rfl
State after:
no goals

State before:
case zero
α : Type u
⊢ take zero [] = []
Tactic:
rfl
State after:
no goals

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