Unused tactic linter fires incorrectly in type ascriptions

[Timeroot]

The following code

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

triggers the unused tactic linter on the show A ≠ ∅ from by sorry part. Any tactic at all there triggers the same issue. I'm guessing this has something to do with the fact that the tactic is being used to construct a type ascription...? as opposed to the proof term of the theorem itself.

I also started a thread on zulip.