diff --git a/Batteries/CodeAction/Deprecated.lean b/Batteries/CodeAction/Deprecated.lean
index f308992885..ec6a2f11c2 100644
--- a/Batteries/CodeAction/Deprecated.lean
+++ b/Batteries/CodeAction/Deprecated.lean
@@ -32,7 +32,7 @@ def deprecatedCodeActionProvider : CodeActionProvider := fun params snap => do
   for m in snap.msgLog.toList do
     if m.data.isDeprecationWarning then
       if h : _ then
-        msgs := msgs.push (snap.cmdState.messages.toList[i])
+        msgs := msgs.push (snap.cmdState.messages.toList[i]'h)
     i := i + 1
   if msgs.isEmpty then return #[]
   let start := doc.meta.text.lspPosToUtf8Pos params.range.start
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index 1cf017c534..b932b5ff71 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -379,7 +379,7 @@ theorem modifyNth_eq_take_drop (f : α → α) :
     ∀ n l, modifyNth f n l = take n l ++ modifyHead f (drop n l) :=
   modifyNthTail_eq_take_drop _ rfl
 
-theorem modifyNth_eq_take_cons_drop (f : α → α) {n l} (h) :
+theorem modifyNth_eq_take_cons_drop (f : α → α) {n l} (h : n < length l) :
     modifyNth f n l = take n l ++ f l[n] :: drop (n + 1) l := by
   rw [modifyNth_eq_take_drop, drop_eq_getElem_cons h]; rfl