fix: setting pp.mdata to true breaks @[pp_with_univ]

[plp127]

This PR fixes an issue where turning on pp.mdata causes constants tagged with @[pp_with_univ] to print as

[mdata pp.universes:true]
  [mdata pp.universes:true]
    [mdata pp.universes:true]
      [mdata pp.universes:true]
        [mdata pp.universes:true]
          [mdata pp.universes:true] [mdata pp.universes:true] [mdata pp.universes:true] [mdata pp.universes:true] ⋯

When pp.mdata is set to true, expressions with mdata are printed by first printing the mdata and the printing the bare expression underneath. This breaks @[pp_with_univ] which works by applying mdata setting pp.universes to true onto the constant name, and then redelaborating the new expression containing mdata. This causes an infinite loop the the delaborator since @[pp_with_univ] applies the mdata, and then since pp.mdata is true the mdata is removed before delaborating the constant, which then has mdata applied again, and so on. We fix the issue by instead having the implementation of @[pp_with_univ] directly set the pp.universes option, instead of delegating it to delabMData with a metadata.

---

[github-actions]

PR summary b1095e016d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ Bar
+ Foo

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit b1095e0).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit b1095e016d
Reference commit 158047ba1d

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[JovanGerb]

You can also use TreeMap.alter, right?

[plp127]

I just copied what was done in Lean.PrettyPrinter.Delaborator.withMDataOptions.