Prerequisites

• [X ] 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 for variables used only in inductions.

Context

This was discussed in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Possible.20linter.2EunusedVariables.20bug

Steps to Reproduce

example (P : Unit → Prop) (H : P () → True) (x : Unit) (h : P x) : True := by
  let h' := h
  cases x
  exact H h'

Expected behavior: No warning occurs.

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

Versions

Lean (version 4.3.0-rc1, commit baa4b68, Release)
Manjaro Linux 23.0