Noisy proofs relying on loopholes in flexible-tactic linter #724

LeanPool's policies require code to pass the mathlib standard linter set without warnings, including the "flexible tactic" linter. However, due to an oversight in mathlib, while simp counts as flexible, its variant simp? does not; and some LeanPool projects uses this to smuggle unreliable code past the linter (since the output of simp? is classed as info, not warning, and thus does not cause a CI fail). For example in
LeanPool/PolynomialMethodRestrictedSums/CompressedSizesRestrictedSum.lean we have

refine le_antisymm ?_ ?_ <;> simp_all? +decide [Finset.max']
· exact fun i hi => not_lt.1 fun contra => not_lt_of_ge (right i contra) hi
· exact ⟨j, left, le_rfl⟩

This produces an info message in CI; but deleting the question-mark on simp_all? produces a flexible-tactic warning. So this code should not have passed the quality gate.

I propose two fixes:

• Submit a Mathlib PR adding simp? and variants (e.g. simp_all?) to the flexible-tactic linter list (see [Merged by Bors] - feat(Tactic/Linter/Flexible): flag simp? and friends as flexible leanprover-community/mathlib4#45414)
• Add a CI gate in LeanPool's quality scripts preventing use of simp?, rw?, etc, as these tactics are not intended for use in production code.