chore: add missing simp to Array.size_feraseIdx (#5577)

leanprover · Oct 2, 2024 · 6cd80c2 · 6cd80c2
1 parent f202469
commit 6cd80c2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
@@ -720,7 +720,7 @@ termination_by a.size - i.val
 decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
 
 -- This is required in `Lean.Data.PersistentHashMap`.
-theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
+@[simp] theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
   induction a, i using Array.feraseIdx.induct with
   | @case1 a i h a' _ ih =>
     unfold feraseIdx