RFC: un-`simp`ing `normalize_apply`

Stream: mathlib4

[Anne Baanen]

So I was looking at some porting notes in Algebra.GCDMonoid.Basic and noticed that docs#normalize_apply seems to get in the way of simplification quite often. It states normalize x = x * normUnit x. I don't like how it turns a thing I'm familiar with, docs#normalize, into a longer expression involving a rather mysterious docs#NormalizationMonoid.normUnit. Moreover, we have quite a few lemmas that are explicitly given higher priority than normalize_apply.

Do we really want this as a simp lemma?

I opened #18006 as a proof of concept PR to remove the simp attribute and it's about evenly matched between removals of simp [- normalize_apply] and additions of simp [normalize_apply].

[Anne Baanen]

Similarly for docs#Localization.mk_eq_monoidOf_mk'_apply which we also have to carefully avoid when simplifying (although I am more sympathetic to keeping this around, and simply updating the simp set so it is more confluent).

[Ruben Van de Velde]

I never liked it much, so +1 from me

[Ruben Van de Velde]

(Probably Ya-el will point out it has x twice on the RHS)

[Anne Baanen]

Anne Baanen said:

Similarly for docs#Localization.mk_eq_monoidOf_mk'_apply which we also have to carefully avoid when simplifying (although I am more sympathetic to keeping this around, and simply updating the simp set so it is more confluent).

See PR #18015.

[Anne Baanen]

There seems to be no objection over the past days, should we go ahead with the change?