diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index bc52dd8e60fbbe57cda7e6b76b1ba056b18af4cb..5a0aca78953ba0a2f4bd119d64c137f9e3ed6efe 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -132,6 +132,8 @@ Section auth.
   Proof. apply view_frag_mono. Qed.
   Lemma auth_frag_core a : core (â—¯ a) = â—¯ (core a).
   Proof. apply view_frag_core. Qed.
+  Global Instance auth_auth_core_id a : CoreId (●□ a).
+  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_frag_is_op a b1 b2 :
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 672aa04da9e037a6dbfde098b04e06f0d930471b..0d7106419f861bdef9c70221f2a5c44ee09e4ae1 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -287,8 +287,10 @@ Section cmra.
   Proof. intros [c ->]. rewrite view_frag_op. apply cmra_included_l. Qed.
   Lemma view_frag_core b : core (â—¯V b) = â—¯V (core b).
   Proof. done. Qed.
+  Global Instance view_auth_core_id a : CoreId (●V□ a).
+  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. by apply core_id_core. Qed.
+  Proof. do 2 constructor; simpl; auto. 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.