Theorem: List.nil_isSuffix (One.lean)

State before:
α✝ : Type u_1
l : List α✝
⊢ [] <:+ l
Tactic:
unfold List.isSuffix
State after:
α✝ : Type u_1
l : List α✝
⊢ ∃ t, t ++ [] = l

State before:
α✝ : Type u_1
l : List α✝
⊢ ∃ t, t ++ [] = l
Tactic:
simp only [append_nil, exists_eq]
State after:
no goals