From aba6f4af8ff03384be41a246c83493f28008f77d Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpvdoorn@gmail.com>
Date: Fri, 21 Apr 2023 19:24:26 +0000
Subject: [PATCH] perf: dsimp only to mitigate to_additive slowness (#3580)

* `to_additive` is slow on this file. I'll try to improve performance in `to_additive`, but this behavior is exposed by working with gigantic proof terms.
* The `dsimp only` in `Submonoid.LocalizationMap.lift` changes `to_additive` time from ~27s to ~7s (still needs improving, but this puts a band-aid on it).
---
 Mathlib/GroupTheory/MonoidLocalization.lean | 24 ++++++++++-----------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/Mathlib/GroupTheory/MonoidLocalization.lean b/Mathlib/GroupTheory/MonoidLocalization.lean
index 7ad23aa77e2ae..59fc10237d289 100644
--- a/Mathlib/GroupTheory/MonoidLocalization.lean
+++ b/Mathlib/GroupTheory/MonoidLocalization.lean
@@ -909,8 +909,8 @@ induced from `N` to `P` sending `z : N` to `g x - g y`, where `(x, y) : M × S`
 noncomputable def lift : N →* P where
   toFun z := g (f.sec z).1 * (IsUnit.liftRight (g.restrict S) hg (f.sec z).2)⁻¹
   map_one' := by rw [mul_inv_left, mul_one] ; exact f.eq_of_eq hg (by rw [← sec_spec, one_mul])
-  map_mul' x y :=
-    by
+  map_mul' x y := by
+    dsimp only
     rw [mul_inv_left hg, ← mul_assoc, ← mul_assoc, mul_inv_right hg, mul_comm _ (g (f.sec y).1), ←
       mul_assoc, ← mul_assoc, mul_inv_right hg]
     repeat' rw [← g.map_mul]
@@ -1203,12 +1203,12 @@ theorem map_comp_map {A : Type _} [CommMonoid A] {U : Submonoid A} {R} [CommMono
   by
   ext z
   show j.toMap _ * _ = j.toMap (l _) * _
-  · rw [mul_inv_left, ← mul_assoc, mul_inv_right]
-    show j.toMap _ * j.toMap (l (g _)) = j.toMap (l _) * _
-    rw [← j.toMap.map_mul, ← j.toMap.map_mul, ← l.map_mul, ← l.map_mul]
-    exact
-      k.comp_eq_of_eq hl j
-        (by rw [k.toMap.map_mul, k.toMap.map_mul, sec_spec', mul_assoc, map_mul_right])
+  rw [mul_inv_left, ← mul_assoc, mul_inv_right]
+  show j.toMap _ * j.toMap (l (g _)) = j.toMap (l _) * _
+  rw [← j.toMap.map_mul, ← j.toMap.map_mul, ← l.map_mul, ← l.map_mul]
+  exact
+    k.comp_eq_of_eq hl j
+      (by rw [k.toMap.map_mul, k.toMap.map_mul, sec_spec', mul_assoc, map_mul_right])
 #align submonoid.localization_map.map_comp_map Submonoid.LocalizationMap.map_comp_map
 #align add_submonoid.localization_map.map_comp_map AddSubmonoid.LocalizationMap.map_comp_map
 
@@ -1608,11 +1608,11 @@ def monoidOf : Submonoid.LocalizationMap S (Localization S) :=
         S with
     toFun := fun x ↦ mk x 1
     map_one' := mk_one
-    map_mul' := fun x y ↦ by rw [mk_mul, mul_one]
+    map_mul' := fun x y ↦ by dsimp only; rw [mk_mul, mul_one]
     map_units' := fun y ↦
-      isUnit_iff_exists_inv.2 ⟨mk 1 y, by rw [mk_mul, mul_one, one_mul, mk_self]⟩
-    surj' := fun z ↦
-      induction_on z fun x ↦ ⟨x, by rw [mk_mul, mul_comm x.fst, ← mk_mul, mk_self, one_mul]⟩
+      isUnit_iff_exists_inv.2 ⟨mk 1 y, by dsimp only; rw [mk_mul, mul_one, one_mul, mk_self]⟩
+    surj' := fun z ↦ induction_on z fun x ↦
+      ⟨x, by dsimp only; rw [mk_mul, mul_comm x.fst, ← mk_mul, mk_self, one_mul]⟩
     eq_iff_exists' := fun x y ↦
       mk_eq_mk_iff.trans <|
         r_iff_exists.trans <|