diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index d948592e9a48e1c41cac32e6bdc5b869bcb5baae..9858c033cfe68790af779907db849130f86e06ae 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1144,8 +1144,7 @@ Section prod.
     core (a, b) = (core a, core b).
   Proof.
     rewrite /core /core' {1}/pcore /=.
-    rewrite (cmra_pcore_core a). simpl.
-    rewrite (cmra_pcore_core b). done.
+    rewrite (cmra_pcore_core a) /= (cmra_pcore_core b). done.
   Qed.
 
   Global Instance prod_cmra_total : CmraTotal A → CmraTotal B → CmraTotal prodR.