diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index 8c7706039b..e3c038c53b 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -1674,7 +1674,7 @@ private theorem neg_udiv_eq_intMin_iff_eq_intMin_eq_one_of_msb_eq_true
     obtain ⟨hx, hy⟩ := this
     simp only [beq_iff_eq] at hy
     subst hy
-    simp only [udiv_one, zero_lt_succ, neg_eq_intMin] at h
+    simp only [udiv_one, neg_eq_intMin] at h
     simp [h]
   · rintro ⟨hx, hy⟩
     subst hx hy
@@ -1701,10 +1701,9 @@ theorem msb_sdiv_eq_decide {x y : BitVec w} :
      := by
   rcases w; decide +revert
   case succ w =>
-    simp only [decide_true, ne_eq, decide_and, decide_not, Bool.true_and,
-      sdiv_eq, udiv_eq]
+    simp only [sdiv_eq, udiv_eq]
     rcases hxmsb : x.msb <;> rcases hymsb : y.msb
-    · simp [hxmsb, hymsb, msb_udiv_eq_false_of, Bool.not_false, Bool.and_false, Bool.false_and,
+    · simp [hxmsb, msb_udiv_eq_false_of, Bool.not_false, Bool.and_false, Bool.false_and,
         Bool.and_true, Bool.or_self, Bool.and_self]
     · simp only [hxmsb, hymsb, msb_neg, msb_udiv_eq_false_of, bne_false, Bool.not_false,
         Bool.and_self, ne_zero_of_msb_true, decide_false, Bool.and_true, Bool.true_and, Bool.not_true,
@@ -1716,7 +1715,7 @@ theorem msb_sdiv_eq_decide {x y : BitVec w} :
         obtain ⟨hcontra, _⟩ := this
         simp only [hcontra, true_eq_false] at hxmsb
       simp [this, hymsb, udiv_ne_zero_iff_ne_zero_and_le]
-    · simp only [hxmsb, hymsb, Bool.not_true, Bool.and_self, Bool.false_and, Bool.not_false,
+    · simp only [Bool.not_true, Bool.and_self, Bool.false_and, Bool.not_false,
         Bool.true_and, Bool.false_or, Bool.and_false, Bool.or_false]
       by_cases hx₁ : x = 0#(w + 1)
       · simp [hx₁, neg_zero, zero_udiv, msb_zero, le_zero_iff, Bool.and_not_self]
@@ -1725,12 +1724,12 @@ theorem msb_sdiv_eq_decide {x y : BitVec w} :
         · simp only [hy₁, decide_false, Bool.not_false, Bool.and_true]
           by_cases hxy₁ : (- x / y) = 0#(w + 1)
           · simp only [hxy₁, neg_zero, msb_zero, false_eq_decide_iff, BitVec.not_le,
-              decide_eq_true_eq, BitVec.not_le]
+              BitVec.not_le]
             simp only [udiv_eq_zero_iff_eq_zero_or_lt, hy₁, _root_.false_or] at hxy₁
             bv_omega
           · simp only [udiv_eq_zero_iff_eq_zero_or_lt, _root_.not_or, BitVec.not_lt,
               hy₁, not_false_eq_true, _root_.true_and] at hxy₁
-            simp only [hxy₁, decide_true, msb_neg, bne_iff_ne, ne_eq,
+            simp only [decide_true, msb_neg, bne_iff_ne, ne_eq,
               bool_to_prop,
               bne_iff_ne, ne_eq, udiv_eq_zero_iff_eq_zero_or_lt, hy₁, _root_.false_or,
               BitVec.not_lt, hxy₁, _root_.true_and, decide_not, not_eq_eq_eq_not, not_eq_not,
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 262c9ffaa2..d4ea0e7f77 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1880,14 +1880,14 @@ theorem toInt_shiftLeftZeroExtend {x : BitVec w} :
     (shiftLeftZeroExtend x n).toInt = x.toInt * 2 ^ n := by
   rw [shiftLeftZeroExtend_eq]
   rcases w with _|w
-  · simp [of_length_zero, shiftLeftZeroExtend_eq]
+  · simp [of_length_zero]
   · rcases n with _|n
-    · simp [shiftLeftZeroExtend_eq]
+    · simp
     · have := Nat.pow_pos (a := 2) (n := n + 1) (by omega)
       have : x.toNat <<< (n + 1) < 2 ^ (w + 1 + (n + 1)) := by
         rw [Nat.shiftLeft_eq, Nat.pow_add (a := 2) (m := w + 1) (n := n + 1), Nat.mul_lt_mul_right (by omega)]
         omega
-      simp only [shiftLeftZeroExtend_eq, toInt_shiftLeft, toNat_setWidth, Nat.lt_add_right_iff_pos,
+      simp only [toInt_shiftLeft, toNat_setWidth, Nat.lt_add_right_iff_pos,
         Nat.zero_lt_succ, toNat_mod_cancel_of_lt, Int.bmod_def]
       by_cases hmsb : x.msb
       · have hge := toNat_ge_of_msb_true hmsb
@@ -1902,7 +1902,7 @@ theorem toInt_shiftLeftZeroExtend {x : BitVec w} :
           show ¬2 * x.toNat < 2 ^ (w + 1) by simp [Nat.pow_add, Nat.mul_comm (2 ^ w) 2, hge]]
         norm_cast
         simp [Int.natCast_mul, Int.natCast_pow, Int.cast_ofNat_Int, Int.sub_mul,
-          Int.sub_right_inj, show w + (n + 1) + 1 = (w + 1) + (n + 1) by omega, Nat.pow_add]
+          show w + (n + 1) + 1 = (w + 1) + (n + 1) by omega, Nat.pow_add]
       · simp only [Bool.not_eq_true] at hmsb
         have hle := toNat_lt_of_msb_false (x := x) hmsb
         simp only [Nat.add_one_sub_one] at hle
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
index 20ef760546..6f8421c91c 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
@@ -130,7 +130,7 @@ theorem Iter.forIn'_toList {α β : Type w} [Iterator α Id β]
   rw [forIn'_toList.aux this]
   rw [forIn'_eq_match_step]
   rw [List.forIn'_eq_foldlM] at *
-  simp only [map_eq_pure_bind, List.foldlM_map, hs]
+  simp only [map_eq_pure_bind, hs]
   cases step using PlausibleIterStep.casesOn
   · rename_i it' out h
     simp only [List.attach_cons, List.foldlM_cons, bind_pure_comp, map_bind]
@@ -180,7 +180,7 @@ theorem Iter.forIn_toList {α β : Type w} [Iterator α Id β]
     intro forInStep
     cases forInStep
     · induction it'.toList <;> simp [*]
-    · simp only [ForIn.forIn, forIn', List.forIn'] at ihy
+    · simp only [ForIn.forIn] at ihy
       simp [ihy h, forIn_eq_forIn_toIterM]
   · rename_i it' h
     simp only [bind_pure_comp]
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
index 7f45f163c0..7dd079a14c 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
@@ -63,7 +63,7 @@ theorem IterM.toArray_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
       | .done _ => return #[]) := by
   simp only [IterM.toArray, LawfulIteratorCollect.toArrayMapped_eq]
   rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
-  simp [bind_pure_comp, pure_bind, toArray]
+  simp [bind_pure_comp, pure_bind]
 
 theorem IterM.toList_toArray [Monad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m]
     {it : IterM (α := α) m β} :
diff --git a/src/Init/Data/Sum/Lemmas.lean b/src/Init/Data/Sum/Lemmas.lean
index 3d4da26067..140b67eced 100644
--- a/src/Init/Data/Sum/Lemmas.lean
+++ b/src/Init/Data/Sum/Lemmas.lean
@@ -48,10 +48,10 @@ section get
   | inr _, _ => rfl
 
 @[simp, grind =] theorem getLeft?_eq_none_iff {x : α ⊕ β} : x.getLeft? = none ↔ x.isRight := by
-  cases x <;> simp only [getLeft?, isRight, eq_self_iff_true, reduceCtorEq]
+  cases x <;> simp only [getLeft?, isRight, reduceCtorEq]
 
 @[simp, grind =] theorem getRight?_eq_none_iff {x : α ⊕ β} : x.getRight? = none ↔ x.isLeft := by
-  cases x <;> simp only [getRight?, isLeft, eq_self_iff_true, reduceCtorEq]
+  cases x <;> simp only [getRight?, isLeft, reduceCtorEq]
 
 theorem eq_left_getLeft_of_isLeft : ∀ {x : α ⊕ β} (h : x.isLeft), x = inl (x.getLeft h)
   | inl _, _ => rfl
diff --git a/src/Init/Grind/Ring/Basic.lean b/src/Init/Grind/Ring/Basic.lean
index 2315d2b158..4fa359c7c2 100644
--- a/src/Init/Grind/Ring/Basic.lean
+++ b/src/Init/Grind/Ring/Basic.lean
@@ -531,7 +531,7 @@ theorem no_int_zero_divisors {α : Type u} [IntModule α] [NoNatZeroDivisors α]
     : k ≠ 0 → k * a = 0 → a = 0 := by
   match k with
   | (k : Nat) =>
-    simp [intCast_natCast]
+    simp only [ne_eq, Int.natCast_eq_zero]
     intro h₁ h₂
     replace h₁ : k ≠ 0 := by intro h; simp [h] at h₁
     rw [IntModule.hmul_nat] at h₂
diff --git a/src/Init/GrindInstances/Ring/BitVec.lean b/src/Init/GrindInstances/Ring/BitVec.lean
index 33ec531a02..217b9c2dc8 100644
--- a/src/Init/GrindInstances/Ring/BitVec.lean
+++ b/src/Init/GrindInstances/Ring/BitVec.lean
@@ -32,7 +32,7 @@ instance : CommRing (BitVec w) where
   intCast_neg _ := BitVec.ofInt_neg
 
 instance : IsCharP (BitVec w) (2 ^ w) := IsCharP.mk' _ _
-  (ofNat_eq_zero_iff := fun x => by simp [BitVec.ofInt, BitVec.toNat_eq])
+  (ofNat_eq_zero_iff := fun x => by simp [BitVec.toNat_eq])
 
 -- Verify we can derive the instances showing how `toInt` interacts with operations:
 example : ToInt.Add (BitVec w) (some 0) (some (2^w)) := inferInstance
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Clz.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Clz.lean
index 4280d7d892..0df671fcc5 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Clz.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Clz.lean
@@ -57,8 +57,8 @@ theorem go_denote_eq {w : Nat} (aig : AIG α)
           · simp [hx]
           · simp [Ref.hgate]
         · intro idx hidx
-          simp only [Nat.add_eq_zero, Nat.succ_ne_self, and_false, reduceIte, RefVec.get_cast,
-            Ref.cast_eq, Nat.add_one_sub_one]
+          simp only [Nat.add_eq_zero, Nat.succ_ne_self, and_false, reduceIte, 
+            Nat.add_one_sub_one]
           rw [RefVec.denote_ite]
           split
           · next h =>
diff --git a/src/lake/Lake/Util/Name.lean b/src/lake/Lake/Util/Name.lean
index 337df886f8..433fe51ade 100644
--- a/src/lake/Lake/Util/Name.lean
+++ b/src/lake/Lake/Util/Name.lean
@@ -67,10 +67,10 @@ theorem eq_anonymous_of_isAnonymous {n : Name} : (h : n.isAnonymous) → n = .an
 | .str .., .num .. => by simp [quickCmpAux]
 | .num p₁ n₁, .num p₂ n₂ => by
   simp only [quickCmpAux]; split <;>
-  simp_all [quickCmpAux_iff_eq, show ∀ p, (p → False) ↔ ¬ p from fun _ => .rfl]
+  simp_all [quickCmpAux_iff_eq]
 | .str p₁ s₁, .str p₂ s₂ => by
   simp only [quickCmpAux]; split <;>
-  simp_all [quickCmpAux_iff_eq, show ∀ p, (p → False) ↔ ¬ p from fun _ => .rfl]
+  simp_all [quickCmpAux_iff_eq]
 
 instance : LawfulCmpEq Name quickCmpAux where
   eq_of_cmp := quickCmpAux_iff_eq.mp
diff --git a/src/lake/Lake/Util/Version.lean b/src/lake/Lake/Util/Version.lean
index 22eb4048e6..4235748e65 100644
--- a/src/lake/Lake/Util/Version.lean
+++ b/src/lake/Lake/Util/Version.lean
@@ -126,7 +126,7 @@ def ToolchainVer.ofString (ver : String) : ToolchainVer := Id.run do
   let colonPos := ver.posOf ':'
   let (origin, tag) :=
     if h : colonPos < ver.endPos then
-      let pos := ver.next' colonPos (by simp_all [h, String.endPos, String.atEnd])
+      let pos := ver.next' colonPos (by simp_all [String.endPos, String.atEnd])
       (ver.extract 0 colonPos, ver.extract pos ver.endPos)
     else
       ("", ver)