diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean
index 31e2b059d106..6cd3ee60fddc 100644
--- a/src/Lean/Elab/Attributes.lean
+++ b/src/Lean/Elab/Attributes.lean
@@ -59,9 +59,9 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa
     else match attr.getKind with
       | .str _ s => pure <| Name.mkSimple s
       | _ => throwErrorAt attr  "Unknown attribute"
-    let .ok _impl := getAttributeImpl (← getEnv) attrName
-      | throwError "Unknown attribute `[{attrName}]`"
-    if let .ok impl := getAttributeImpl (← getEnv) attrName then
+    match getAttributeImpl (← getEnv) attrName with
+      | .error _ => throwError "Unknown attribute `[{attrName}]`. Note, that attributes are impossible to use in the same file they are declared in: consider extracting the declaration into a separate file."
+      | .ok impl =>
       if regularInitAttr.getParam? (← getEnv) impl.ref |>.isSome then  -- skip `builtin_initialize` attributes
         -- Reject attribute uses where the implementation's module has been loaded for IR only as
         -- this would make it `inServer`-dependent and confused shake as well (#13599).
diff --git a/tests/elab/attributeErrors.lean b/tests/elab/attributeErrors.lean
index aa01f42e17b4..84700b8851ac 100644
--- a/tests/elab/attributeErrors.lean
+++ b/tests/elab/attributeErrors.lean
@@ -6,7 +6,7 @@ Tests errors generated by the core attribute infrastructure. Does *not* test err
 attributes' individual preprocessing (e.g., `[reducible]`).
 -/
 
-/-- error: Unknown attribute `[nonexistent_attribute]` -/
+/-- error: Unknown attribute `[nonexistent_attribute]`. Note, that attributes are impossible to use in the same file they are declared in: consider extracting the declaration into a separate file. -/
 #guard_msgs in
 @[nonexistent_attribute] def x := 32
 
diff --git a/tests/elab_fail/nonfatalattrs.lean.out.expected b/tests/elab_fail/nonfatalattrs.lean.out.expected
index 6cc8d2771c79..87dbff1a1c51 100644
--- a/tests/elab_fail/nonfatalattrs.lean.out.expected
+++ b/tests/elab_fail/nonfatalattrs.lean.out.expected
@@ -1,4 +1,4 @@
-nonfatalattrs.lean:6:2-6:19: error: Unknown attribute `[attrUnimplementedattr]`
+nonfatalattrs.lean:6:2-6:19: error: Unknown attribute `[attrUnimplementedattr]`. Note, that attributes are impossible to use in the same file they are declared in: consider extracting the declaration into a separate file.
 foo : Nat
 nonfatalattrs.lean:11:12-11:17: error: invalid 'class', declaration 'bar.bar' must be inductive datatype, structure, or constant
 bar : Nat