diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean
index bf4ff6d8d5..421dd67983 100644
--- a/src/Init/Data/Nat/Div.lean
+++ b/src/Init/Data/Nat/Div.lean
@@ -119,7 +119,7 @@ theorem mod_one (x : Nat) : x % 1 = 0 := by
   have : (y : Nat) → y < 1 → y = 0 := by
     intro y
     cases y with
-    | zero   => intro h; rfl
+    | zero   => intro h; exact rfl -- TODO remove exact
     | succ y => intro h; apply absurd (Nat.lt_of_succ_lt_succ h) (Nat.not_lt_zero y)
   exact this _ h
 
diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean
index 707337ed2d..37506468df 100644
--- a/src/Init/Data/String/Extra.lean
+++ b/src/Init/Data/String/Extra.lean
@@ -38,7 +38,7 @@ theorem one_le_csize (c : Char) : 1 ≤ csize c := by
 
 theorem eq_empty_of_bsize_eq_zero (h : s.endPos = {}) : s = "" := by
   match s with
-  | ⟨[]⟩   => rfl
+  | ⟨[]⟩   => exact rfl -- TODO: remove exact
   | ⟨c::cs⟩ =>
     injection h with h
     simp [endPos, utf8ByteSize, utf8ByteSize.go] at h
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 4d5bf0706d..60284d635d 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -351,8 +351,6 @@ macro:1 x:tactic " <;> " y:tactic:0 : tactic => `(tactic| focus ($x:tactic; all_
 /-- `rfl` is equivalent to `exact rfl`, but has a few optimizatons. -/
 syntax (name := refl) "rfl" : tactic
 
-macro_rules | `(tactic| rfl) => `(tactic| exact rfl)
-
 /--
   Similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions,
   theorems included (relevant for declarations defined by well-founded recursion). -/