deprecation
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index 3994d2f..44d9786 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -140,7 +140,7 @@ refine ih.trans ?_ simp only [Array.get_eq_getElem, AssocList.foldl_eq, Array.toList_set] rw [List.drop_eq_getElem_cons hi, List.bind_cons, List.foldl_append, - List.drop_set_of_lt _ _ (by omega), Array.getElem_eq_toList_getElem] + List.drop_set_of_lt _ _ (by omega), Array.getElem_eq_getElem_toList] · next i source target hi => rw [expand.go_neg hi, List.drop_eq_nil_of_le, bind_nil, foldl_nil] rwa [Array.size_eq_length_toList, Nat.not_lt] at hi
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean index 11751f0..a5e9f2c 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
@@ -297,7 +297,7 @@ dsimp; omega rw [List.getElem?_eq_getElem i_in_bounds, List.getElem?_eq_getElem i_in_bounds'] simp only [List.get_eq_getElem, Nat.zero_add] at h - rw [← Array.getElem_eq_toList_getElem] + rw [← Array.getElem_eq_getElem_toList] simp [h] · have arr_data_length_le_i : arr.toList.length ≤ i := by dsimp; omega
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean index daa2720..563df99 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
@@ -503,7 +503,7 @@ conv => rhs; rw [Array.size_mk] exact hbound simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte, - Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq + Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq rw [hidx, hl] at heq simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq simp only [← heq] at l_ne_b @@ -536,7 +536,7 @@ conv => rhs; rw [Array.size_mk] exact hbound simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte, - Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq + Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq rw [hidx, hl] at heq simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq have i_eq_l : i = l.1 := by rw [← heq] @@ -596,7 +596,7 @@ conv => rhs; rw [Array.size_mk] exact hbound simp only [getElem!, id_eq_idx, Array.toList_length, idx_in_bounds2, ↓reduceDIte, - Fin.eta, Array.get_eq_getElem, Array.getElem_eq_toList_getElem, decidableGetElem?] at heq + Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq rw [hidx] at heq simp only [Option.some.injEq] at heq rw [← heq] at hl