reducible non-instances

Stream: mathlib4

[Yaël Dillies]

In !4#1725 it seems that making docs4#Function.Injective.addGroupWtihOne reducible makes a bunch of things break in Data.Real.Basic. Should we review the note reducible non-instances. Let me also remark that it could have to do with docs4#AbsoluteValue not having a hom class (as I'm hitting similar errors in !4#1238.

[Floris van Doorn]

What is causing these errors? Are reducible non-instances unfolded by simp and that is causing issues?
If simp unfolds reducible declarations but not instances, maybe we can mark the declarations to have the same reducibility as instances? (This requires a core change, since docs4#Lean.ReducibilityStatus doesn't have the option "instances" that docs4#Lean.Meta.TransparencyMode has.)