Theorem: List.modifyLast_singleton (One.lean)

State before:
α : Type u_1
f : α → α
a : α
⊢ modifyLast f [a] = [f a]
Tactic:
rw [← nil_append [a], modifyLast_append_one, nil_append]
State after:
no goals