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

Mathlib/FieldTheory/RatFunc/Basic.lean

@@ -364,7 +364,7 @@ def map [MonoidHomClass F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ S[X]⁰.comap 
   map_one' := by
     beta_reduce -- Porting note(#12129): force the function to be applied
     rw [← ofFractionRing_one, ← Localization.mk_one, liftOn_ofFractionRing_mk, dif_pos]
-    · simpa using ofFractionRing_one
+    · simpa [Localization.mk_eq_monoidOf_mk'] using ofFractionRing_one
     · simpa using Submonoid.one_mem _
   map_mul' x y := by
     beta_reduce -- Porting note(#12129): force the function to be applied

Mathlib/GroupTheory/MonoidLocalization/Away.lean

@@ -152,9 +152,9 @@ class of `(y, 0)` in the Localization of `M` at the Submonoid generated by `x`."
 abbrev Away.monoidOf : Submonoid.LocalizationMap.AwayMap x (Away x) :=
   Localization.monoidOf (Submonoid.powers x)
 
--- @[simp] -- Porting note (#10618): simp can prove thisrove this
 @[to_additive]
-theorem Away.mk_eq_monoidOf_mk' : mk = (Away.monoidOf x).mk' := by simp
+theorem Away.mk_eq_monoidOf_mk' : mk = (Away.monoidOf x).mk' := by
+  simp [Localization.mk_eq_monoidOf_mk']
 
 /-- Given `x : M` and a Localization map `f : M →* N` away from `x`, we get an isomorphism between
 the Localization of `M` at the Submonoid generated by `x` as a quotient type and `N`. -/

Mathlib/GroupTheory/MonoidLocalization/Basic.lean

@@ -1230,7 +1230,7 @@ theorem mk_eq_monoidOf_mk'_apply (x y) : mk x y = (monoidOf S).mk' x y :=
       conv => rhs; rw [← mul_one 1]; rw [← mul_one x]
       exact mk_eq_mk_iff.2 (Con.symm _ <| (Localization.r S).mul (Con.refl _ (x, 1)) <| one_rel _)
 
-@[to_additive (attr := simp)]
+@[to_additive]
 theorem mk_eq_monoidOf_mk' : mk = (monoidOf S).mk' :=
   funext fun _ ↦ funext fun _ ↦ mk_eq_monoidOf_mk'_apply _ _
 
@@ -1298,7 +1298,7 @@ variable {α : Type*} [CancelCommMonoid α] {s : Submonoid α} {a₁ b₁ : α}
 
 @[to_additive]
 theorem mk_left_injective (b : s) : Injective fun a => mk a b := fun c d h => by
-  simpa [-mk_eq_monoidOf_mk', mk_eq_mk_iff, r_iff_exists] using h
+  simpa [mk_eq_mk_iff, r_iff_exists] using h
 
 @[to_additive]
 theorem mk_eq_mk_iff' : mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = a₂ * b₁ := by

Mathlib/GroupTheory/MonoidLocalization/Order.lean

@@ -106,7 +106,7 @@ sending `a` to `a - b`."]
 def mkOrderEmbedding (b : s) : α ↪o Localization s where
   toFun a := mk a b
   inj' := mk_left_injective _
-  map_rel_iff' {a b} := by simp [-mk_eq_monoidOf_mk', mk_le_mk]
+  map_rel_iff' {a b} := by simp [mk_le_mk]
 
 end OrderedCancelCommMonoid
 

Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean

@@ -528,7 +528,7 @@ theorem isUnit_iff_isUnit_val (f : HomogeneousLocalization.AtPrime 𝒜 𝔭) :
       (hc ▸ Ideal.mul_mem_left _ c.1 (Ideal.mul_mem_right b _ h))
   refine isUnit_of_mul_eq_one _ (Quotient.mk'' ⟨f.1, f.3, f.2, this⟩) ?_
   rw [← mk_mul, ext_iff_val, val_mk]
-  simp [mul_comm f.den.1]
+  simp [mul_comm f.den.1, Localization.mk_eq_monoidOf_mk']
 
 instance : Nontrivial (HomogeneousLocalization.AtPrime 𝒜 𝔭) :=
   ⟨⟨0, 1, fun r => by simp [ext_iff_val, val_zero, val_one, zero_ne_one] at r⟩⟩