diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean
index 3b8eb7268d..c13120c883 100644
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -11,9 +11,6 @@ import Init.ByCases
 import Init.Conv
 import Init.Omega
 
--- Remove after the next stage0 update
-set_option allowUnsafeReducibility true
-
 namespace Fin
 
 /-- If you actually have an element of `Fin n`, then the `n` is always positive -/
diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index 197888bf00..65fb8dc4ec 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -14,9 +14,6 @@ import Init.RCases
 # Lemmas about integer division needed to bootstrap `omega`.
 -/
 
--- Remove after the next stage0 update
-set_option allowUnsafeReducibility true
-
 open Nat (succ)
 
 namespace Int