diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index 2ae6b815723eb1d7e6fabd1b5ae7d2e4bad17243..b9eac03efa2cb83dc4dc737bf95ef20e10842aee 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -273,6 +273,8 @@ Section lemmas.
     apply _.
   Qed.
 
+  (** The introduction lemma for atomic_update. This should usually not be used
+  directly; use the [iAuIntro] tactic instead. *)
   Lemma aupd_intro P Q α β Eo Ei Φ :
     Absorbing P → Persistent P → Laterable Q →
     (P ∧ Q -∗ atomic_acc Eo Ei α Q β Φ) →