unused tactic linter issue

Stream: mathlib4

[Alex Meiburg]

I have a case where the unused tactic linter fires incorrectly:

import Mathlib

theorem test (A : Set ℕ) (x : ℕ) (hx : x ∈ A) : False := by
  have h2 : (Set.nonempty_iff_ne_empty.mpr (by simp : { y : ℕ |
    (Set.nonempty_iff_ne_empty.mpr (show A ≠ ∅ from by sorry)).some = y } ≠ ∅)).some = 7 := by
    sorry
  sorry

The show A ≠ ∅ from by sorry part is used to construct a type ascription, but not exactly the term itself(?), which is why I think it gets marked as unused. Of course that sorry is necessary - you can't leave it out! And any other tactic you put there to complete the proof also triggers the linter.

Figured I'd file it as an issue too: #31840

[Damiano Testa]

I just want to point out that the unreachableTactic linter equally misfires here.