chore: address unusedHavesSuffices warning (#13754)

This linter was silently not doing anything until leanprover/lean4#4410 was fixed, and now it is working so a backlog of warnings needed to be addressed. Some were addressed here: #13680.

The warnings in this PRs are false positives (leanprover-community/batteries#428?), but a workaround is put in place.



Co-authored-by: L Lllvvuu <[email protected]>

Author: llllvvuu

Mathlib/Data/Nat/Log.lean

@@ -30,11 +30,12 @@ namespace Nat
 such that `b^k ≤ n`, so if `b^k = n`, it returns exactly `k`. -/
 --@[pp_nodot] porting note: unknown attribute
 def log (b : ℕ) : ℕ → ℕ
-  | n =>
-    if h : b ≤ n ∧ 1 < b then
-      have : n / b < n := div_lt_self ((Nat.zero_lt_one.trans h.2).trans_le h.1) h.2
-      log b (n / b) + 1
-    else 0
+  | n => if h : b ≤ n ∧ 1 < b then log b (n / b) + 1 else 0
+decreasing_by
+  -- putting this in the def triggers the `unusedHavesSuffices` linter:
+  -- https://github.com/leanprover-community/batteries/issues/428
+  have : n / b < n := div_lt_self ((Nat.zero_lt_one.trans h.2).trans_le h.1) h.2
+  decreasing_trivial
 #align nat.log Nat.log
 
 @[simp]
@@ -238,11 +239,13 @@ theorem add_pred_div_lt {b n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : (n + b - 1) /
 `k : ℕ` such that `n ≤ b^k`, so if `b^k = n`, it returns exactly `k`. -/
 --@[pp_nodot]
 def clog (b : ℕ) : ℕ → ℕ
-  | n =>
-    if h : 1 < b ∧ 1 < n then
-      have : (n + b - 1) / b < n := add_pred_div_lt h.1 h.2
-      clog b ((n + b - 1) / b) + 1
-    else 0
+  | n => if h : 1 < b ∧ 1 < n then clog b ((n + b - 1) / b) + 1 else 0
+decreasing_by
+  -- putting this in the def triggers the `unusedHavesSuffices` linter:
+  -- https://github.com/leanprover-community/batteries/issues/428
+  have : (n + b - 1) / b < n := add_pred_div_lt h.1 h.2
+  decreasing_trivial
+
 #align nat.clog Nat.clog
 
 theorem clog_of_left_le_one {b : ℕ} (hb : b ≤ 1) (n : ℕ) : clog b n = 0 := by