diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index 1c6aafe2c7c7ef87c7951f73a9a40c29abbb4316..39b6b0bbcf057501804f0eb8a7c2b8a8347ab57c 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' f (φ : K * A → Prop) `{∀ kx, Decision (φ kx)} 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' f (φ : A → Prop) `{∀ x, Decision (φ x)} 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 a2c17f4bef5c5658d83e7b9343c0de1a3432b4d6..19f48d4014ad3fc6be08253d1933768ab38de3be 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -1137,25 +1137,14 @@ 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' Φ (P : K * A → Prop) `{∀ k, Decision (P k)} m :
-    ([∗ map] k ↦ x ∈ filter P m, Φ k x) ⊣⊢
-    ([∗ map] k ↦ x ∈ m, if decide (P (k, x)) then Φ k x else emp).
-  Proof.
-    induction m as [|k v m ? IH] using map_ind.
-    { by rewrite map_filter_empty !big_sepM_empty. }
-    destruct (decide (P (k, v))).
-    - rewrite map_filter_insert //.
-      rewrite !big_sepM_insert //.
-      * by rewrite decide_True // IH.
-      * apply map_filter_lookup_None; eauto.
-    - rewrite map_filter_insert_not' //; last by congruence.
-      rewrite !big_sepM_insert // decide_False // IH. rewrite left_id. eauto.
-  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}
-      Φ (P : K * A → Prop) `{∀ k, Decision (P k)} m :
-    ([∗ map] k ↦ x ∈ filter P m, Φ k x) ⊣⊢
-    ([∗ map] k ↦ x ∈ m, ⌜P (k, x)⌝ → Φ k x).
+      Φ (φ : 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 :
@@ -1830,19 +1819,14 @@ 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) →
@@ -1855,12 +1839,6 @@ Section gset.
     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) →