chore: squeeze a simp in HashMap/WF (#909)

leanprover-community · Aug 12, 2024 · d4dfc4e · d4dfc4e
1 parent 7b244ea
commit d4dfc4e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Batteries/Data/HashMap/WF.lean b/Batteries/Data/HashMap/WF.lean
@@ -225,7 +225,7 @@ private theorem pairwise_replaceF [BEq α] [PartialEquivBEq α]
   | cons a l ih =>
     simp only [List.pairwise_cons, List.replaceF] at H ⊢
     generalize e : cond .. = z; unfold cond at e; revert e
-    split <;> (intro h; subst h; simp)
+    split <;> (intro h; subst h; simp only [List.pairwise_cons])
     · next e => exact ⟨(H.1 · · ∘ PartialEquivBEq.trans e), H.2⟩
     · next e =>
       refine ⟨fun a h => ?_, ih H.2⟩