diff --git a/iris/algebra/dyn_reservation_map.v b/iris/algebra/dyn_reservation_map.v
index fd59b3a80f9d7e0300c553bc2d65ced54efd8c1b..b31404a902dd293b2b16ac91206e33f85624fedd 100644
--- a/iris/algebra/dyn_reservation_map.v
+++ b/iris/algebra/dyn_reservation_map.v
@@ -243,7 +243,7 @@ Section cmra.
 
   Lemma dyn_reservation_map_data_mono k a b :
     a ≼ b → dyn_reservation_map_data k a ≼ dyn_reservation_map_data k b.
-  Proof. intros [c ->]. rewrite dyn_reservation_map_data_op. eauto. Qed.
+  Proof. intros [c ->]. by rewrite dyn_reservation_map_data_op. Qed.
   Global Instance dyn_reservation_map_data_is_op k a b1 b2 :
     IsOp a b1 b2 →
     IsOp' (dyn_reservation_map_data k a) (dyn_reservation_map_data k b1) (dyn_reservation_map_data k b2).
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 4715bdc62f79a0f46bad6b498e933174209f7161..58ce801bb6489895dcddc960a612b97d5a5e2d7d 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -346,7 +346,7 @@ Lemma singleton_included_l m i x :
 Proof.
   split.
   - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
-    exists (x â‹…? m' !! i). rewrite -Some_op_opM. eauto.
+    exists (x â‹…? m' !! i). by rewrite -Some_op_opM.
   - intros (y&Hi&[mz Hy]). exists (partial_alter (λ _, mz) i m).
     intros j; destruct (decide (i = j)) as [->|].
     + by rewrite lookup_op lookup_singleton lookup_partial_alter Hi.
diff --git a/iris/algebra/reservation_map.v b/iris/algebra/reservation_map.v
index ea300bbf5adb17d9075f2627bc9ad05b19343616..1be3502ffcdd9a2fc0cbced105b95c6a13609ea5 100644
--- a/iris/algebra/reservation_map.v
+++ b/iris/algebra/reservation_map.v
@@ -225,7 +225,7 @@ Section cmra.
   Qed.
   Lemma reservation_map_data_mono k a b :
     a ≼ b → reservation_map_data k a ≼ reservation_map_data k b.
-  Proof. intros [c ->]. rewrite reservation_map_data_op. eauto. Qed.
+  Proof. intros [c ->]. by rewrite reservation_map_data_op. Qed.
   Global Instance reservation_map_data_is_op k a b1 b2 :
     IsOp a b1 b2 →
     IsOp' (reservation_map_data k a) (reservation_map_data k b1) (reservation_map_data k b2).
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 5add4f59d560053bd2034300086edc42af8d3eb9..5392eb6f05d2d9728d16f8c146dbcebd8bdb4e5b 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -288,7 +288,7 @@ Section cmra.
   Lemma view_frag_op b1 b2 : â—¯V (b1 â‹… b2) = â—¯V b1 â‹… â—¯V b2.
   Proof. done. Qed.
   Lemma view_frag_mono b1 b2 : b1 ≼ b2 → ◯V b1 ≼ ◯V b2.
-  Proof. intros [c ->]. rewrite view_frag_op. eauto. Qed.
+  Proof. intros [c ->]. by rewrite view_frag_op. Qed.
   Lemma view_frag_core b : core (â—¯V b) = â—¯V (core b).
   Proof. done. Qed.
   Lemma view_both_core_discarded a b :
@@ -424,8 +424,8 @@ Section cmra.
       + apply equiv_dist=> n.
         by eapply view_auth_dfrac_includedN, cmra_included_includedN.
     - intros [[[dq ->]| ->] ->].
-      + rewrite view_auth_dfrac_op -assoc. eauto.
-      + eauto.
+      + by rewrite view_auth_dfrac_op -assoc.
+      + done.
   Qed.
   Lemma view_auth_includedN n a1 a2 b :
     ●V a1 ≼{n} ●V a2 ⋅ ◯V b ↔ a1 ≡{n}≡ a2.
@@ -448,7 +448,7 @@ Section cmra.
     split.
     - intros [xf [_ Hb]]; simpl in *.
       revert Hb; rewrite left_id. by exists (view_frag_proj xf).
-    - intros [bf ->]. rewrite comm view_frag_op -assoc. eauto.
+    - intros [bf ->]. by rewrite comm view_frag_op -assoc.
   Qed.
 
   (** The weaker [view_both_included] lemmas below are a consequence of the