Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-26 21:16 7b938899

View on Github →

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.

Estimated changes

modified theorem list.last_append
modified theorem list.last_concat
modified theorem list.last_cons_cons
modified theorem list.last_singleton