diff --git a/library/init/logic.lean b/library/init/logic.lean
index 31f14818b2..334aee2423 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -542,6 +542,7 @@ inductive Exists {α : Type u} (p : α → Prop) : Prop
 
 attribute [intro] Exists.intro
 
+@[pattern]
 def exists.intro := @Exists.intro
 
 notation `exists` binders `, ` r:(scoped P, Exists P) := r