the other one

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 :=