Flexible linter false positives/negatives

1. Doesn't trigger (false negative):

theorem foo {x₁ x₂ : Nat} {l₁ l₂ : List Nat} (h : x₁ :: l₁ = x₂ :: l₂) : l₁ = l₂ := by
  simp at h
  exact h.right

2. Doesn't trigger (false negative):

theorem foo {x₁ x₂ : Nat} {l₁ l₂ : List Nat} (h : x₁ :: l₁ = x₂ :: l₂) : l₁ = l₂ := by
  simp at h
  have := h.right
  sorry

3. Triggers (false positive):

theorem foo {x₁ x₂ : Nat} {l₁ l₂ : List Nat} (h : x₁ :: l₁ = x₂ :: l₂) : l₁ = l₂ := by
  simp at h
  let h := 3
  sorry

Zulip discussion

The issue provides three Lean snippets showing the flexible linter's false negatives and false positive, but names no source file or test. Reproduce these examples first, then read the linter implementation and linked Zulip discussion; done means the first two cases trigger appropriately while the locally shadowed h in the third does not.