one more tiny correction

leanprover · Jan 13, 2025 · 1f95486 · 1f95486
1 parent 2a94e4a
commit 1f95486
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -563,7 +563,7 @@ theorem wfImp_alterₘ [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β}
       simp only [buckets_withComputedSize]
       simp only [containsKey_of_perm <| toListModel_updateBucket_alter h]
       rw [← getValueCast?_eq_some_getValueCast h₁]
-      conv => lhs; congr; rw [containsKey_alterKey_self h.distinct];
+      conv => lhs; congr; rw [containsKey_alterKey_self h.distinct]
     · next h₁ =>
       rw [containsₘ_eq_containsKey h] at h₁
       rw [alterKey]