diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9e159d300fec94aa91ed91de143368f487f328ce..2df67374d4cf24beb1b6e92157e3f4520050a96f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -88,6 +88,8 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
   `big_sepL_lookup_acc_impl`, `big_sepL2_lookup_acc_impl`,
   `big_sepM_lookup_acc_impl`, `big_sepM2_lookup_acc_impl`,
   `big_sepS_elem_of_acc_impl`, `big_sepMS_elem_of_acc_impl`.
+* Add lemmas `big_sepM_filter'` and `big_sepM_filter` matching the corresponding
+  `big_sepS` lemmas.
 
 **Changes in `proofmode`:**
 
diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index 1c6aafe2c7c7ef87c7951f73a9a40c29abbb4316..a56da2ac8c8aee78070c5859a970549cf29407f6 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -396,6 +396,20 @@ Section gmap.
     ([^o map] k↦y ∈ <[i:=x]> m, <[i:=P]> f k) ≡ (P `o` [^o map] k↦y ∈ m, f k).
   Proof. apply (big_opM_fn_insert (λ _ _, id)). Qed.
 
+  Lemma big_opM_filter' (φ : K * A → Prop) `{∀ kx, Decision (φ kx)} f m :
+    ([^o map] k ↦ x ∈ filter φ m, f k x)
+    ≡ ([^o map] k ↦ x ∈ m, if decide (φ (k, x)) then f k x else monoid_unit).
+  Proof.
+    induction m as [|k v m ? IH] using map_ind.
+    { by rewrite map_filter_empty !big_opM_empty. }
+    destruct (decide (φ (k, v))).
+    - rewrite map_filter_insert //.
+      assert (filter φ m !! k = None) by (apply map_filter_lookup_None; eauto).
+      by rewrite !big_opM_insert // decide_True // IH.
+    - rewrite map_filter_insert_not' //; last by congruence.
+      rewrite !big_opM_insert // decide_False // IH. by rewrite left_id.
+  Qed.
+
   Lemma big_opM_union f m1 m2 :
     m1 ##ₘ m2 →
     ([^o map] k↦y ∈ m1 ∪ m2, f k y)
@@ -522,6 +536,20 @@ Section gset.
     by induction X using set_ind_L; rewrite /= ?big_opS_insert ?left_id // big_opS_eq.
   Qed.
 
