diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index 4cf58ef72a..07e8c7bbbd 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -267,6 +267,6 @@ theorem getLast?_attach {xs : List α} :
     subst h'
     simp at h
   · symm
-    simpa
+    simpa [getLast_eq_iff_getLast_eq_some]
 
 end List
diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index f1986e632a..41f0dcbb58 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -67,7 +67,7 @@ theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.
 
 @[simp] theorem filterMap_head (f : α → Option β) (l : List α) (h) :
     (l.filterMap f).head h = (l.findSome? f).get (by simp_all [Option.isSome_iff_ne_none])  := by
-  simp
+  simp [head_eq_iff_head?_eq_some]
 
 @[simp] theorem filterMap_getLast? (f : α → Option β) (l : List α) : (l.filterMap f).getLast? = l.reverse.findSome? f := by
   rw [getLast?_eq_head?_reverse]
@@ -75,7 +75,7 @@ theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.
 
 @[simp] theorem filterMap_getLast (f : α → Option β) (l : List α) (h) :
     (l.filterMap f).getLast h = (l.reverse.findSome? f).get (by simp_all [Option.isSome_iff_ne_none]) := by
-  simp
+  simp [getLast_eq_iff_getLast_eq_some]
 
 @[simp] theorem map_findSome? (f : α → Option β) (g : β → γ) (l : List α) :
     (l.findSome? f).map g = l.findSome? (Option.map g ∘ f) := by
@@ -246,7 +246,7 @@ theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
 
 @[simp] theorem filter_head (p : α → Bool) (l : List α) (h) :
     (l.filter p).head h = (l.find? p).get (by simp_all [Option.isSome_iff_ne_none]) := by
-  simp
+  simp [head_eq_iff_head?_eq_some]
 
 @[simp] theorem filter_getLast? (p : α → Bool) (l : List α) : (l.filter p).getLast? = l.reverse.find? p := by
   rw [getLast?_eq_head?_reverse]
@@ -254,7 +254,7 @@ theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
 
 @[simp] theorem filter_getLast (p : α → Bool) (l : List α) (h) :
     (l.filter p).getLast h = (l.reverse.find? p).get (by simp_all [Option.isSome_iff_ne_none]) := by
-  simp
+  simp [getLast_eq_iff_getLast_eq_some]
 
 @[simp] theorem find?_filterMap (xs : List α) (f : α → Option β) (p : β → Bool) :
     (xs.filterMap f).find? p = (xs.find? (fun a => (f a).any p)).bind f := by
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 8d680fd4fe..1bceaa89ba 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -917,13 +917,7 @@ theorem head!_of_head? [Inhabited α] : ∀ {l : List α}, head? l = some a →
 theorem head?_eq_head : ∀ {l} h, @head? α l = some (head l h)
   | _::_, _ => rfl
 
-/--
-We simplify `xs.head h = a` to `xs.head? = some a`,
-despite not simplifying `xs.head h` to `(xs.head?).get ⋯`.
-We can often make further progress on the goal after this simplification,
-because the dependency on `h` has been removed.
--/
-@[simp] theorem head_eq_iff_head?_eq_some {xs : List α} (h) : xs.head h = a ↔ xs.head? = some a := by
+theorem head_eq_iff_head?_eq_some {xs : List α} (h) : xs.head h = a ↔ xs.head? = some a := by
   cases xs with
   | nil => simp at h
   | cons x xs => simp
