mathlib3

3c4dcd1a - one less lemma in some_lemmas.lean