diff --git a/library/init/setoid.lean b/library/init/setoid.lean
index dc138dc779..3a7a00dabd 100644
--- a/library/init/setoid.lean
+++ b/library/init/setoid.lean
@@ -17,12 +17,12 @@ namespace setoid
   variable [s : setoid A]
   include s
 
-  theorem refl (a : A) : a ≈ a :=
+  theorem refl [refl] (a : A) : a ≈ a :=
   and.elim_left (@setoid.iseqv A s) a
 
-  theorem symm {a b : A} : a ≈ b → b ≈ a :=
+  theorem symm [symm] {a b : A} : a ≈ b → b ≈ a :=
   λ H, and.elim_left (and.elim_right (@setoid.iseqv A s)) a b H
 
-  theorem trans {a b c : A} : a ≈ b → b ≈ c → a ≈ c :=
+  theorem trans [trans] {a b c : A} : a ≈ b → b ≈ c → a ≈ c :=
   λ H₁ H₂, and.elim_right (and.elim_right (@setoid.iseqv A s)) a b c H₁ H₂
 end setoid