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

State before:
α : Type u_1
⊢ take 1 [] = []
Tactic:
rw [take]
State after:
no goals