diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index 5c70f94cceb756b468bb359e73c3aff9f751a9b5..0df7d47c3c1c9b0492c4664e07251592edfdc18f 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -727,10 +727,12 @@ Proof. by rewrite /bi_bare and_exist_l. Qed.
 Lemma bare_True_emp : ■ True ⊣⊢ ■ emp.
 Proof. apply (anti_symm _); rewrite /bi_bare; auto. Qed.
 
-Lemma bare_and_l P Q : P ∧ ■ Q ⊣⊢ ■ (P ∧ Q).
-Proof. by rewrite /bi_bare !assoc (comm _ P). Qed.
-Lemma bare_and_r P Q : ■ P ∧ Q ⊣⊢ ■ (P ∧ Q).
+Lemma bare_and_l P Q : ■ P ∧ Q ⊣⊢ ■ (P ∧ Q).
 Proof. by rewrite /bi_bare assoc. Qed.
+Lemma bare_and_r P Q : P ∧ ■ Q ⊣⊢ ■ (P ∧ Q).
+Proof. by rewrite /bi_bare !assoc (comm _ P). Qed.
+Lemma bare_and_lr P Q : ■ P ∧ Q ⊣⊢ P ∧ ■ Q.
+Proof. by rewrite bare_and_l bare_and_r. Qed.
 
 (* Affine propositions *)
 Global Instance Affine_proper : Proper ((≡) ==> iff) (@Affine PROP).
@@ -1073,10 +1075,10 @@ Qed.
 Lemma persistently_and_bare_sep_r P Q : P ∧ □ Q ⊣⊢ P ∗ ⬕ Q.
 Proof. by rewrite !(comm _ P) persistently_and_bare_sep_l. Qed.
 Lemma and_sep_bare_persistently P Q : ⬕ P ∧ ⬕ Q ⊣⊢ ⬕ P ∗ ⬕ Q.
-Proof. by rewrite -persistently_and_bare_sep_l -bare_and bare_and_l. Qed.
+Proof. by rewrite -persistently_and_bare_sep_l -bare_and bare_and_r. Qed.
 
 Lemma bare_persistently_sep_dup P : ⬕ P ⊣⊢ ⬕ P ∗ ⬕ P.
-Proof. by rewrite -persistently_and_bare_sep_l bare_and_l bare_and idemp. Qed.
+Proof. by rewrite -persistently_and_bare_sep_l bare_and_r bare_and idemp. Qed.
 
 (* Conditional bare modality *)
 Global Instance bare_if_ne p : NonExpansive (@bi_bare_if PROP p).
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index c618fb0dacb2582ab0c310c8d6b94dd1eda1741d..7c9b492a5247a8924dddde1ae20437b675ecbade 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -180,7 +180,7 @@ Global Instance into_wand_impl_true_false P Q P' :
   IntoWand true false (P' → Q) P Q.
 Proof.
   rewrite /FromAssumption /IntoWand /= => ? HP. apply wand_intro_r.
-  rewrite -persistently_and_bare_sep_l HP -{2}(affine_bare P') bare_and_l -bare_and_r.
+  rewrite -persistently_and_bare_sep_l HP -{2}(affine_bare P') -bare_and_lr.
   by rewrite bare_persistently_elim impl_elim_l.
 Qed.
 
@@ -288,13 +288,13 @@ Global Instance into_and_and_affine_l P Q Q' :
   Affine P → FromBare Q' Q → IntoAnd false (P ∧ Q) P Q'.
 Proof.
   intros. rewrite /IntoAnd /=.
-  by rewrite -(affine_bare P) bare_and_r bare_and (from_bare Q').
+  by rewrite -(affine_bare P) bare_and_l bare_and (from_bare Q').
 Qed.
 Global Instance into_and_and_affine_r P P' Q :
   Affine Q → FromBare P' P → IntoAnd false (P ∧ Q) P' Q.
 Proof.
   intros. rewrite /IntoAnd /=.
-  by rewrite -(affine_bare Q) bare_and_l bare_and (from_bare P').
+  by rewrite -(affine_bare Q) bare_and_r bare_and (from_bare P').
 Qed.
 
 Global Instance into_and_sep `{PositiveBI PROP} P Q : IntoAnd true (P ∗ Q) P Q.
@@ -333,7 +333,7 @@ Global Instance into_sep_and_persistent_l P P' Q Q' :
   Persistent P → AndIntoSep P P' Q Q' → IntoSep (P ∧ Q) P' Q'.
 Proof.
   destruct 2 as [P Q Q'|P Q]; rewrite /IntoSep.
-  - rewrite -(from_bare Q') -(affine_bare P) bare_and_r -bare_and_l.
+  - rewrite -(from_bare Q') -(affine_bare P) bare_and_lr.
     by rewrite persistent_and_bare_sep_l_1.
   - by rewrite persistent_and_bare_sep_l_1.
 Qed.
@@ -341,7 +341,7 @@ Global Instance into_sep_and_persistent_r P P' Q Q' :
   Persistent Q → AndIntoSep Q Q' P P' → IntoSep (P ∧ Q) P' Q'.
 Proof.
   destruct 2 as [Q P P'|Q P]; rewrite /IntoSep.
-  - rewrite -(from_bare P') -(affine_bare Q) bare_and_l -bare_and_r.
+  - rewrite -(from_bare P') -(affine_bare Q) -bare_and_lr.
     by rewrite persistent_and_bare_sep_r_1.
   - by rewrite persistent_and_bare_sep_r_1.
 Qed.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 2b97e11521134fbf5ffa59711bfccfe8b7a7a846..7f28831a7fd33e70d1f4d867b82683da70b9f6ee 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -339,7 +339,7 @@ Lemma env_spatial_is_nil_bare_persistently Δ :
   env_spatial_is_nil Δ = true → Δ ⊢ ⬕ Δ.
 Proof.
   intros. unfold of_envs; destruct Δ as [? []]; simplify_eq/=.
-  rewrite !right_id {1}bare_and_l persistently_and.
+  rewrite !right_id {1}bare_and_r persistently_and.
   by rewrite persistently_bare persistently_idemp persistently_pure.
 Qed.
 
@@ -556,7 +556,7 @@ Proof.
   intros ??? <-. destruct (env_spatial_is_nil Δ) eqn:?.
   - rewrite (env_spatial_is_nil_bare_persistently Δ) //; simpl. apply impl_intro_l.
     rewrite envs_app_singleton_sound //; simpl.
-    rewrite -(from_bare P') bare_and_l -bare_and_r.
+    rewrite -(from_bare P') -bare_and_lr.
     by rewrite persistently_and_bare_sep_r bare_persistently_elim wand_elim_r.
   - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
     by rewrite -(from_bare P') persistent_and_bare_sep_l_1 wand_elim_r.
@@ -712,7 +712,7 @@ Proof.
     by rewrite sep_elim_r persistently_and_bare_sep_l wand_elim_r.
   - destruct Hpos.
     rewrite -(affine_bare R) (_ : R = â–¡?false R)%I // (into_persistent _ R).
-    rewrite bare_and_r -bare_and_l bare_sep sep_elim_r bare_elim.
+    rewrite bare_and_lr bare_sep sep_elim_r bare_elim.
     by rewrite persistently_and_bare_sep_l wand_elim_r.
 Qed.