diff --git a/CHANGELOG.md b/CHANGELOG.md
index deec3e67a689e01d2ffa3f21c3b21c28ed928168..69b247d4f7bcb6f9053e437c6fb3d02b904731f6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -43,6 +43,15 @@ API-breaking change is listed.
 - Set `Hint Mode` for the classes `PartialOrder`, `TotalOrder`, `MRet`, `MBind`,
   `MJoin`, `FMap`, `OMap`, `MGuard`, `SemiSet`, `Set_`, `TopSet`, and `Infinite`.
 - Make `map_filter_strong_ext` and `map_filter_ext` bidirectional.
+- Make collection of lemmas for filter + union/disjoint consistent for sets and
+  maps:
+  + Sets: Add lemmas `disjoint_filter`, `disjoint_filter_complement`, and
+    `filter_union_complement`.
+  + Maps: Rename `map_disjoint_filter` → `map_disjoint_filter_complement` and
+    `map_union_filter` → `map_filter_union_complement` to be consistent with sets.
+  + Maps: Add lemmas `map_disjoint_filter` and `map_filter_union` analogous to
+    sets.
+- Add cross split lemma `map_cross_split` for maps
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
@@ -54,6 +63,9 @@ s/\bdecide_right\b/decide_False_pi/g
 s/\bPermutation_nil\b/Permutation_nil_r/g
 s/\bPermutation_singleton\b/Permutation_singleton_r/g
 s/\Permutation_cons_inv\b/Permutation_cons_inv_r/g
+# Filter
+s/\bmap_disjoint_filter\b/map_disjoint_filter_complement/g
+s/\bmap_union_filter\b/map_filter_union_complement/g
 ' $(find theories -name "*.v")
 ```
 
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index c955877ec89249d84865e842d6bf18a7575faf15..d46161ad4702b70cebe632f37134c2892a988304 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -182,7 +182,7 @@ Proof.
   intros.
   exists (filter (λ '(k,x), k ∈ X1) m), (filter (λ '(k,x), k ∉ X1) m).
   assert (filter (λ '(k, _), k ∈ X1) m ##ₘ filter (λ '(k, _), k ∉ X1) m).
-  { apply map_disjoint_filter. }
+  { apply map_disjoint_filter_complement. }
   split_and!; [|done| |].
   - apply map_eq; intros i. apply option_eq; intros x.
     rewrite lookup_union_Some, !map_filter_lookup_Some by done.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 2b568bfca9a603ed28df8c8a92d8789dc6dffa2c..3c56b7360473c3c6d3da37d699d862859f9aca4b 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1868,7 +1868,15 @@ Proof.
 Qed.
 Lemma map_disjoint_delete_r {A} (m1 m2 : M A) i : m1 ##ₘ m2 → m1 ##ₘ delete i m2.
 Proof. symmetry. by apply map_disjoint_delete_l. Qed.
-Lemma map_disjoint_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
+
+Lemma map_disjoint_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m1 m2 : M A) :
+  m1 ##ₘ m2 → filter P m1 ##ₘ filter P m2.
+Proof.
+  rewrite !map_disjoint_spec. intros ? i x y.
+  rewrite !map_filter_lookup_Some. naive_solver.
+Qed.
+Lemma map_disjoint_filter_complement {A} (P : K * A → Prop)
+    `{!∀ x, Decision (P x)} (m : M A) :
   filter P m ##ₘ filter (λ v, ¬ P v) m.
 Proof.
   apply map_disjoint_spec. intros i x y.
@@ -2184,11 +2192,21 @@ Proof.
   naive_solver eauto using map_Forall_union_1_1,
     map_Forall_union_1_2, map_Forall_union_2.
 Qed.
