diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 9e81bb8dfcabda6f4db4ed8f2051d1b70b40df02..126f67a6b8ae21be6d807e7960caea27be4d5768 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -523,16 +523,21 @@ Proof.
     eauto using alloc_unit_singleton_updateP with subst.
 Qed.
 
+Lemma gmap_local_update m1 m2 m1' m2' :
+  (∀ i, (m1 !! i, m2 !! i) ~l~> (m1' !! i, m2' !! i)) →
+  (m1, m2) ~l~> (m1', m2').
+Proof.
+  intros Hupd. apply local_update_unital=> n mf Hmv Hm.
+  apply forall_and_distr=> i. rewrite lookup_op -cmra_opM_fmap_Some.
+  apply Hupd; simpl; first done. by rewrite Hm lookup_op cmra_opM_fmap_Some.
+Qed.
+
 Lemma alloc_local_update m1 m2 i x :
   m1 !! i = None → ✓ x → (m1,m2) ~l~> (<[i:=x]>m1, <[i:=x]>m2).
 Proof.
-  rewrite cmra_valid_validN=> Hi ?.
-  apply local_update_unital=> n mf Hmv Hm; simpl in *.
-  split; auto using insert_validN.
-  intros j; destruct (decide (i = j)) as [->|].
-  - move: (Hm j); rewrite Hi symmetry_iff dist_None lookup_op op_None=>-[_ Hj].
-    by rewrite lookup_op !lookup_insert Hj.
-  - rewrite Hm lookup_insert_ne // !lookup_op lookup_insert_ne //.
+  intros Hi ?. apply gmap_local_update=> j.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_insert_ne.
+  rewrite !lookup_insert Hi. by apply alloc_option_local_update.
 Qed.
 
 Lemma alloc_singleton_local_update m i x :
@@ -544,24 +549,20 @@ Lemma insert_local_update m1 m2 i x y x' y' :
   (x, y) ~l~> (x', y') →
   (m1, m2) ~l~> (<[i:=x']>m1, <[i:=y']>m2).
 Proof.
-  intros Hi1 Hi2 Hup; apply local_update_unital=> n mf Hmv Hm; simpl in *.
-  destruct (Hup n (mf !! i)) as [? Hx']; simpl in *.
-  { move: (Hmv i). by rewrite Hi1. }
-  { move: (Hm i). by rewrite lookup_op Hi1 Hi2 Some_op_opM (inj_iff Some). }
-  split; auto using insert_validN.
-  rewrite Hm Hx'=> j; destruct (decide (i = j)) as [->|].
-  - by rewrite lookup_insert lookup_op lookup_insert Some_op_opM.
-  - by rewrite lookup_insert_ne // !lookup_op lookup_insert_ne.
+  intros Hi1 Hi2 Hup. apply gmap_local_update=> j.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_insert_ne.
+  rewrite !lookup_insert Hi1 Hi2. by apply option_local_update.
 Qed.
 
 Lemma singleton_local_update_any m i y x' y' :
   (∀ x, m !! i = Some x → (x, y) ~l~> (x', y')) →
   (m, {[ i := y ]}) ~l~> (<[i:=x']>m, {[ i := y' ]}).
 Proof.
-  intros. rewrite /singletonM /map_singleton -(insert_insert ∅ i y' y).
-  apply local_update_total_valid0=>_ _ /singleton_includedN_l [x0 [/dist_Some_inv_r Hlk0 _]].
-  edestruct Hlk0 as [x [Hlk _]]; [done..|].
-  eapply insert_local_update; [|eapply lookup_insert|]; eauto.
+  intros. apply gmap_local_update=> j.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_insert_ne.
+  rewrite !lookup_singleton lookup_insert.
+  destruct (m !! j); first by eauto using option_local_update.
+  apply local_update_total_valid0=> _ _ /option_includedN; naive_solver.
 Qed.
 
 Lemma singleton_local_update m i x y x' y' :
@@ -576,13 +577,9 @@ Qed.
 Lemma delete_local_update m1 m2 i x `{!Exclusive x} :
   m2 !! i = Some x → (m1, m2) ~l~> (delete i m1, delete i m2).
 Proof.
-  intros Hi. apply local_update_unital=> n mf Hmv Hm; simpl in *.
-  split; auto using delete_validN.
-  rewrite Hm=> j; destruct (decide (i = j)) as [<-|].
-  - rewrite lookup_op !lookup_delete left_id symmetry_iff dist_None.
-    apply eq_None_not_Some=> -[y Hi'].
-    move: (Hmv i). rewrite Hm lookup_op Hi Hi' -Some_op. by apply exclusiveN_l.
-  - by rewrite lookup_op !lookup_delete_ne // lookup_op.
+  intros Hi. apply gmap_local_update=> j.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_delete_ne.
+  rewrite !lookup_delete Hi. by apply delete_option_local_update.
 Qed.
 
 Lemma delete_singleton_local_update m i x `{!Exclusive x} :
@@ -596,12 +593,9 @@ Lemma delete_local_update_cancelable m1 m2 i mx `{!Cancelable mx} :
   m1 !! i ≡ mx → m2 !! i ≡ mx →
   (m1, m2) ~l~> (delete i m1, delete i m2).
 Proof.
-  intros Hm1i Hm2i. apply local_update_unital=> n mf Hmv Hm; simpl in *.
-  split; [eauto using delete_validN|].
-  intros j. destruct (decide (i = j)) as [->|].
-  - move: (Hm j). rewrite !lookup_op Hm1i Hm2i !lookup_delete. intros Hmx.
-    rewrite (cancelableN mx n (mf !! j) None) ?right_id // -Hmx -Hm1i. apply Hmv.
-  - by rewrite lookup_op !lookup_delete_ne // Hm lookup_op.
+  intros Hi1 Hi2. apply gmap_local_update=> j.
+  destruct (decide (i = j)) as [->|]; last by rewrite !lookup_delete_ne.
+  rewrite !lookup_delete Hi1 Hi2. by apply delete_option_local_update_cancelable.
 Qed.
 
 Lemma delete_singleton_local_update_cancelable m i x `{!Cancelable (Some x)} :
diff --git a/iris/algebra/local_updates.v b/iris/algebra/local_updates.v
index c8a854745757ddfb77018b9a026f62a2870355c6..24592eedec10f693c1c39f8916ddfc1ed36c6292 100644
--- a/iris/algebra/local_updates.v
+++ b/iris/algebra/local_updates.v
@@ -160,8 +160,6 @@ Lemma prod_local_update_2 {A B : cmra} (x1 y1 : A) (x2 y2 x2' y2' : B) :
 Proof. intros. by apply prod_local_update. Qed.
 
 (** * Option *)
-(* TODO: Investigate whether we can use these in proving the very similar local
-   updates on finmaps. *)
 Lemma option_local_update {A : cmra} (x y x' y' : A) :
   (x, y) ~l~> (x',y') →
   (Some x, Some y) ~l~> (Some x', Some y').