Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-25 10:07 f43bd45e

View on Github →

fix(tactic/lint/simp): only head-beta reduce, don't whnf (#4237) This is necessary to accept simp lemmas like injective reverse.

Estimated changes

modified theorem finset.ne_empty_of_mem
modified theorem list.cons_injective
modified theorem list.length_injective
modified theorem list.length_injective_iff
modified theorem list.reverse_injective