fix proof

leanprover · Sep 23, 2024 · 1769ea4 · 1769ea4
1 parent 8a4193e
commit 1769ea4
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/Init/Data/Array/TakeDrop.lean b/src/Init/Data/Array/TakeDrop.lean
@@ -12,6 +12,7 @@ namespace Array
 theorem exists_of_uset (self : Array α) (i d h) :
     ∃ l₁ l₂, self.toList = l₁ ++ self[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
       (self.uset i d h).toList = l₁ ++ d :: l₂ := by
-  simpa [Array.getElem_eq_toList_getElem] using List.exists_of_set _
+  simpa only [ugetElem_eq_getElem, getElem_eq_toList_getElem, uset, toList_set] using
+    List.exists_of_set _
 
 end Array