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.

[SproutSeeds]

Hi all, I am planning a local first pass on this issue this week. I will run style preflight and local gate before opening any draft PR. If someone is already working on this, happy to coordinate and I can switch targets.

[SproutSeeds]

I can still reproduce the unusedTactic false positive on current master.

• The smaller repro I landed on is let _ := (by trivial : ((by exact True) : Prop)); trivial.
• The issue seems to be in UnusedTactic.getTactics: it recurses into the annotation side of Parser.Term.typeAscription, so it records tactics that live only inside the type annotation.
• I pushed a narrow branch-backed fix here: https://github.com/SproutSeeds/mathlib4/tree/cody/issue-31840-unused-tactic-ascription (commit 2b07584dbcc). It walks the value side of (e : T) but skips T, and adds a regression test in MathlibTest/UnusedTactic.lean.
• Focused local verification passed with env COPYFILE_DISABLE=1 ~/.elan/bin/lake build Mathlib.Tactic.Linter.UnusedTactic MathlibTest.UnusedTactic.

One caveat

On the exact original issue snippet I still also see the separate unreachableTactic warning. That looks like the analogous Batteries linter path rather than this mathlib-side unusedTactic walker, so I kept this branch focused on the issue as filed.