From 64cf78017b8a06b3b93a7045db9135923ca8eb34 Mon Sep 17 00:00:00 2001
From: Parcly Taxel <reddeloostw@gmail.com>
Date: Mon, 16 Sep 2024 14:54:16 +0800
Subject: [PATCH] the other one

---
 src/Init/Core.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 3a13d45c44d4..0ff69a30982c 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -817,7 +817,7 @@ variable {a b c d : Prop}
 theorem iff_iff_implies_and_implies {a b : Prop} : (a ↔ b) ↔ (a → b) ∧ (b → a) :=
   Iff.intro (fun h => And.intro h.mp h.mpr) (fun h => Iff.intro h.left h.right)
 
-@[refl] theorem Iff.refl (a : Prop) : a ↔ a :=
+theorem Iff.refl (a : Prop) : a ↔ a :=
   Iff.intro (fun h => h) (fun h => h)
 
 @[refl] protected theorem Iff.rfl {a : Prop} : a ↔ a :=