diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
index f86f518b06cdd..699d126ab1ea8 100644
--- a/src/data/set/basic.lean
+++ b/src/data/set/basic.lean
@@ -15,7 +15,7 @@ end set
 section set_coe
 universe u
 variables {α : Type u}
-@[simp] theorem set.set_coe_eq_subtype (s : set α) :
+theorem set.set_coe_eq_subtype (s : set α) :
   coe_sort.{(u+1) (u+2)} s = {x // x ∈ s} := rfl
 
 @[simp] theorem set_coe.forall {s : set α} {p : s → Prop} :
diff --git a/src/group_theory/sylow.lean b/src/group_theory/sylow.lean
index dddf8f5ed6c74..2c3a18dc2ba1b 100644
--- a/src/group_theory/sylow.lean
+++ b/src/group_theory/sylow.lean
@@ -181,7 +181,7 @@ local attribute [instance] set_fintype
 
 lemma exists_subgroup_card_pow_prime [fintype G] {p : ℕ} : ∀ {n : ℕ} (hp : nat.prime p)
   (hdvd : p ^ n ∣ card G), ∃ H : set G, is_subgroup H ∧ fintype.card H = p ^ n
-| 0 := λ _ _, ⟨trivial G, by apply_instance, by simp [-set.set_coe_eq_subtype]⟩
+| 0 := λ _ _, ⟨trivial G, by apply_instance, by simp⟩
 | (n+1) := λ hp hdvd,
 let ⟨H, ⟨hH1, hH2⟩⟩ := exists_subgroup_card_pow_prime hp
   (dvd.trans (nat.pow_dvd_pow _ (nat.le_succ _)) hdvd) in
diff --git a/src/tactic/subtype_instance.lean b/src/tactic/subtype_instance.lean
index c8010dfc1c9d8..c2d4cf24e8a98 100644
--- a/src/tactic/subtype_instance.lean
+++ b/src/tactic/subtype_instance.lean
@@ -28,7 +28,7 @@ do
   field ← get_current_field,
   b ← target >>= is_prop,
   if b then  do
-    `[simp [subtype.ext], dsimp],
+    `[simp [subtype.ext], dsimp [set.set_coe_eq_subtype]],
     intros,
     applyc field; assumption
   else do