From f7fcff56b847239b0a7a5bf9b67c84dd0d771c60 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 24 Oct 2020 16:48:43 -0700
Subject: [PATCH] chore: remove workaround

---
 src/Init/Data/Nat/Div.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean
index ec42344bca..d4ce2aed43 100644
--- a/src/Init/Data/Nat/Div.lean
+++ b/src/Init/Data/Nat/Div.lean
@@ -98,7 +98,7 @@ theorem modLt (x : Nat) {y : Nat} : y > 0 → x % y < y := by
      | Or.inr h₁ =>
        have hgt : y > x from gtOfNotLe h₁
        have heq : x % y = x from modEqOfLt hgt
-       rw [← heq] at hgt; -- TODO: remove `;`
+       rw [← heq] at hgt
        exact hgt
 
 theorem modLe (x y : Nat) : x % y ≤ x := by