diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index a7a9657766ac14c20432a379342cd9660ce7c5af..5ebe71471eb3753baf62181766d389c6e8da86d8 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -314,11 +314,15 @@ Global Instance singleton_is_op i a a1 a2 :
   IsOp a a1 a2 → IsOp' ({[ i := a ]} : gmap K A) {[ i := a1 ]} {[ i := a2 ]}.
 Proof. rewrite /IsOp' /IsOp=> ->. by rewrite -singleton_op. Qed.
 
-Global Instance gmap_core_id m : (∀ x : A, CoreId x) → CoreId m.
+Lemma gmap_core_id m : (∀ i x, m !! i = Some x → CoreId x) → CoreId m.
 Proof.
-  intros; apply core_id_total=> i.
-  rewrite lookup_core. apply (core_id_core _).
+  intros Hcore; apply core_id_total=> i.
+  rewrite lookup_core. destruct (m !! i) as [x|] eqn:Hix; rewrite Hix; [|done].
+  by eapply Hcore.
 Qed.
+Global Instance gmap_core_id' m : (∀ x : A, CoreId x) → CoreId m.
+Proof. auto using gmap_core_id. Qed.
+
 Global Instance gmap_singleton_core_id i (x : A) :
   CoreId x → CoreId {[ i := x ]}.
 Proof. intros. by apply core_id_total, singleton_core'. Qed.