Theorem: List.getCons?_eq_some (LeanColls/Data/List.lean)

State before:
α : Type u_1
x : α
xs c : List α
⊢ c.getCons? = some (x, xs) ↔ c = x :: xs
Tactic:
cases c <;> simp [getCons?]
State after:
no goals