`linter.unusedVariables` false positive when used in `decreasing_by`

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

In some cases, the linter.unusedVariables yields false positives.

Context

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/False.20Positive.20Warning.3A.20.60linter.2EunusedVariables.60

Steps to Reproduce

variable (α : Type)

def sample (n : Nat) : Nat :=
  match h : n with
  | 0 => 0
  | m + 1 => m + sample (m / 2)
  decreasing_by
    simp [h]
    simp_wf
    exact Nat.lt_of_le_of_lt (Nat.div_le_self _ _) (Nat.lt_succ_self _)

Expected behavior: No warning occurs.

Actual behavior: The message "unused variable h [linter.unusedVariables]" is shown.

Versions

Lean "4.3.0-rc2"
OS: lean playground's OS version

Start by running the minimal sample reproducer with Lean and confirm that linter.unusedVariables reports h despite its use in decreasing_by. Trace the linter.unusedVariables implementation and its handling of termination proofs; done means the reproducer emits no unused-variable warning without regressing related linter behavior.