Commit 2025-03-24 18:17 ae692475

refactor(GroupTheory/MonoidLocalization): tweak simp-normal form (#23263) We have a couple of derived definitions such as mulEquivOfMulEquiv and mulEquivOfQuotients with apply lemmas turning them into more general definitions. The issue is those derived definitions also have more specific apply_mk' lemmas. Those had @[simp] attributes, but weren't in simp-normal form due to the apply lemmas firing before the apply_mk'. They can't be simply de-@[simp]ed either since they then get stuck after the apply lemma. The solution proposed in this PR is to add @[simp] lemmas so the more general definitions can simplify. This means creating one new lemma, lift_localizationMap_mk', and adding @[simp] attributes to a few others.