mathlib

7b938899 - refactor(data/list/basic): Remove many redundant hypotheses (#12950)

refactor(data/list/basic): Remove many redundant hypotheses (#12950) Many theorems about `last` required arguments proving that certain things were not equal to `nil`, when in fact this was always the case. These hypotheses have been removed and replaced with the corresponding proofs.