lint

Author: kim-em

Mathlib/Data/List/Basic.lean

@@ -396,8 +396,8 @@ theorem mem_getLast?_append_of_mem_getLast? {l₁ l₂ : List α} {x : α} (h :
 @[simp]
 theorem head!_nil [Inhabited α] : ([] : List α).head! = default := rfl
 
-@[simp] theorem head_cons_tail (x : List α) (h : x ≠ []) : x.head h :: x.tail = x := by
-  cases x <;> simp at h ⊢
+@[deprecated cons_head_tail (since := "2025-08-15")]
+theorem head_cons_tail (x : List α) (h : x ≠ []) : x.head h :: x.tail = x := by simp
 
 theorem head_eq_getElem_zero {l : List α} (hl : l ≠ []) :
     l.head hl = l[0]'(length_pos_iff.2 hl) :=