linter.fugue.bulletSubgoals

A tactic that splits the goal is followed by one · per branch — always. Run unbulleted, nothing marks where one branch ends and the next begins, and a later edit to the first branch silently changes which goal the rest applies to.

This is a port of Mathlib's linter.style.multiGoal: its getManyGoals walk and its exclusions / ignoreBranch sets are reproduced verbatim (they have no extension point upstream), then exclusions gains the project's deliberately-many-goals combinators — the tac_selector (1,2: tac, all: tac) and the <;> [t₁ | t₂] pipe. all_goals / any_goals stay in ignoreBranch, so this linter is quiet on them and linter.fugue.goalSelector is what flags them. Do not also enable linter.style.multiGoal.