chore: use local instance in Lsp.Diagnostics (#5031)

I'm experimenting with changing the signature of `Ord.arrayOrd`; rather
than make a local synonym here, let's make a local instance so it
doesn't interact with the experiments.

src/Lean/Data/Lsp/Diagnostics.lean

@@ -113,8 +113,7 @@ structure DiagnosticWith (α : Type) where
 def DiagnosticWith.fullRange (d : DiagnosticWith α) : Range :=
   d.fullRange?.getD d.range
 
-local instance [Ord α] : Ord (Array α) := Ord.arrayOrd
-
+attribute [local instance] Ord.arrayOrd in
 /-- Restriction of `DiagnosticWith` to properties that are displayed to users in the InfoView. -/
 private structure DiagnosticWith.UserVisible (α : Type) where
   range               : Range