-Lemma map_union_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
+Lemma map_filter_union {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m1 m2 : M A) :
+  m1 ##ₘ m2 →
+  filter P (m1 ∪ m2) = filter P m1 ∪ filter P m2.
+Proof.
+  intros. apply map_eq; intros i. apply option_eq; intros x.
+  rewrite lookup_union_Some, !map_filter_lookup_Some,
+    lookup_union_Some by auto using map_disjoint_filter.
+  naive_solver.
+Qed.
+Lemma map_filter_union_complement {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
   filter P m ∪ filter (λ v, ¬ P v) m = m.
 Proof.
   apply map_eq; intros i. apply option_eq; intros x.
-  rewrite lookup_union_Some, !map_filter_lookup_Some by apply map_disjoint_filter.
+  rewrite lookup_union_Some, !map_filter_lookup_Some
+    by auto using map_disjoint_filter_complement.
   destruct (decide (P (i,x))); naive_solver.
 Qed.
 Lemma map_fmap_union {A B} (f : A → B) (m1 m2 : M A) :
@@ -2208,6 +2226,31 @@ Proof.
   destruct (m1 !! i), (m2 !! i); simpl; repeat (destruct (f _)); naive_solver.
 Qed.
 
+Lemma map_cross_split {A} (m ma mb mc md : M A) :
+  ma ##ₘ mb → mc ##ₘ md →
+  ma ∪ mb = m → mc ∪ md = m →
+  ∃ mac mad mbc mbd,
+    mac ##ₘ mad ∧ mbc ##ₘ mbd ∧
+    mac ##ₘ mbc ∧ mad ##ₘ mbd ∧
+    mac ∪ mad = ma ∧ mbc ∪ mbd = mb ∧ mac ∪ mbc = mc ∧ mad ∪ mbd = md.
+Proof.
+  intros Hab_disj Hcd_disj Hab Hcd.
+  exists (filter (λ kx, is_Some (mc !! kx.1)) ma),
+    (filter (λ kx, ¬is_Some (mc !! kx.1)) ma),
+    (filter (λ kx, is_Some (mc !! kx.1)) mb),
+    (filter (λ kx, ¬is_Some (mc !! kx.1)) mb).
+  split_and!; [auto using map_disjoint_filter_complement, map_disjoint_filter,
+    map_filter_union_complement..| |].
+  - rewrite <-map_filter_union, Hab, <-Hcd by done.
+    apply map_eq; intros k. apply option_eq; intros x.
+    rewrite map_filter_lookup_Some, lookup_union_Some, <-not_eq_None_Some by done.
+    rewrite map_disjoint_alt in Hcd_disj; naive_solver.
+  - rewrite <-map_filter_union, Hab, <-Hcd by done.
+    apply map_eq; intros k. apply option_eq; intros x.
+    rewrite map_filter_lookup_Some, lookup_union_Some, <-not_eq_None_Some by done.
+    rewrite map_disjoint_alt in Hcd_disj; naive_solver.
+Qed.
+
 (** ** Properties of the [union_list] operation *)
 Lemma map_disjoint_union_list_l {A} (ms : list (M A)) (m : M A) :
   ⋃ ms ##ₘ m ↔ Forall (.##ₘ m) ms.
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 8ae76e1961dde3857eccbed93f1400078224ef44..2aaa7c5361acef463dd63a664ec0e5e883af6b5e 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -302,39 +302,50 @@ Lemma minimal_exists_L R `{!LeibnizEquiv C, !Transitive R,
 Proof. unfold_leibniz. apply (minimal_exists R). Qed.
 
 (** * Filter *)
+Lemma elem_of_filter (P : A → Prop) `{!∀ x, Decision (P x)} X x :
+  x ∈ filter P X ↔ P x ∧ x ∈ X.
+Proof.
+  unfold filter, set_filter.
+  by rewrite elem_of_list_to_set, elem_of_list_filter, elem_of_elements.
+Qed.
+Global Instance set_unfold_filter (P : A → Prop) `{!∀ x, Decision (P x)} X Q x :
+  SetUnfoldElemOf x X Q → SetUnfoldElemOf x (filter P X) (P x ∧ Q).
+Proof.
+  intros ?; constructor. by rewrite elem_of_filter, (set_unfold_elem_of x X Q).
+Qed.
+
 Section filter.
   Context (P : A → Prop) `{!∀ x, Decision (P x)}.
 
-  Lemma elem_of_filter X x : x ∈ filter P X ↔ P x ∧ x ∈ X.
-  Proof.
-    unfold filter, set_filter.
-    by rewrite elem_of_list_to_set, elem_of_list_filter, elem_of_elements.
-  Qed.
-  Global Instance set_unfold_filter X Q x :
-    SetUnfoldElemOf x X Q → SetUnfoldElemOf x (filter P X) (P x ∧ Q).
-  Proof.
-    intros ?; constructor. by rewrite elem_of_filter, (set_unfold_elem_of x X Q).
-  Qed.
-
   Lemma filter_empty : filter P (∅:C) ≡ ∅.
   Proof. set_solver. Qed.
-  Lemma filter_union X Y : filter P (X ∪ Y) ≡ filter P X ∪ filter P Y.
-  Proof. set_solver. Qed.
   Lemma filter_singleton x : P x → filter P ({[ x ]} : C) ≡ {[ x ]}.
   Proof. set_solver. Qed.
   Lemma filter_singleton_not x : ¬P x → filter P ({[ x ]} : C) ≡ ∅.
   Proof. set_solver. Qed.
 
+  Lemma disjoint_filter X Y : X ## Y → filter P X ## filter P Y.
+  Proof. set_solver. Qed.
+  Lemma filter_union X Y : filter P (X ∪ Y) ≡ filter P X ∪ filter P Y.
+  Proof. set_solver. Qed.
+  Lemma disjoint_filter_complement X : filter P X ## filter (λ x, ¬P x) X.
+  Proof. set_solver. Qed.
+  Lemma filter_union_complement X : filter P X ∪ filter (λ x, ¬P x) X ≡ X.
+  Proof. intros x. destruct (decide (P x)); set_solver. Qed.
+
   Section leibniz_equiv.
     Context `{!LeibnizEquiv C}.
     Lemma filter_empty_L : filter P (∅:C) = ∅.
-    Proof. set_solver. Qed.
-    Lemma filter_union_L X Y : filter P (X ∪ Y) = filter P X ∪ filter P Y.
-    Proof. set_solver. Qed.
+    Proof. unfold_leibniz. apply filter_empty. Qed.
     Lemma filter_singleton_L x : P x → filter P ({[ x ]} : C) = {[ x ]}.
-    Proof. set_solver. Qed.
+    Proof. unfold_leibniz. apply filter_singleton. Qed.
     Lemma filter_singleton_not_L x : ¬P x → filter P ({[ x ]} : C) = ∅.
-    Proof. set_solver. Qed.
+    Proof. unfold_leibniz. apply filter_singleton_not. Qed.
+
+    Lemma filter_union_L X Y : filter P (X ∪ Y) = filter P X ∪ filter P Y.
+    Proof. unfold_leibniz. apply filter_union. Qed.
+    Lemma filter_union_complement_L X Y : filter P X ∪ filter (λ x, ¬P x) X = X.
+    Proof. unfold_leibniz. apply filter_union_complement. Qed.
   End leibniz_equiv.
 End filter.