Theorem: List.getRest_nil (One.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ getRest l [] = some l
Tactic:
unfold getRest
State after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ (match l, [] with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l

State before:
α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ (match l, [] with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l
Tactic:
simp only
State after:
no goals