linter.unusedSectionVars: does not detect variable uses in where clauses

[kim-em]

The unused section variable linter does not detect when a variable is used inside a where clause.

MWE

variable (n : Nat)
include n

theorem foo : ∃ (_ : Nat), True := by
  exists k
  where
  k := n + 1

This produces a warning:

automatically included section variable(s) unused in theorem 'foo':
  n
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit n in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`

But n is used in the where clause (k := n + 1).

Discussion

https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/unused.20section.20variable.20linter.20is.20buggy/near/565224606

Note: the same Zulip thread also reports a related issue where the linter warns about an instance that cannot be omitted because it's referenced in the type of another included variable.