diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index e9e8779135..b4f78e6b80 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -284,7 +284,7 @@ theorem iff_iff_implies_and_implies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (
 theorem Iff.refl (a : Prop) : a ↔ a :=
   Iff.intro (fun h => h) (fun h => h)
 
-theorem Iff.rfl {a : Prop} : a ↔ a :=
+protected theorem Iff.rfl {a : Prop} : a ↔ a :=
   Iff.refl a
 
 theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index c26993f12f..383e5c6e07 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -107,7 +107,7 @@ init_quot
 inductive HEq {α : Sort u} (a : α) : {β : Sort u} → β → Prop where
   | refl {} : HEq a a
 
-@[matchPattern] def HEq.rfl {α : Sort u} {a : α} : HEq a a :=
+@[matchPattern] protected def HEq.rfl {α : Sort u} {a : α} : HEq a a :=
   HEq.refl a
 
 theorem eq_of_heq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=