diff --git a/lean-toolchain b/lean-toolchain
index cf25a98..f8a3648 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.15.0-rc1
+leanprover/lean4:nightly-2024-12-17
diff --git a/src/verso/Verso/Code/Highlighted.lean b/src/verso/Verso/Code/Highlighted.lean
index 77f4636..d38b7dc 100644
--- a/src/verso/Verso/Code/Highlighted.lean
+++ b/src/verso/Verso/Code/Highlighted.lean
@@ -367,13 +367,13 @@ where
 def _root_.Array.mapIndexed (arr : Array α) (f : Fin arr.size → α → β) : Array β := Id.run do
   let mut out := #[]
   for h : i in [:arr.size] do
-    out := out.push (f ⟨i, h.right⟩ arr[i])
+    out := out.push (f ⟨i, by get_elem_tactic⟩ arr[i])
   out
 
 def _root_.Array.mapIndexedM [Monad m] (arr : Array α) (f : Fin arr.size → α → m β) : m (Array β) := do
   let mut out := #[]
   for h : i in [:arr.size] do
-    out := out.push (← f ⟨i, h.right⟩ arr[i])
+    out := out.push (← f ⟨i, by get_elem_tactic⟩ arr[i])
   pure out
 
 
diff --git a/src/verso/Verso/Doc.lean b/src/verso/Verso/Doc.lean
index a263459..e877436 100644
--- a/src/verso/Verso/Doc.lean
+++ b/src/verso/Verso/Doc.lean
@@ -37,14 +37,11 @@ inductive MathMode where | inline | display
 deriving Repr, BEq, Hashable, Ord, ToJson, FromJson
 
 private def arrayEq (eq : α → α → Bool) (xs ys : Array α) : Bool := Id.run do
-    if h : xs.size = ys.size then
-      for h' : i in [0:xs.size] do
-        have : i < ys.size := by
-          let ⟨_, h''⟩ := h'
-          simp [*] at h''; assumption
-        if !(eq xs[i] ys[i]) then return false
-      return true
-    else return false
+  if xs.size = ys.size then
+    for x in xs, y in ys do
+      if !(eq x y) then return false
+    return true
+  else return false
 
 inductive Inline (genre : Genre) : Type where
   | text (string : String)
diff --git a/src/verso/Verso/Hover.lean b/src/verso/Verso/Hover.lean
index d78463f..f2dabbf 100644
--- a/src/verso/Verso/Hover.lean
+++ b/src/verso/Verso/Hover.lean
@@ -35,5 +35,7 @@ deriving TypeName
 def addCustomHover [Monad m] [MonadInfoTree m] [MonadLiftT IO m] (stx : Syntax) (hover : UserHover) : m Unit := do
   let txt ← match hover with
     | .markdown str => pure str
-    | .messageData m => m.toString
+     -- TODO Change signature to MonadLiftT BaseIO m. This formulation is for a bit wider
+     -- compatibility in December 2024, but after another release it can go away.
+    | .messageData m => (m.toString : IO String)
   pushInfoLeaf <| .ofCustomInfo ⟨stx, .mk <| CustomHover.mk txt⟩