remove simp on set_coe_eq_subtype (#682)

leanprover-community · Feb 4, 2019 · 5395232 · 5395232
1 parent 5e5f1e2
commit 5395232
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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