linter.unusedVariables bug

Stream: std4

[Sven Manthe]

I got a wrong positive of linter.unusedVariables; a reduced working example is

import Mathlib
theorem sor {α: Prop} (a: ℕ): α := sorry
structure Game (A: Type*) where
  T: Set (List A)
def Game.residual (G: Game A) {x: List A} (_: x ∈ G.T): Game A where
  T := G.T
noncomputable def sew {G: Game A}
  (_: {a: A} → (h: [a] ∈ G.T) → List (G.residual h).T):
  ℕ := 0
theorem eqPre (G: Game A): ∀_: List A, False := by
  intro x
  let f {a: A} (h: [a] ∈ (G.residual (sor 0)).T):
  List ((Game.residual (Game.residual G (_ : x ∈ G.T)) h).T) := []
  let str := sew f --this line causes "unused variable 'str'", although str is used
  induction' x
  { exact sor str }
  exact sor 0

I already posted this in "new members" (cf. https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Possible.20linter.2EunusedVariables.20bug/near/401429971), and after some discussion it was suggested to repost it here.

[Scott Morrison]

Mario has minimised this at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Possible.20linter.2EunusedVariables.20bug/near/401865331