Possible change to multigoal linter

Stream: mathlib4

[Alastair Irving]

I noticed recently that the multigoal linter does not apply inside have or suffices blocks. This has already been reported as an issue, #20081. The problem seems to be that both tactics expand to the focus tactic and currently that's listed under ignoreBranch rather than exclusions in the linter.

In #30470 I tried the simple experiment of moving focus to exclusions rather than ignoreBranch. It appears to be doing the right thing. It identifies a number of places in Mathlib where multiple goals are created inside of have blocks. I haven't checked all of them so can't be sure there aren't false positives.

Please can someone with more expert knowledge comment on whether this change is reasonable or if there's a good reason for having focus in ignoreBranch? If it sounds reasonable then we should make the change and fix the newly identified failures.

[Damiano Testa]

I think that the reason for this is just historical. When developing the linter, there were lots of exceptions, so I made the decision of trying to minimize fixes to existing code. This helped showcase that the linter was doing the correct thing and also helped making mathlib compliant and merge the linter.

[Damiano Testa]

Having looked at your proposed change, I think that it is the correct thing to do and there are two issues to check:

• if there are false positives, think very carefully about whether they are unavoidable;
• make sure that you run !bench, once the PR is stable, to expose any possible performance implication.

[Alastair Irving]

Thanks, I'll look at updating my PR when I get time and will follow your suggestions.

[Alastair Irving]

OK, I think #30470 is ready for review. I fixed all the new instances of the lint (mostly they were trivial) and added a test. Its just waiting for bench to run now.