diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4f1dabb9841c26088f2e14e6558c0865c81f0b1f..42bc8763e14c8b840b957952d8563933ade27c39 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -141,6 +141,11 @@ API-breaking change is listed.
   + Remove `map_to_list_empty_inv_alt`; chain `Permutation_nil_r` and
     `map_to_list_empty_iff` instead.
   + Add lemma `map_filter_empty_iff`.
+- Add generalized lemma `map_filter_insert` that covers both the True and False
+  case. Rename old `map_filter_insert` → `map_filter_insert_True` and
+  `map_filter_insert_not_delete` → `map_filter_insert_False`.
++ Weaken premise of `map_filter_delete_not` to make it consistent with
+  `map_filter_insert_not'`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
@@ -195,6 +200,9 @@ s/\bsize_empty_inv\b/size_empty_iff/g
 s/\bdom_empty_inv(_L|)\b/dom_empty_iff\1/g
 s/\bgmultiset_elements_empty('|_inv)\b/gmultiset_elements_empty_iff/g
 s/\bgmultiset_size_empty_inv\b/gmultiset_size_empty_iff/g
+# map_filter_insert
+s/\bmap_filter_insert\b/map_filter_insert_True/g
+s/\bmap_filter_insert_not_delete\b/map_filter_insert_False/g
 EOF
 ```
 
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 2707671d9bdfe6af5f2d720005b8ba137ffa308a..3419b40225ce147ea38be8854cbcfef60d93c979 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1305,34 +1305,6 @@ Section map_filter_insert_and_delete.
   Context {A} (P : K * A → Prop) `{!∀ x, Decision (P x)}.
   Implicit Types m : M A.
 
-  Lemma map_filter_insert m i x :
-    P (i, x) → filter P (<[i:=x]> m) = <[i:=x]> (filter P m).
-  Proof.
-    intros HP. apply map_eq. intros j. apply option_eq; intros y.
-    rewrite map_filter_lookup_Some. destruct (decide (i = j)) as [->|?].
-    - rewrite !lookup_insert. naive_solver.
-    - rewrite !lookup_insert_ne by done. symmetry. apply map_filter_lookup_Some.
-  Qed.
-
-  Lemma map_filter_insert_not' m i x :
-    ¬ P (i, x) → (∀ y, m !! i = Some y → ¬ P (i, y)) →
-    filter P (<[i:=x]> m) = filter P m.
-  Proof.
-    intros Hx HP. apply map_filter_strong_ext. intros j y.
-    rewrite lookup_insert_Some. naive_solver.
-  Qed.
-  Lemma map_filter_insert_not m i x :
-    (∀ y, ¬ P (i, y)) → filter P (<[i:=x]> m) = filter P m.
-  Proof. intros HP. by apply map_filter_insert_not'. Qed.
-
-  Lemma map_filter_insert_not_delete m i x :
-    ¬ P (i, x) → filter P (<[i:=x]> m) = filter P (delete i m).
-  Proof.
-    intros. rewrite <-insert_delete_insert by done.
-    rewrite map_filter_insert_not'; [done..|].
-    rewrite lookup_delete; done.
-  Qed.
-
   Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m).
   Proof.
     apply map_eq. intros j. apply option_eq; intros y.
@@ -1341,14 +1313,40 @@ Section map_filter_insert_and_delete.
     - rewrite lookup_delete_ne, !map_filter_lookup_Some, lookup_delete_ne by done.
       naive_solver.
   Qed.
-
   Lemma map_filter_delete_not m i:
-    (∀ y, ¬ P (i, y)) → filter P (delete i m) = filter P m.
+    (∀ y, m !! i = Some y → ¬ P (i, y)) →
+    filter P (delete i m) = filter P m.
+  Proof.
+    intros. apply map_filter_strong_ext. intros j y.
+    rewrite lookup_delete_Some. naive_solver.
+  Qed.
+
+  Lemma map_filter_insert m i x :
+    filter P (<[i:=x]> m)
+    = if decide (P (i, x)) then <[i:=x]> (filter P m) else filter P (delete i m).
+  Proof.
+    apply map_eq. intros j. apply option_eq; intros y.
+    rewrite map_filter_lookup_Some, lookup_insert_Some. case_decide.
+    - rewrite lookup_insert_Some, map_filter_lookup_Some. naive_solver.
+    - rewrite map_filter_lookup_Some, lookup_delete_Some. naive_solver.
+  Qed.
+  Lemma map_filter_insert_True m i x :
+    P (i, x) → filter P (<[i:=x]> m) = <[i:=x]> (filter P m).
+  Proof. intros. by rewrite map_filter_insert, decide_True. Qed.
+  Lemma map_filter_insert_False m i x :
+    ¬ P (i, x) → filter P (<[i:=x]> m) = filter P (delete i m).
+  Proof. intros. by rewrite map_filter_insert, decide_False. Qed.
+
+  Lemma map_filter_insert_not' m i x :
+    ¬ P (i, x) → (∀ y, m !! i = Some y → ¬ P (i, y)) →
+    filter P (<[i:=x]> m) = filter P m.
   Proof.
-    intros ?. case (m !! i) as [x|] eqn:?.
-    - by rewrite <-(map_filter_insert_not_delete _ _ x), insert_id by done.
-    - by rewrite delete_notin.
+    intros. rewrite map_filter_insert, decide_False by done.
+    by rewrite map_filter_delete_not.
   Qed.
+  Lemma map_filter_insert_not m i x :
+    (∀ y, ¬ P (i, y)) → filter P (<[i:=x]> m) = filter P m.
+  Proof. intros. by apply map_filter_insert_not'. Qed.
 End map_filter_insert_and_delete.
 
 Section map_filter_misc.
@@ -1372,7 +1370,7 @@ Section map_filter_misc.
     apply list_to_map_flip. induction m as [|k x m ? IH] using map_ind.
     { by rewrite map_to_list_empty, map_filter_empty, map_to_list_empty. }
     rewrite map_to_list_insert, filter_cons by done. destruct (decide (P _)).
-    - rewrite map_filter_insert by done.
+    - rewrite map_filter_insert_True by done.
       by rewrite map_to_list_insert, IH by (rewrite map_filter_lookup_None; auto).
     - by rewrite map_filter_insert_not' by naive_solver.
   Qed.
@@ -2764,12 +2762,11 @@ Section setoid_inversion.
     revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hm.
     { rewrite map_filter_empty in Hm. exists ∅.
       by rewrite map_filter_empty, <-map_empty_equiv_eq. }
-    destruct (decide (P (i,x))).
-    - rewrite map_filter_insert in Hm by done.
-      apply insert_equiv_eq in Hm as (x'&m2'&->&?&(m2''&->&?)%IH).
+    rewrite map_filter_insert in Hm. case_decide.
+    - apply insert_equiv_eq in Hm as (x'&m2'&->&?&(m2''&->&?)%IH).
       exists (<[i:=x']> m2''). split; [|by f_equiv].
-      by rewrite map_filter_insert by (by eapply HP).
-    - rewrite map_filter_insert_not' in Hm by naive_solver.
+      by rewrite map_filter_insert_True by (by eapply HP).
+    - rewrite delete_notin in Hm by done.
       apply IH in Hm as (m2'&->&Hm2). exists (<[i:=x]> m2'). split; [|by f_equiv].
       assert (m2' !! i = None).
       { by rewrite <-None_equiv_eq, Hm2, None_equiv_eq. }