Why are the operators on Real irreducible?

Stream: mathlib4

[Daniel Weber]

Looking at file#Mathlib/Data/Real/Basic, I can see that the operators on Real (zero, one, addition, multiplication, etc.) are irreducible_defs. What is the design thought behind that?

[Mario Carneiro]

you don't want to unfold them, and lean will sometimes unfold them anyway resulting in performance issues (when e.g. trying to prove that sin x = cos x by unfolding literally everything and ending up with some goal like Real.add = Real.sub which it wants to keep unfolding...)