diff --git a/CHANGELOG.md b/CHANGELOG.md
index eb55cc22610e406d0ed6f3ccf90acb8de1652dac..bade5df0d729a3dd47673da0e2aebbfdde45622c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -155,6 +155,8 @@ API-breaking change is listed.
   does not unfold `gset` operations. (by Paolo G. Giarrusso, BedRock Systems)
 - Add `get_head` tactic to determine the syntactic head of a function
   application term.
+- Add map lookup lemmas: `lookup_union_is_Some`, `lookup_difference_is_Some`,
+  `lookup_union_Some_l_inv`, `lookup_union_Some_r_inv`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index a6211d3eefa59811f2f097137b80e0f6b4524091..653842a565d3dc83b1f9b18077b2d5a6cc96c15c 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2043,13 +2043,6 @@ Proof. rewrite lookup_union. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
 Lemma lookup_union_None {A} (m1 m2 : M A) i :
   (m1 ∪ m2) !! i = None ↔ m1 !! i = None ∧ m2 !! i = None.
 Proof. rewrite lookup_union.  destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
-Lemma map_positive_l {A} (m1 m2 : M A) : m1 ∪ m2 = ∅ → m1 = ∅.
-Proof.
-  intros Hm. apply map_empty. intros i. apply (f_equal (.!! i)) in Hm.
-  rewrite lookup_empty, lookup_union_None in Hm; tauto.
-Qed.
-Lemma map_positive_l_alt {A} (m1 m2 : M A) : m1 ≠ ∅ → m1 ∪ m2 ≠ ∅.
-Proof. eauto using map_positive_l. Qed.
 Lemma lookup_union_Some {A} (m1 m2 : M A) i x :
   m1 ##ₘ m2 → (m1 ∪ m2) !! i = Some x ↔ m1 !! i = Some x ∨ m2 !! i = Some x.
 Proof.
@@ -2062,6 +2055,19 @@ Proof. intro. rewrite lookup_union_Some_raw; intuition. Qed.
 Lemma lookup_union_Some_r {A} (m1 m2 : M A) i x :
   m1 ##ₘ m2 → m2 !! i = Some x → (m1 ∪ m2) !! i = Some x.
 Proof. intro. rewrite lookup_union_Some; intuition. Qed.
+Lemma lookup_union_Some_inv_l {A} (m1 m2 : M A) i x :
+  (m1 ∪ m2) !! i = Some x → m2 !! i = None → m1 !! i = Some x.
+Proof. rewrite lookup_union_Some_raw. naive_solver. Qed.
+Lemma lookup_union_Some_inv_r {A} (m1 m2 : M A) i x :
+  (m1 ∪ m2) !! i = Some x → m1 !! i = None → m2 !! i = Some x.
+Proof. rewrite lookup_union_Some_raw. naive_solver. Qed.
+Lemma lookup_union_is_Some {A} (m1 m2 : M A) i :
+  is_Some ((m1 ∪ m2) !! i) ↔ is_Some (m1 !! i) ∨ is_Some (m2 !! i).
+Proof.
+  rewrite <-!not_eq_None_Some, !lookup_union_None.
+  destruct (m1 !! i); naive_solver.
+Qed.
+
 Lemma map_union_comm {A} (m1 m2 : M A) : m1 ##ₘ m2 → m1 ∪ m2 = m2 ∪ m1.
 Proof.
   intros Hdisjoint. apply (merge_comm (union_with (λ x _, Some x))).
@@ -2069,6 +2075,14 @@ Proof.
   destruct (m1 !! i), (m2 !! i); compute; naive_solver.
 Qed.
 
+Lemma map_positive_l {A} (m1 m2 : M A) : m1 ∪ m2 = ∅ → m1 = ∅.
+Proof.
+  intros Hm. apply map_empty. intros i. apply (f_equal (.!! i)) in Hm.
+  rewrite lookup_empty, lookup_union_None in Hm; tauto.
+Qed.
+Lemma map_positive_l_alt {A} (m1 m2 : M A) : m1 ≠ ∅ → m1 ∪ m2 ≠ ∅.
+Proof. eauto using map_positive_l. Qed.
+
 Lemma map_subseteq_union {A} (m1 m2 : M A) : m1 ⊆ m2 → m1 ∪ m2 = m2.
 Proof.
   rewrite map_subseteq_spec.
@@ -2525,6 +2539,9 @@ Proof.
   unfold difference, map_difference; rewrite lookup_difference_with.
   destruct (m1 !! i), (m2 !! i); compute; intuition congruence.
 Qed.
+Lemma lookup_difference_is_Some {A} (m1 m2 : M A) i :
+  is_Some ((m1 ∖ m2) !! i) ↔ is_Some (m1 !! i) ∧ m2 !! i = None.
+Proof. unfold is_Some. setoid_rewrite lookup_difference_Some. naive_solver. Qed.
 Lemma lookup_difference_None {A} (m1 m2 : M A) i :
   (m1 ∖ m2) !! i = None ↔ m1 !! i = None ∨ is_Some (m2 !! i).
 Proof.