diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean
index 5d0bc3516d..c1336eb560 100644
--- a/src/Init/Data/Array/Attach.lean
+++ b/src/Init/Data/Array/Attach.lean
@@ -98,7 +98,7 @@ well-founded recursion mechanism to prove that the function terminates.
 
 @[simp] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (xs : Array α) (h : ∀ b ∈ xs.push a, P b) :
     pmap f (xs.push a) h =
-      (pmap f xs (fun a m => by simp at h; exact h.1 _ m)).push (f a (h a (by simp))) := by
+      (pmap f xs (fun a m => by simp [forall_or_eq_imp] at h; exact h.1 _ m)).push (f a (h a (by simp))) := by
   simp [pmap]
 
 @[simp] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
@@ -153,7 +153,7 @@ theorem attachWith_congr {xs ys : Array α} (w : xs = ys) {P : α → Prop} {H :
 
 @[simp] theorem attachWith_push {a : α} {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
     (xs.push a).attachWith P H =
-      (xs.attachWith P (fun x h => by simp at H; exact H.1 _ h)).push ⟨a, H a (by simp)⟩ := by
+      (xs.attachWith P (fun x h => by simp [forall_or_eq_imp] at H; exact H.1 _ h)).push ⟨a, H a (by simp)⟩ := by
   cases xs
   simp
 
diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index aa5f78bc6d..7b3ad59ca1 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -867,7 +867,7 @@ theorem and_le_right {n m : Nat} : n &&& m ≤ m :=
   le_of_testBit (by simp)
 
 theorem left_le_or {n m : Nat} : n ≤ n ||| m :=
-  le_of_testBit (by simp)
+  le_of_testBit (by simp [imp_or_left_iff_true])
 
 theorem right_le_or {n m : Nat} : m ≤ n ||| m :=
-  le_of_testBit (by simp)
+  le_of_testBit (by simp [imp_or_right_iff_true])
diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean
index 0a126d3aa8..ce98f61e8c 100644
--- a/src/Init/Data/Vector/Attach.lean
+++ b/src/Init/Data/Vector/Attach.lean
@@ -100,7 +100,7 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
 
 @[simp] theorem pmap_push {P : α → Prop} {f : ∀ a, P a → β} {a : α} {xs : Vector α n} {h : ∀ b ∈ xs.push a, P b} :
     pmap f (xs.push a) h =
-      (pmap f xs (fun a m => by simp at h; exact h.1 _ m)).push (f a (h a (by simp))) := by
+      (pmap f xs (fun a m => by simp [forall_or_eq_imp] at h; exact h.1 _ m)).push (f a (h a (by simp))) := by
   simp [pmap]
 
 @[simp] theorem attach_empty : (#v[] : Vector α 0).attach = #v[] := rfl
@@ -147,7 +147,7 @@ theorem attachWith_congr {xs ys : Vector α n} (w : xs = ys) {P : α → Prop} {
 
 @[simp] theorem attachWith_push {a : α} {xs : Vector α n} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
     (xs.push a).attachWith P H =
-      (xs.attachWith P (fun x h => by simp at H; exact H.1 _ h)).push ⟨a, H a (by simp)⟩ := by
+      (xs.attachWith P (fun x h => by simp [forall_or_eq_imp] at H; exact H.1 _ h)).push ⟨a, H a (by simp)⟩ := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean
index 83ba4102e1..e2f8ad0a78 100644
--- a/src/Init/PropLemmas.lean
+++ b/src/Init/PropLemmas.lean
@@ -100,10 +100,10 @@ theorem or_rotate : a ∨ b ∨ c ↔ b ∨ c ∨ a := by simp only [or_left_com
 theorem or_iff_left  (hb : ¬b) : a ∨ b ↔ a := or_iff_left_iff_imp.mpr  hb.elim
 theorem or_iff_right (ha : ¬a) : a ∨ b ↔ b := or_iff_right_iff_imp.mpr ha.elim
 
-@[simp] theorem imp_or_left_iff_true {P Q : Prop} : (P → P ∨ Q) ↔ True := by
+theorem imp_or_left_iff_true {P Q : Prop} : (P → P ∨ Q) ↔ True := by
   simpa using Or.inl
 
-@[simp] theorem imp_or_right_iff_true {P Q : Prop} : (Q → P ∨ Q) ↔ True := by
+theorem imp_or_right_iff_true {P Q : Prop} : (Q → P ∨ Q) ↔ True := by
   simpa using Or.inr
 
 /-! ## distributivity -/
@@ -360,15 +360,15 @@ theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x,
     (∀ a, a = a' ∨ Q a → P a) ↔ P a' ∧ ∀ a, Q a → P a := by
   simp only [or_imp, forall_and, forall_eq]
 
-@[simp] theorem forall_eq_or_imp' {P Q : α → Prop} {a' : α} :
+theorem forall_eq_or_imp' {P Q : α → Prop} {a' : α} :
     (∀ (a : α), a' = a ∨ Q a → P a) ↔ P a' ∧ ∀ (a : α), Q a → P a := by
   simp only [or_imp, forall_and, forall_eq']
 
-@[simp] theorem forall_or_eq_imp {P Q : α → Prop} :
+theorem forall_or_eq_imp {P Q : α → Prop} :
     (∀ a, Q a ∨ a = a' → P a) ↔ (∀ a, Q a → P a) ∧ P a' := by
   simp only [or_imp, forall_and, forall_eq]
 
-@[simp] theorem forall_or_eq_imp' {P Q : α → Prop} :
+theorem forall_or_eq_imp' {P Q : α → Prop} :
     (∀ a, Q a ∨ a' = a → P a) ↔ (∀ a, Q a → P a) ∧ P a' := by
   simp only [or_imp, forall_and, forall_eq']
 
@@ -438,22 +438,18 @@ theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) : (∀ h' :
 @[simp] theorem forall_self_imp (P : Prop) (Q : P → Prop) : (∀ p : P, P → Q p) ↔ ∀ p, Q p :=
   ⟨fun h p => h p p, fun h _ p => h p⟩
 
-@[simp]
 theorem forall_or_imp_or_self_right_right {P Q R : α → Prop} :
     (∀ a, P a ∨ Q a → R a ∨ Q a) ↔ (∀ a, P a → R a ∨ Q a) := by
   simp only [or_imp, imp_or_right_iff_true, and_true]
 
-@[simp]
 theorem forall_or_imp_or_self_right_left {P Q R : α → Prop} :
     (∀ a, P a ∨ Q a → Q a ∨ R a) ↔ (∀ a, P a → Q a ∨ R a) := by
   simp only [or_imp, imp_or_left_iff_true, and_true]
 
-@[simp]
 theorem forall_or_imp_or_self_left_right {P Q R : α → Prop} :
     (∀ a, Q a ∨ P a → R a ∨ Q a) ↔ (∀ a, P a → R a ∨ Q a) := by
   simp only [or_imp, imp_or_right_iff_true, true_and]
 
-@[simp]
 theorem forall_or_imp_or_self_left_left {P Q R : α → Prop} :
     (∀ a, Q a ∨ P a → Q a ∨ R a) ↔ (∀ a, P a → Q a ∨ R a) := by
   simp only [or_imp, imp_or_left_iff_true, true_and]