+  Lemma big_opS_filter' (φ : A → Prop) `{∀ x, Decision (φ x)} f X :
+    ([^o set] y ∈ filter φ X, f y)
+    ≡ ([^o set] y ∈ X, if decide (φ y) then f y else monoid_unit).
+  Proof.
+    induction X as [|x X ? IH] using set_ind_L.
+    { by rewrite filter_empty_L !big_opS_empty. }
+    destruct (decide (φ x)).
+    - rewrite filter_union_L filter_singleton_L //.
+      rewrite !big_opS_insert //; last set_solver.
+      by rewrite decide_True // IH.
+    - rewrite filter_union_L filter_singleton_not_L // left_id_L.
+      by rewrite !big_opS_insert // decide_False // IH left_id.
+  Qed.
+
   Lemma big_opS_op f g X :
     ([^o set] y ∈ X, f y `o` g y) ≡ ([^o set] y ∈ X, f y) `o` ([^o set] y ∈ X, g y).
   Proof. by rewrite big_opS_eq /big_opS_def -big_opL_op. Qed.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 323b2e2c22cb044e0092447781797b7ca1dc1452..680771920e617911b891047d3c2ec15f409f2d88 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -1137,6 +1137,16 @@ Section map.
     ([∗ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ∗ [∗ map] k↦y ∈ m, Φ k).
   Proof. apply big_opM_fn_insert'. Qed.
 
+  Lemma big_sepM_filter' (φ : K * A → Prop) `{∀ kx, Decision (φ kx)} Φ m :
+    ([∗ map] k ↦ x ∈ filter φ m, Φ k x) ⊣⊢
+    ([∗ map] k ↦ x ∈ m, if decide (φ (k, x)) then Φ k x else emp).
+  Proof. apply: big_opM_filter'. Qed.
+  Lemma big_sepM_filter `{BiAffine PROP}
+      (φ : K * A → Prop) `{∀ kx, Decision (φ kx)} Φ m :
+    ([∗ map] k ↦ x ∈ filter φ m, Φ k x) ⊣⊢
+    ([∗ map] k ↦ x ∈ m, ⌜φ (k, x)⌝ → Φ k x).
+  Proof. setoid_rewrite <-decide_emp. apply big_sepM_filter'. Qed.
+
   Lemma big_sepM_union Φ m1 m2 :
     m1 ##ₘ m2 →
     ([∗ map] k↦y ∈ m1 ∪ m2, Φ k y)
@@ -1809,43 +1819,32 @@ Section gset.
   Lemma big_sepS_singleton Φ x : ([∗ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x.
   Proof. apply big_opS_singleton. Qed.
 
-  Lemma big_sepS_filter' (P : A → Prop) `{∀ x, Decision (P x)} Φ X :
-    ([∗ set] y ∈ filter P X, Φ y)
-    ⊣⊢ ([∗ set] y ∈ X, if decide (P y) then Φ y else emp).
-  Proof.
-    induction X as [|x X ? IH] using set_ind_L.
-    { by rewrite filter_empty_L !big_sepS_empty. }
-    destruct (decide (P x)).
-    - rewrite filter_union_L filter_singleton_L //.
-      rewrite !big_sepS_insert //; last set_solver.
-      by rewrite decide_True // IH.
-    - rewrite filter_union_L filter_singleton_not_L // left_id_L.
-      by rewrite !big_sepS_insert // decide_False // IH left_id.
-  Qed.
+  Lemma big_sepS_filter' (φ : A → Prop) `{∀ x, Decision (φ x)} Φ X :
+    ([∗ set] y ∈ filter φ X, Φ y)
+    ⊣⊢ ([∗ set] y ∈ X, if decide (φ y) then Φ y else emp).
+  Proof. apply: big_opS_filter'. Qed.
+  Lemma big_sepS_filter `{BiAffine PROP}
+      (φ : A → Prop) `{∀ x, Decision (φ x)} Φ X :
+    ([∗ set] y ∈ filter φ X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ⌜φ y⌝ → Φ y).
+  Proof. setoid_rewrite <-decide_emp. apply big_sepS_filter'. Qed.
 
-  Lemma big_sepS_filter_acc' (P : A → Prop) `{∀ y, Decision (P y)} Φ X Y :
-    (∀ y, y ∈ Y → P y → y ∈ X) →
+  Lemma big_sepS_filter_acc' (φ : A → Prop) `{∀ y, Decision (φ y)} Φ X Y :
+    (∀ y, y ∈ Y → φ y → y ∈ X) →
     ([∗ set] y ∈ X, Φ y) -∗
-      ([∗ set] y ∈ Y, if decide (P y) then Φ y else emp) ∗
-      (([∗ set] y ∈ Y, if decide (P y) then Φ y else emp) -∗ [∗ set] y ∈ X, Φ y).
+      ([∗ set] y ∈ Y, if decide (φ y) then Φ y else emp) ∗
+      (([∗ set] y ∈ Y, if decide (φ y) then Φ y else emp) -∗ [∗ set] y ∈ X, Φ y).
   Proof.
-    intros ?. destruct (proj1 (subseteq_disjoint_union_L (filter P Y) X))
+    intros ?. destruct (proj1 (subseteq_disjoint_union_L (filter φ Y) X))
       as (Z&->&?); first set_solver.
     rewrite big_sepS_union // big_sepS_filter'.
     by apply sep_mono_r, wand_intro_l.
   Qed.
-
-  Lemma big_sepS_filter `{BiAffine PROP}
-      (P : A → Prop) `{∀ x, Decision (P x)} Φ X :
-    ([∗ set] y ∈ filter P X, Φ y) ⊣⊢ ([∗ set] y ∈ X, ⌜P y⌝ → Φ y).
-  Proof. setoid_rewrite <-decide_emp. apply big_sepS_filter'. Qed.
-
   Lemma big_sepS_filter_acc `{BiAffine PROP}
-      (P : A → Prop) `{∀ y, Decision (P y)} Φ X Y :
-    (∀ y, y ∈ Y → P y → y ∈ X) →
+      (φ : A → Prop) `{∀ y, Decision (φ y)} Φ X Y :
+    (∀ y, y ∈ Y → φ y → y ∈ X) →
     ([∗ set] y ∈ X, Φ y) -∗
-      ([∗ set] y ∈ Y, ⌜P y⌝ → Φ y) ∗
-      (([∗ set] y ∈ Y, ⌜P y⌝ → Φ y) -∗ [∗ set] y ∈ X, Φ y).
+      ([∗ set] y ∈ Y, ⌜φ y⌝ → Φ y) ∗
+      (([∗ set] y ∈ Y, ⌜φ y⌝ → Φ y) -∗ [∗ set] y ∈ X, Φ y).
   Proof. intros. setoid_rewrite <-decide_emp. by apply big_sepS_filter_acc'. Qed.
 
   Lemma big_sepS_list_to_set Φ (l : list A) :