simps and semireducible

Stream: mathlib4

[Yury G. Kudryashov]

@Floris van Doorn Am I right that simps can see through semireducible definitions? I'm porting nnreals now, and I defined NNReal.toReal to use as coe.

[Yury G. Kudryashov]

Since defeq coes are no longer a thing, it makes sense to use this function in simps.

[Yury G. Kudryashov]

I can redefine NNReal as a structure but then I'll loose all the lemmas about Subtype (incl. those in Nonnneg).

[Eric Wieser]

Yury G. Kudryashov said:

I can redefine NNReal as a structure...

This sounds sufficiently awful that I wouldn't want to do it without trying a backport first

[Floris van Doorn]

simps was not designed for type synonyms that are (semi)reducibly defined to as a structure, so I expect it will only apply the Subtype configuration, and that it is not configurable.

[Floris van Doorn]

Did mathlib3 use simps in the nnreal file?

[Yury G. Kudryashov]

Yes, at least once. It's not a problem in mathlib3, because you get coe.

[Yury G. Kudryashov]

What about banning use of simps on type synonyms?