diff --git a/library/algebra/field.lean b/library/algebra/field.lean
index 12c9950610..de649d1517 100644
--- a/library/algebra/field.lean
+++ b/library/algebra/field.lean
@@ -454,10 +454,3 @@ section discrete_field
 end discrete_field
 
 end algebra
-
-
-/-
-    decidable.by_cases
-      (assume Ha : a = 0, sorry)
-      (assume Ha : a ≠ 0, sorry)
--/
diff --git a/library/data/real/order.lean b/library/data/real/order.lean
index 0dcc00cedf..0243619abf 100644
--- a/library/data/real/order.lean
+++ b/library/data/real/order.lean
@@ -6,8 +6,6 @@ The real numbers, constructed as equivalence classes of Cauchy sequences of rati
 This construction follows Bishop and Bridges (1985).
 
 To do:
- o Break positive naturals into their own file and fill in sorry's
- o Fill in sorrys for helper lemmas that will not be handled by simplifier
  o Rename things and possibly make theorems private
 -/