add `mergeWithGrind` linter

I don't want to commit to the entire new `weeklyLintSet`, but this linter that is currently the only one included seems like a good addition. This is a small change, it only lints three proofs currently (and all seem like improvements). We would add this on the next Mathlib release. 