diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 790e5e51dbb1a16ac4b894214b977a7ec6f0716d..c8e996fa20a3b9a7fd56d1a6ba3f0dc217010379 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -78,7 +78,7 @@ Section inv.
     rewrite assoc_L -!union_difference_L //; set_solver.
   Qed.
 
-  Lemma own_inv_to_inv M P: own_inv M P  -∗ inv M P.
+  Lemma own_inv_to_inv M P: own_inv M P -∗ inv M P.
   Proof.
     iIntros "#I". rewrite inv_eq. iIntros (E H).
     iPoseProof (own_inv_acc with "I") as "H"; eauto.