chore: fix and re-enable differential geometry elaborators test (leanprover-community#34562)

`set_option pp.mvars false` normalises the universe levels, making the output sufficiently deterministic.
Follow-up to leanprover-community#30744.

Author: grunweg

MathlibTest/DifferentialGeometry/NotationAdvanced.lean

@@ -367,22 +367,21 @@ Hint: failures to find a model with corners can be debugged with the command `se
 -- TODO: the error message could be more helpful.
 variable {E'''' : Type*} [NormedAddCommGroup E''''] [NormedSpace ℝ E''''] (σ : ℝ →+* ℝ) [RingHomIsometric σ]
 
--- FIXME: the error message is non-deterministic because of different universe levels,
--- normalise this somehow and re-enable this test!
 variable {f : M → E'' →SL[σ] E''''} in
-/-
+/--
 error: Application type mismatch: The argument
   𝓘(ℝ, E'' →SL[σ] E'''')
 has type
   ModelWithCorners.{0, max u_11 u_13, max u_11 u_13} ℝ (E'' →SL[σ] E'''') (E'' →SL[σ] E'''')
 but is expected to have type
-  ModelWithCorners.{u_1, ?u.235761, ?u.235762} 𝕜 ?E' ?H'
+  ModelWithCorners.{u_1, _, _} 𝕜 ?E' ?H'
 in the application
   @ContMDiff 𝕜 inst✝³⁰ E inst✝²⁹ inst✝²⁸ H inst✝²⁷ I ?M ?inst✝ ?inst✝¹ ?E' ?inst✝² ?inst✝³ ?H' ?inst✝⁴
     𝓘(ℝ, E'' →SL[σ] E'''')
 -/
---#guard_msgs in
---#check CMDiff 2 f
+#guard_msgs in
+set_option pp.mvars.anonymous false in
+#check CMDiff 2 f
 
 end