diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index b18756aedb..8bc19067ff 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@@ -80,7 +80,7 @@ instance : Div (Fin n) where
 instance : HMod (Fin n) Nat (Fin n) where
   hMod := Fin.modn
 
-instance : OfNat (Fin (n+1)) i where
+instance : OfNat (Fin (noindex! (n+1))) i where
   ofNat := Fin.ofNat i
 
 theorem vneOfNe {i j : Fin n} (h : i ≠ j) : val i ≠ val j :=