Unused obtain is not picked up by the unused have linter

Stream: mathlib4

[Yaël Dillies]

The unusedHaveSuffices linter does not pick up unused obtain calls:

import Mathlib.Tactic.Linter.Lint

theorem I_dont_have_unused_haves : True := by
  obtain I_am_used : True := trivial
  trivial

theorem I_have_unused_haves : True := by
  have I_am_unused : True := trivial
  trivial

#lint
-- Found 1 error in 2 declarations (plus 0 automatically generated ones) in the current file with 15 linters

/- The `unusedHavesSuffices` linter reports:
THE FOLLOWING DECLARATIONS HAVE INEFFECTUAL TERM MODE HAVE/SUFFICES BLOCKS. In the case of `have` this is a term of the form `have h := foo, bar` where `bar` does not refer to `foo`. Such statements have no effect on the generated proof, and can just be replaced by `bar`, in addition to being ineffectual, they may make unnecessary assumptions in proofs appear as if they are used. For `suffices` this is a term of the form `suffices h : foo, proof_of_goal, proof_of_foo` where `proof_of_goal` does not refer to `foo`. Such statements have no effect on the generated proof, and can just be replaced by `proof_of_goal`, in addition to being ineffectual, they may make unnecessary assumptions in proofs appear as if they are used. -/
#check I_have_unused_haves /- unnecessary have I_am_unused : True -/

[Aaron Liu]

It looks like the obtain doesn't actually make it into the final proof term

[Aaron Liu]

It's as if you used a haveI