linter.style.multiGoal ignores suffices ... by branch

[dwrensha]

import Mathlib.Tactic.Linter.Multigoal

set_option linter.style.multiGoal true

example : 0 = 0 ∧ 0 = 0 := by
  refine ⟨?_, ?_⟩
  rfl -- The linter flags this line, as expected.
  rfl


example : 0 = 0 ∧ 0 = 0 ∧ 0 = 0 := by
  suffices h : 0 = 0 by
    refine ⟨h, ?_, ?_⟩
    rfl -- I expect to see the linter flag this line, but it does not.
    rfl
  rfl

It looks to me like the problem is that the suffices expands in to a focus node, which then get causes everything below that to get ignored:

mathlib4/Mathlib/Tactic/Linter/Multigoal.lean

Line 124 in 7669cc5

``Lean.Parser.Tactic.focus,

[dwrensha]

cc @adomani

[dwrensha]

Here is a line in mathlib that should get flagged by the multiGoal linter, but currently does not, due to this bug:

mathlib4/Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean

Line 344 in 7669cc5

simp only [ne_eq, differentiableAt_const]