Theorem: List.modifyLast_nil (One.lean)

State before:
α✝ : Type u_1
f : α✝ → α✝
⊢ modifyLast f [] = []
Tactic:
unfold modifyLast modifyLast.go
State after:
α✝ : Type u_1
f : α✝ → α✝
⊢ [] = []

State before:
α✝ : Type u_1
f : α✝ → α✝
⊢ [] = []
Tactic:
simp only
State after:
no goals