simp tag on StieltjesFunction.measure_singleton

Stream: mathlib4

[Anatole Dedecker]

In #11746 (not ready for review yet), the simpNF linter fails on docs#StieltjesFunction.measure_singleton with message

simplify fails on left-hand side:
failed to synthesize
  MeasureTheory.NoAtoms (StieltjesFunction.measure f)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

This goes away if I remove the instance

@[to_additive]
instance continuousSMul_of_properSMul [ProperSMul G X] : ContinuousSMul G X where
  continuous_smul := (isProperMap_smul_pair G X).continuous.fst

but that seems a bit extreme.

If anyone wants to investigate what's going on, that would be great! Otherwise, Riccardo just suggested removing the simp tag on this lemma, does that sound fine?