Variable highlighting with `peel`

[madvorak]

When variable highlighting is active in one's IDE, the variable created by peel isn't highlighted.

import Mathlib.Tactic.Peel

example (P : ℕ → Prop) (hP : ∃ n : ℕ, P n) :
    ∃ n : ℕ, P n := by
  peel hP with hn
  exact hn

Here hn should be highlighted already on the peel line.