diff --git a/Mathlib/Combinatorics/Additive/VerySmallDoubling.lean b/Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
index 4230bc2b1da357..16af74cfe4075e 100644
--- a/Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
+++ b/Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
@@ -143,7 +143,7 @@ lemma mul_inv_eq_inv_mul_of_doubling_lt_two (h : #(A * A) < 2 * #A) : A * A⁻¹
 
 private lemma weaken_doubling (h : #(A * A) < (3 / 2 : ℚ) * #A) : #(A * A) < 2 * #A := by
   rw [← Nat.cast_lt (α := ℚ), Nat.cast_mul, Nat.cast_two]
-  linarith only [h]
+  linarith
 
 private lemma nonempty_of_doubling (h : #(A * A) < (3 / 2 : ℚ) * #A) : A.Nonempty := by
   by_contra! rfl
diff --git a/lakefile.lean b/lakefile.lean
index 6b3b4bba48ce66..513df8f528a609 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -34,6 +34,7 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[
   ⟨`linter.allScriptsDocumented, true⟩,
   ⟨`linter.pythonStyle, true⟩,
   ⟨`linter.style.longFile, .ofNat 1500⟩,
+  ⟨`linter.tacticAnalysis.regressions.linarithToGrind, true⟩,
   -- ⟨`linter.nightlyRegressionSet, true⟩,
   -- `latest_import.yml` uses this comment: if you edit it, make sure that the workflow still works
 ]