deprecation

Author: kim-em

Mathlib/GroupTheory/MonoidLocalization/Basic.lean

@@ -1452,7 +1452,7 @@ theorem AddSubmonoid.isLocalizationMap_nat_int (S : AddSubmonoid ℕ) (hS : S 
     · exact ⟨z, 0, zero_mem _, by lia⟩
     have ⟨n, hnS, hn0⟩ := S.bot_or_exists_ne_zero.resolve_left hS
     have key : z < n * (z / n + 1) := Nat.lt_mul_div_succ _ <| Nat.pos_of_ne_zero hn0
-    exact ⟨(z / n + 1) * n - z, (z / n + 1) * n, nsmul_mem hnS _, by cutsat⟩
+    exact ⟨(z / n + 1) * n - z, (z / n + 1) * n, nsmul_mem hnS _, by lia⟩
 
 theorem AddSubmonoid.isLocalizationMap_top_nat_int :
     (⊤ : AddSubmonoid ℕ).IsLocalizationMap ((↑) : ℕ → ℤ) :=