Commit 2024-10-21 15:16 4ed749a9
View on Github →RFC chore(GroupTheory/MonoidLocalization): un-@[simp] Localization.mk_eq_monoidOf_mk' (#18015)
This lemma feels somewhat close to exposing an implementation detail to me, although it can be argued that the right hand side is indeed a bit simpler since it definitely uses more simple machinery. Again the balance is somewhat even between removing now-unnecessary simp [-Localization.mk_eq_monoidOf_mk'] and adding new simp [Localization.mk_eq_monoidOf_mk'].
Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/RFC.3A.20un-.60simp.60ing.20.60normalize_apply.60