refactor(Combinatorics/SimpleGraph/Walk): simplify proof of "support_tail_of_not_nil" (#28967)

The proof of the lemma named "support_tail_of_not_nil" is shortened. Since "support_tail" is not needed anymore, it is removed.
@[deprecated (since := "2025-08-26")] sign is added for the removed "support_tail".
The library references to "support_tail" are replaced with "support_tail_of_not_nil".

To keep [@simp] on "cons_support_tail" and avoid the linter error, the [@simp] of "support_tail_of_not_nil" (previously on "support_tail") is removed. There might be a better way that I am missing, to deal with the linter error.

Co-authored-by: utkuo <utkuokur@gmail.com>

Author: utkuokur

Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

@@ -126,12 +126,13 @@ lemma isHamiltonianCycle_isCycle_and_isHamiltonian_tail :
 lemma isHamiltonianCycle_iff_isCycle_and_support_count_tail_eq_one :
     p.IsHamiltonianCycle ↔ p.IsCycle ∧ ∀ a, (support p).tail.count a = 1 := by
   simp +contextual [isHamiltonianCycle_isCycle_and_isHamiltonian_tail,
-    IsHamiltonian, support_tail, IsCycle.not_nil]
+    IsHamiltonian, support_tail_of_not_nil, IsCycle.not_nil]
 
 /-- A Hamiltonian cycle visits every vertex. -/
 lemma IsHamiltonianCycle.mem_support (hp : p.IsHamiltonianCycle) (b : α) :
     b ∈ p.support :=
-  List.mem_of_mem_tail <| support_tail p hp.1.not_nil ▸ hp.isHamiltonian_tail.mem_support _
+  List.mem_of_mem_tail <|
+    support_tail_of_not_nil p hp.1.not_nil ▸ hp.isHamiltonian_tail.mem_support _
 
 /-- The length of a Hamiltonian cycle is the number of vertices. -/
 lemma IsHamiltonianCycle.length_eq [Fintype α] (hp : p.IsHamiltonianCycle) :
@@ -142,7 +143,8 @@ lemma IsHamiltonianCycle.length_eq [Fintype α] (hp : p.IsHamiltonianCycle) :
 
 lemma IsHamiltonianCycle.count_support_self (hp : p.IsHamiltonianCycle) :
     p.support.count a = 2 := by
-  rw [support_eq_cons, List.count_cons_self, ← support_tail _ hp.1.not_nil, hp.isHamiltonian_tail]
+  rw [support_eq_cons, List.count_cons_self,
+    ← support_tail_of_not_nil _ hp.1.not_nil, hp.isHamiltonian_tail]
 
 lemma IsHamiltonianCycle.support_count_of_ne (hp : p.IsHamiltonianCycle) (h : a ≠ b) :
     p.support.count b = 1 := by

Mathlib/Combinatorics/SimpleGraph/Walk.lean

@@ -1162,16 +1162,11 @@ lemma not_nil_of_tail_not_nil {p : G.Walk v w} (hp : ¬ p.tail.Nil) : ¬ p.Nil :
     (p.copy hu hv).Nil = p.Nil := by
   subst_vars; rfl
 
-@[simp] lemma support_tail (p : G.Walk u u) (hp : ¬ p.Nil) :
+lemma support_tail_of_not_nil (p : G.Walk u v) (hp : ¬ p.Nil) :
     p.tail.support = p.support.tail := by
   rw [← cons_support_tail p hp, List.tail_cons]
 
-lemma support_tail_of_not_nil (p : G.Walk u v) (hnp : ¬p.Nil) :
-    p.tail.support = p.support.tail := by
-  match p with
-  | .nil => simp only [nil_nil, not_true_eq_false] at hnp
-  | .cons h q =>
-    simp only [tail_cons, getVert_cons_succ, support_copy, support_cons, List.tail_cons]
+@[deprecated (since := "2025-08-26")] alias support_tail := support_tail_of_not_nil
 
 /-- Given a set `S` and a walk `w` from `u` to `v` such that `u ∈ S` but `v ∉ S`,
 there exists a dart in the walk whose start is in `S` but whose end is not. -/