Commit 2026-02-21 23:47 0c5ce993

chore: weekly lints for 2026-02-16 (#35490) Changes suggested by the mergeWithGrind linter, from the weekly job posted at #mathlib4 > Weekly linting log @ 💬. As suggested by @Vierkantor, I have used the linter.tacticAnalysis.mergeWithGrind option to turn off the linter in two theorems: one where there was a comment about not making this change for performance reasons and another that appears to be a bug with the linter. Now that there is a precedent for using the grind interactive mode in Mathlib, I have used this in one proof where it results in fewer calls to grind and a clearer proof.