@@ -2326,19 +2320,13 @@ theorem bind_reverse {β} (l : List α) (f : α → List β) : (l.reverse.bind f
     by_cases h' : l = []
     · simp_all
     · simp only [head_eq_iff_head?_eq_some, head?_reverse] at ih
-      simp [ih, h, h', getLast_cons]
+      simp [ih, h, h', getLast_cons, head_eq_iff_head?_eq_some]
 
 theorem getLast_eq_head_reverse {l : List α} (h : l ≠ []) :
     l.getLast h = l.reverse.head (by simp_all) := by
   rw [← head_reverse]
 
-/--
-We simplify `xs.getLast h = a` to `xs.getLast? = some a`,
-despite not simplifying `xs.getLast h` to `(xs.getLast?).get ⋯`.
-We can often make further progress on the goal after this simplification,
-because the dependency on `h` has been removed.
--/
-@[simp] theorem getLast_eq_iff_getLast_eq_some {xs : List α} (h) : xs.getLast h = a ↔ xs.getLast? = some a := by
+theorem getLast_eq_iff_getLast_eq_some {xs : List α} (h) : xs.getLast h = a ↔ xs.getLast? = some a := by
   rw [getLast_eq_head_reverse, head_eq_iff_head?_eq_some]
   simp
 
diff --git a/src/Init/Data/List/Nat/Range.lean b/src/Init/Data/List/Nat/Range.lean
index becacb2741..688eaac29e 100644
--- a/src/Init/Data/List/Nat/Range.lean
+++ b/src/Init/Data/List/Nat/Range.lean
@@ -69,7 +69,7 @@ theorem head?_range' (n : Nat) : (range' s n).head? = if n = 0 then none else so
   induction n <;> simp_all [range'_succ, head?_append]
 
 @[simp] theorem head_range' (n : Nat) (h) : (range' s n).head h = s := by
-  repeat simp_all [head?_range']
+  repeat simp_all [head?_range', head_eq_iff_head?_eq_some]
 
 theorem getLast?_range' (n : Nat) : (range' s n).getLast? = if n = 0 then none else some (s + n - 1) := by
   induction n generalizing s with
@@ -86,7 +86,7 @@ theorem getLast?_range' (n : Nat) : (range' s n).getLast? = if n = 0 then none e
 @[simp] theorem getLast_range' (n : Nat) (h) : (range' s n).getLast h = s + n - 1 := by
   cases n with
   | zero => simp at h
-  | succ n => simp [getLast?_range']
+  | succ n => simp [getLast?_range', getLast_eq_iff_getLast_eq_some]
 
 theorem pairwise_lt_range' s n (step := 1) (pos : 0 < step := by simp) :
     Pairwise (· < ·) (range' s n step) :=
@@ -305,7 +305,7 @@ theorem head?_range (n : Nat) : (range n).head? = if n = 0 then none else some 0
 @[simp] theorem head_range (n : Nat) (h) : (range n).head h = 0 := by
   cases n with
   | zero => simp at h
-  | succ n => simp [head?_range]
+  | succ n => simp [head?_range, head_eq_iff_head?_eq_some]
 
 theorem getLast?_range (n : Nat) : (range n).getLast? = if n = 0 then none else some (n - 1) := by
   induction n with
@@ -317,7 +317,7 @@ theorem getLast?_range (n : Nat) : (range n).getLast? = if n = 0 then none else
 @[simp] theorem getLast_range (n : Nat) (h) : (range n).getLast h = n - 1 := by
   cases n with
   | zero => simp at h
-  | succ n => simp [getLast?_range]
+  | succ n => simp [getLast?_range, getLast_eq_iff_getLast_eq_some]
 
 theorem take_range (m n : Nat) : take m (range n) = range (min m n) := by
   apply List.ext_getElem
diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean
index 2cb7274716..479d22ed63 100644
--- a/src/Init/Data/List/Nat/TakeDrop.lean
+++ b/src/Init/Data/List/Nat/TakeDrop.lean
@@ -275,7 +275,7 @@ theorem head?_drop (l : List α) (n : Nat) :
 theorem head_drop {l : List α} {n : Nat} (h : l.drop n ≠ []) :
     (l.drop n).head h = l[n]'(by simp_all) := by
   have w : n < l.length := length_lt_of_drop_ne_nil h
-  simpa [getElem?_eq_getElem, h, w] using head?_drop l n
+  simpa [getElem?_eq_getElem, h, w, head_eq_iff_head?_eq_some] using head?_drop l n
 
 theorem getLast?_drop {l : List α} : (l.drop n).getLast? = if l.length ≤ n then none else l.getLast? := by
   rw [getLast?_eq_getElem?, getElem?_drop]