diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index 00f829c2f3c4f1a935c3e0269c743036efbf57a3..3166745c3e13cdfeb1a351acbd0f6a049cf40a93 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -130,6 +130,13 @@ Section auth.
   Proof. apply view_frag_mono. Qed.
   Lemma auth_frag_core a : core (â—¯ a) = â—¯ (core a).
   Proof. apply view_frag_core. Qed.
+  Lemma auth_both_core_discarded a b :
+    core (●{DfracDiscarded} a ⋅ ◯ b) ≡ ●{DfracDiscarded} a ⋅ ◯ (core b).
+  Proof. apply view_both_core_discarded. Qed.
+  Lemma auth_both_core_frac q a b :
+    core (●{#q} a ⋅ ◯ b) ≡ ◯ (core b).
+  Proof. apply view_both_core_frac. 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).
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index ce5b96b9c9aadf1a302bc517fc42a15a124af0d2..aa39cebce3343c2038caedbea0024df4f06b7b50 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -209,6 +209,15 @@ Section cmra.
       | Some (dq, ag) => ✓{n} dq ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
       | None => ∃ a, rel n a (view_frag_proj x)
       end := eq_refl _.
+  Local Definition view_pcore_eq :
+      pcore = λ x, Some (View (core (view_auth_proj x)) (core (view_frag_proj x)))
+    := eq_refl _.
+  Local Definition view_core_eq :
+      core = λ x, View (core (view_auth_proj x)) (core (view_frag_proj x))
+    := eq_refl _.
+  Local Definition view_op_eq :
+      op = λ x y, View (view_auth_proj x ⋅ view_auth_proj y) (view_frag_proj x ⋅ view_frag_proj y)
+    := eq_refl _.
 
   Lemma view_cmra_mixin : CmraMixin (view rel).
   Proof.
@@ -285,6 +294,13 @@ 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.
+  Lemma view_both_core_discarded a b :
+    core (●V{DfracDiscarded} a ⋅ ◯V b) ≡ ●V{DfracDiscarded} a ⋅ ◯V (core b).
+  Proof. rewrite view_core_eq view_op_eq /= !left_id //. Qed.
+  Lemma view_both_core_frac q a b :
+    core (●V{#q} a ⋅ ◯V b) ≡ ◯V (core b).
+  Proof. rewrite view_core_eq view_op_eq /= !left_id //. 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).