chore: address unusedHavesSuffices warning

Author: llllvvuu

Mathlib/Data/Nat/Log.lean

@@ -30,11 +30,10 @@ 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
+  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 +237,11 @@ 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
+  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