minor linter issue

Stream: lean4

[Kevin Buzzard]

namespace PSigma

theorem subtype_ext {β : Sort _} {p : α → β → Prop} :
    ∀ {x₀ x₁ : Σ'a, Subtype (p a)}, x₀.fst = x₁.fst → (x₀.snd : β) = x₁.snd → x₀ = x₁
  | ⟨_, _, _⟩, ⟨_, _, hb₁⟩, rfl, rfl => rfl

/-

(correct) linter error

unused variable `hb₁` [linter.unusedVariables]

but the squiggle is in the wrong place (not under `hb₁`)

-/