size_alter' cosmetic improvement

leanprover · Jan 13, 2025 · ec5d4e8 · ec5d4e8
1 parent 0692e90
commit ec5d4e8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
@@ -1029,7 +1029,7 @@ theorem size_alter' [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)
     (m.alter k f).size =
     m.size
       - (if m.contains k then 1 else 0)
-      + (if (f (m.get? k)).isNone then 0 else 1) :=
+      + (if (f (m.get? k)).isSome then 1 else 0) :=
   sorry
 
 theorem size_alter_le [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} :