diff --git a/src/Init/Data/AC.lean b/src/Init/Data/AC.lean
index faab678d29..6d332944d7 100644
--- a/src/Init/Data/AC.lean
+++ b/src/Init/Data/AC.lean
@@ -186,7 +186,7 @@ theorem Context.evalList_insert
     case inr =>
       split
       case inl => simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
-      case inr => simp_all [evalList, EvalInformation.evalOp]; simp [ih]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)] -- TODO: remove `simp [ih]` after `update stage0`
+      case inr => simp_all [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
 
 theorem Context.evalList_sort_congr
   (ctx : Context α)