fix: update LazyDiscrTree to not reuse names when caching

[joehendrix]

This fixes an issue discovered in Mathlib with the meta cache being poisoned by using a name generator. It is difficult to reproduce due to the name collisions being rare, but here is a minimal module with definitions that result in an error:

prelude
universe u

inductive Unit2 : Type where
  | unit : Unit2

inductive Eq2 {α : Sort u} : α → α → Prop where
  | refl (a : α) : Eq2 a a

structure Subtype2 {α : Sort u} (p : α → Prop) where
  val : α

def End (α) := α → α
theorem end_app_eq (α : Type u) (f : End α) (a : α) : Eq2 (f a) (f a) := Eq2.refl _
theorem Set.coe_eq_subtype {α : Type u} (s : α → Prop) : Eq2 (Subtype2 s) (Subtype2 s) := Eq2.refl _
def succAboveCases {_ : Unit2} {α : Unit2 → Sort u} (i : Unit2) (v : α i) : α i := v
theorem succAbove_cases_eq_insertNth : Eq2 @succAboveCases.{u + 1} @succAboveCases.{u + 1} := Eq2.refl _

Removing any of thee last 5 definitions avoids the error. Testing against Mathlib shows this PR fixes the issue.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f986f69a32c6167d772a50b0e7f3078dc104ee24 --onto ae492265fec103aa834d897bf9f68c94d10f0785. (2024-03-05 21:34:31)