diff --git a/src/Lean/Data/RArray.lean b/src/Lean/Data/RArray.lean
index c58f07fe1078..54b7fd5612b2 100644
--- a/src/Lean/Data/RArray.lean
+++ b/src/Lean/Data/RArray.lean
@@ -35,7 +35,7 @@ theorem RArray.get_ofFn {n : Nat} (f : Fin n → α) (h : 0 < n) (i : Fin n) :
   go 0 n h (Nat.le_refl _) (Nat.zero_le _) i.2
 where
   go lb ub h1 h2 (h3 : lb ≤ i.val) (h3 : i.val < ub) : (ofFn.go f lb ub h1 h2).get i = f i := by
-    induction lb, ub, h1, h2 using RArray.ofFn.go.induct (f := f) (n := n)
+    induction lb, ub, h1, h2 using RArray.ofFn.go.induct (n := n)
     case case1 =>
       simp [ofFn.go, RArray.get_eq_getImpl, RArray.getImpl]
       congr
@@ -53,7 +53,7 @@ theorem RArray.size_ofFn {n : Nat} (f : Fin n → α) (h : 0 < n) :
   go 0 n h (Nat.le_refl _)
 where
   go lb ub h1 h2 : (ofFn.go f lb ub h1 h2).size = ub - lb := by
-    induction lb, ub, h1, h2 using RArray.ofFn.go.induct (f := f) (n := n)
+    induction lb, ub, h1, h2 using RArray.ofFn.go.induct (n := n)
     case case1 => simp [ofFn.go, size]; omega
     case case2 ih1 ih2 hiu => rw [ofFn.go]; simp [size, *]; omega