TO CONTRIBUTORS:

Make sure you have:

  * [ ] reviewed and applied the coding style: [coding](https://github.com/leanprover/mathlib/blob/master/docs/contribute/style.md), [naming](https://github.com/leanprover/mathlib/blob/master/docs/contribute/naming.md)
  * [ ] reviewed and applied [the documentation requirements](https://github.com/leanprover/mathlib/blob/master/docs/contribute/doc.md)
  * [ ] for tactics:
     * [ ] added or adapted documentation in [tactics.md](https://github.com/leanprover/mathlib/blob/master/docs/tactics.md)
     * [ ] write an example of use of the new feature in [tactics.lean](https://github.com/leanprover/mathlib/blob/master/test/tactics.lean)
  * [ ] make sure definitions and lemmas are put in the right files
  * [ ] make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: [code review check list](https://github.com/leanprover/mathlib/blob/master/docs/contribute/code-review.md)
