From 9fed5bda7d2048a5bd293bb660b5deb03ad1f33a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 19 Mar 2022 09:44:57 -0700
Subject: [PATCH] chore: remove workarounds

---
 src/Init/Data/Nat/Div.lean  | 9 +++------
 src/Init/Data/Nat/Log2.lean | 1 -
 2 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean
index 352139deea..3dc3165300 100644
--- a/src/Init/Data/Nat/Div.lean
+++ b/src/Init/Data/Nat/Div.lean
@@ -18,8 +18,7 @@ protected def div (x y : @& Nat) : Nat :=
     Nat.div (x - y) y + 1
   else
     0
-decreasing_by
-  decreasing_with apply div_rec_lemma; assumption
+decreasing_by apply div_rec_lemma; assumption
 
 instance : Div Nat := ⟨Nat.div⟩
 
@@ -37,8 +36,7 @@ theorem div.inductionOn.{u}
     ind x y h (inductionOn (x - y) y ind base)
   else
     base x y h
-decreasing_by
-  decreasing_with apply div_rec_lemma; assumption
+decreasing_by apply div_rec_lemma; assumption
 
 @[extern "lean_nat_mod"]
 protected def mod (x y : @& Nat) : Nat :=
@@ -46,8 +44,7 @@ protected def mod (x y : @& Nat) : Nat :=
     Nat.mod (x - y) y
   else
     x
-decreasing_by
-  decreasing_with apply div_rec_lemma; assumption
+decreasing_by apply div_rec_lemma; assumption
 
 instance : Mod Nat := ⟨Nat.mod⟩
 
diff --git a/src/Init/Data/Nat/Log2.lean b/src/Init/Data/Nat/Log2.lean
index 82269f5c84..315a60694b 100644
--- a/src/Init/Data/Nat/Log2.lean
+++ b/src/Init/Data/Nat/Log2.lean
@@ -25,5 +25,4 @@ Computes `⌊max 0 (log₂ n)⌋`.
 @[extern "lean_nat_log2"]
 def log2 (n : @& Nat) : Nat :=
   if h : n ≥ 2 then log2 (n / 2) + 1 else 0
-termination_by _ n => n
 decreasing_by exact log2_terminates _ h