diff --git a/templates/contribute/index.md b/templates/contribute/index.md
index e40f22489..edb31be92 100644
--- a/templates/contribute/index.md
+++ b/templates/contribute/index.md
@@ -199,7 +199,8 @@ whether to proceed at all.
 
 - The **"blocked-by-other-PR"** label means that some specific other PR(s) should be resolved before addressing this one. To add the "blocked-by-other-PR" label to your PR, include the PR numbers of the dependencies in the PR comment (following the example hidden in the comment there) so that others can see at a glance which PRs should be reviewed first. The label will be added automatically by a bot and will also be removed automatically when the other PRs have been merged. PRs with this label do not appear on the review queue.
 
-- The **easy** label should be used to mark PRs that can be immediately approved. Maintainers and reviewers often look at easy PRs first to keep the queue flowing. Easy PRs typically add a single lemma, correct typos in documentation, or similar. If you have any doubt whether your PR is trivial you should not add this label. In particular, a PR is generally *not* easy if the diff is more than 25 lines, it adds any definitions or new files, or it adds any `simp` lemmas or instances that are not immediately analogous to existing `simp` lemmas or instances.
+- The **easy** label should be used to mark PRs that can be immediately approved. Maintainers and reviewers often look at easy PRs first to keep the queue flowing. Easy PRs typically add a single lemma, correct typos in documentation, or similar. If you have any doubt whether your PR is trivial, you should not add this label.
+In particular, a PR is generally *not* easy if the diff is more than 25 lines, it changes any existing definitions or theorem statements, it adds any definitions or new files, or it adds any `simp` lemmas or instances that are not immediately analogous to existing `simp` lemmas or instances. (If they are immediately analogous, you should put such context in the PR description anyway.) Note that a small diff does not automatically make a PR easy!
 
 - The **delegated** label means that a maintainer has issued the "bors delegate" (or "bors d+") command. The author of the PR
 should now merge the PR themselves once any final requested changes have been made, and CI has succeeded. They can do this using