Please include a summary of the changes made in the PR description, as that text will become the commit message. You are also encouraged to append the following co-authorship template if you'd like to acknowledge suggestions / commits made by other users:
Co-authored-by: name <name@example.com>
Make sure you have:
- reviewed and applied the coding style: coding, naming
- reviewed and applied the documentation requirements
- for tactics:
- added or adapted documentation in the tactic doc entries
- write an example of use of the new feature in test/tactics.lean or another test file
- 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
If you're confused by comments on your PR like bors r+ or bors d+, please see our notes on bors for information on our merging workflow.