diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index 00f829c2f3c4f1a935c3e0269c743036efbf57a3..b76c2e6b56a9dcb0e8e9e30f0ba465bf953a3e86 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -134,6 +134,8 @@ Section auth.
   Proof. rewrite /auth_auth. apply _. Qed.
   Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
   Proof. rewrite /auth_frag. apply _. Qed.
+  Global Instance auth_both_core_id a1 a2 : CoreId a2 → CoreId (●□ a1 ⋅ ◯ a2).
+  Proof. rewrite /auth_auth /auth_frag. apply _. Qed.
   Global Instance auth_frag_is_op a b1 b2 :
     IsOp a b1 b2 → IsOp' (◯ a) (◯ b1) (◯ b2).
   Proof. rewrite /auth_frag. apply _. Qed.
diff --git a/iris/algebra/lib/mono_list.v b/iris/algebra/lib/mono_list.v
index b91656f250e99ff7dd7be95fa5ad5e4f7711ad2b..9aa8503549ff780be34fb3afae869ed8a4d47b5e 100644
--- a/iris/algebra/lib/mono_list.v
+++ b/iris/algebra/lib/mono_list.v
@@ -50,6 +50,8 @@ Section mono_list_props.
   (** * Operation *)
   Global Instance mono_list_lb_core_id l : CoreId (â—¯ML l).
   Proof. rewrite /mono_list_lb. apply _. Qed.
+  Global Instance mono_list_auth_core_id l : CoreId (●ML□ l).
+  Proof. rewrite /mono_list_auth. apply _. Qed.
 
   Lemma mono_list_auth_dfrac_op dq1 dq2 l :
     ●ML{dq1 ⋅ dq2} l ≡ ●ML{dq1} l ⋅ ●ML{dq2} l.
diff --git a/iris/algebra/lib/mono_nat.v b/iris/algebra/lib/mono_nat.v
index b712ad6e87424d14e6b76cc6dc28d553b9360378..a30056d162e313e723c9a6f4bc5d2e30057255e3 100644
--- a/iris/algebra/lib/mono_nat.v
+++ b/iris/algebra/lib/mono_nat.v
@@ -32,6 +32,8 @@ Section mono_nat.
 
   Global Instance mono_nat_lb_core_id n : CoreId (â—¯MN n).
   Proof. apply _. Qed.
+  Global Instance mono_nat_auth_core_id l : CoreId (●MN□ l).
+  Proof. apply _. Qed.
 
   Lemma mono_nat_auth_dfrac_op dq1 dq2 n :
     ●MN{dq1 ⋅ dq2} n ≡ ●MN{dq1} n ⋅ ●MN{dq2} n.
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index ce5b96b9c9aadf1a302bc517fc42a15a124af0d2..44b97fb7fa382abc919f0d161c51bd976c59d783 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -289,6 +289,8 @@ Section cmra.
   Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.
   Global Instance view_frag_core_id b : CoreId b → CoreId (◯V b).
   Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.
+  Global Instance view_both_core_id a b : CoreId b → CoreId (●V□ a ⋅ ◯V b).
+  Proof. do 2 constructor; simpl; auto. rewrite !left_id. apply: core_id_core. Qed.
   Global Instance view_frag_is_op b b1 b2 :
     IsOp b b1 b2 → IsOp' (◯V b) (◯V b1) (◯V b2).
   Proof. done. Qed.