diff --git a/src/Init/Data/Nat/SOM.lean b/src/Init/Data/Nat/SOM.lean
index 594bf9f808..f021500d88 100644
--- a/src/Init/Data/Nat/SOM.lean
+++ b/src/Init/Data/Nat/SOM.lean
@@ -122,7 +122,7 @@ where
 theorem Poly.append_denote (ctx : Context) (p₁ p₂ : Poly) : (p₁ ++ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
   match p₁ with
   | [] => simp!
-  | v :: p₁ => sorry -- TODO(0) simp! [append_denote _ p₁ p₂, Nat.add_assoc]
+  | v :: p₁ => simp! [append_denote _ p₁ p₂, Nat.add_assoc]
 
 theorem Poly.add_denote (ctx : Context) (p₁ p₂ : Poly) : (p₁.add p₂).denote ctx = p₁.denote ctx + p₂.denote ctx :=
   go hugeFuel p₁ p₂
diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean
index d2074bc295..707337ed2d 100644
--- a/src/Init/Data/String/Extra.lean
+++ b/src/Init/Data/String/Extra.lean
@@ -61,7 +61,7 @@ theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
 
 theorem Iterator.sizeOf_next_lt_of_atEnd (i : String.Iterator) (h : ¬ i.atEnd = true) : sizeOf i.next < sizeOf i :=
-  have h : i.hasNext = true := by sorry -- TODO(0) simp_arith [atEnd] at h; simp_arith [hasNext, h]
+  have h : i.hasNext = true := by simp_arith [atEnd] at h; simp_arith [hasNext, h]
   sizeOf_next_lt_of_hasNext i h
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)