diff --git a/src/Init/Data/List/Erase.lean b/src/Init/Data/List/Erase.lean
index 59da134963..9b1b532540 100644
--- a/src/Init/Data/List/Erase.lean
+++ b/src/Init/Data/List/Erase.lean
@@ -230,6 +230,12 @@ theorem eraseP_comm {l : List α} (h : ∀ a ∈ l, ¬ p a ∨ ¬ q a) :
       · simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))]
       · simp [h₁, h₂, ih (fun b m => h b (mem_cons_of_mem _ m))]
 
+theorem head_eraseP_mem (xs : List α) (p : α → Bool) (h) : (xs.eraseP p).head h ∈ xs :=
+  (eraseP_sublist xs).head_mem h
+
+theorem getLast_eraseP_mem (xs : List α) (p : α → Bool) (h) : (xs.eraseP p).getLast h ∈ xs :=
+  (eraseP_sublist xs).getLast_mem h
+
 /-! ### erase -/
 section erase
 variable [BEq α]
@@ -388,6 +394,12 @@ theorem Nodup.not_mem_erase [LawfulBEq α] {a : α} (h : Nodup l) : a ∉ l.eras
 theorem Nodup.erase [LawfulBEq α] (a : α) : Nodup l → Nodup (l.erase a) :=
   Nodup.sublist <| erase_sublist _ _
 
+theorem head_erase_mem (xs : List α) (a : α) (h) : (xs.erase a).head h ∈ xs :=
+  (erase_sublist a xs).head_mem h
+
+theorem getLast_erase_mem (xs : List α) (a : α) (h) : (xs.erase a).getLast h ∈ xs :=
+  (erase_sublist a xs).getLast_mem h
+
 end erase
 
 /-! ### eraseIdx -/
diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean
index 6d7b420ac0..ccc0898a4b 100644
--- a/src/Init/Data/List/Sublist.lean
+++ b/src/Init/Data/List/Sublist.lean
@@ -185,6 +185,12 @@ theorem Sublist.subset : l₁ <+ l₂ → l₁ ⊆ l₂
 protected theorem Sublist.mem (hx : a ∈ l₁) (hl : l₁ <+ l₂) : a ∈ l₂ :=
   hl.subset hx
 
+theorem Sublist.head_mem (s : ys <+ xs) (h) : ys.head h ∈ xs :=
+  s.mem (List.head_mem h)
+
+theorem Sublist.getLast_mem (s : ys <+ xs) (h) : ys.getLast h ∈ xs :=
+  s.mem (List.getLast_mem h)
+
 instance : Trans (@Sublist α) Subset Subset :=
   ⟨fun h₁ h₂ => trans h₁.subset h₂⟩
 
@@ -246,6 +252,12 @@ protected theorem Sublist.filterMap (f : α → Option β) (s : l₁ <+ l₂) :
 protected theorem Sublist.filter (p : α → Bool) {l₁ l₂} (s : l₁ <+ l₂) : filter p l₁ <+ filter p l₂ := by
   rw [← filterMap_eq_filter]; apply s.filterMap
 
+theorem head_filter_mem (xs : List α) (p : α → Bool) (h) : (xs.filter p).head h ∈ xs :=
+  (filter_sublist xs).head_mem h
+
+theorem getLast_filter_mem (xs : List α) (p : α → Bool) (h) : (xs.filter p).getLast h ∈ xs :=
+  (filter_sublist xs).getLast_mem h
+
 theorem sublist_filterMap_iff {l₁ : List β} {f : α → Option β} :
     l₁ <+ l₂.filterMap f ↔ ∃ l', l' <+ l₂ ∧ l₁ = l'.filterMap f := by
   induction l₂ generalizing l₁ with