Update src/Init/Data/Subtype.lean

src/Init/Data/Bool.lean

@@ -448,16 +448,18 @@ theorem not_ite_eq_false_eq_true (p : Prop) [h : Decidable p] (b c : Bool) :
   cases h with | _ p => simp [p]
 
 /-
-Added for confluence between `if_true_left` and `ite_false_same` on
-`if b = true then True else b = true`
+It would be nice to have this for confluence between `if_true_left` and `ite_false_same` on
+`if b = true then True else b = true`.
+However the discrimination tree key is just `→`, so this is tried too often.
 -/
-@[simp] theorem eq_false_imp_eq_true : ∀(b:Bool), (b = false → b = true) ↔ (b = true) := by decide
+theorem eq_false_imp_eq_true : ∀(b:Bool), (b = false → b = true) ↔ (b = true) := by decide
 
 /-
-Added for confluence between `if_true_left` and `ite_false_same` on
-`if b = false then True else b = false`
+It would be nice to have this for confluence between `if_true_left` and `ite_false_same` on
+`if b = false then True else b = false`.
+However the discrimination tree key is just `→`, so this is tried too often.
 -/
-@[simp] theorem eq_true_imp_eq_false : ∀(b:Bool), (b = true → b = false) ↔ (b = false) := by decide
+theorem eq_true_imp_eq_false : ∀(b:Bool), (b = true → b = false) ↔ (b = false) := by decide
 
 /-! ### forall -/
 

src/Init/Data/List/Erase.lean

@@ -337,7 +337,7 @@ theorem mem_of_mem_erase {a b : α} {l : List α} (h : a ∈ l.erase b) : a ∈
 
 @[simp] theorem erase_eq_self_iff [LawfulBEq α] {l : List α} : l.erase a = l ↔ a ∉ l := by
   rw [erase_eq_eraseP', eraseP_eq_self_iff]
-  simp
+  simp [forall_mem_ne']
 
 theorem erase_filter [LawfulBEq α] (f : α → Bool) (l : List α) :
     (filter f l).erase a = filter f (l.erase a) := by

src/Init/Data/List/Lemmas.lean

@@ -388,11 +388,9 @@ theorem forall_mem_cons {p : α → Prop} {a : α} {l : List α} :
   ⟨fun H => ⟨H _ (.head ..), fun _ h => H _ (.tail _ h)⟩,
    fun ⟨H₁, H₂⟩ _ => fun | .head .. => H₁ | .tail _ h => H₂ _ h⟩
 
-@[simp]
 theorem forall_mem_ne {a : α} {l : List α} : (∀ a' : α, a' ∈ l → ¬a = a') ↔ a ∉ l :=
   ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩
 
-@[simp]
 theorem forall_mem_ne' {a : α} {l : List α} : (∀ a' : α, a' ∈ l → ¬a' = a) ↔ a ∉ l :=
   ⟨fun h m => h _ m rfl, fun h _ m e => h (e.symm ▸ m)⟩
 

src/Init/PropLemmas.lean

@@ -403,7 +403,7 @@ theorem Decidable.not_imp_symm [Decidable a] (h : ¬a → b) (hb : ¬b) : a :=
 theorem Decidable.not_imp_comm [Decidable a] [Decidable b] : (¬a → b) ↔ (¬b → a) :=
   ⟨not_imp_symm, not_imp_symm⟩
 
-@[simp] theorem Decidable.not_imp_self [Decidable a] : (¬a → a) ↔ a := by
+theorem Decidable.not_imp_self [Decidable a] : (¬a → a) ↔ a := by
   have := @imp_not_self (¬a); rwa [not_not] at this
 
 theorem Decidable.or_iff_not_imp_left [Decidable a] : a ∨ b ↔ (¬a → b) :=

tests/lean/run/1017.lean

@@ -26,7 +26,7 @@ def isFinite : Prop :=
 instance hasNextWF : WellFoundedRelation {s : ρ // isFinite s} where
   rel := λ s1 s2 => hasNext s2.val s1.val
   wf := ⟨λ ⟨s,h⟩ => ⟨⟨s,h⟩, by
-    simp
+    simp only [Subtype.forall]
     cases h; case intro w h =>
     induction w generalizing s
     case zero =>
@@ -40,7 +40,7 @@ instance hasNextWF : WellFoundedRelation {s : ρ // isFinite s} where
       cases h_next; case intro x h_next =>
       simp [lengthBoundedBy, take, h_next] at h
       have := ih s' h
-      exact Acc.intro (⟨s',h'⟩ : {s : ρ // isFinite s}) (by simpa)
+      exact Acc.intro (⟨s',h'⟩ : {s : ρ // isFinite s}) (by simpa only [Subtype.forall])
   ⟩⟩
 
 def mwe [Stream ρ τ] (acc : α) : {l : ρ // isFinite l} → α