feat(Combinatorics/SimpleGraph/Walk): make p.Nil the simpNF of p = nil and p.length = 0 (#39218)

These are equivalent, and `p.Nil` works even when the endpoints of the walk aren't defeq.

[#graph theory > Deprecate `p = nil` in favor of `p.Nil`?](https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/Deprecate.20.60p.20.3D.20nil.60.20in.20favor.20of.20.60p.2ENil.60.3F/with/538017334)

The main event is `Walk/Basic.lean`:
- Swapped sides of `nil_iff_eq_nil` to create `eq_nil_iff_nil`, tagged `@[simp]` and deprecated the original
- Changed the RHS of `length_eq_zero_iff` from `p = nil` to `p.Nil`, and generalized to non-closed walks
- Deprecated `nil_iff_length_eq` which is the symmetric iff
- Added `Nil.length_eq_zero` alias
- Untagged `exists_length_eq_zero_iff` with `@[simp]` and added `exists_nil_iff` to replace it

The rest is fixing everything that broke (or uses of now-deprecated lemmas), and:
- [`Walk/Maps`] Added `nil_map_iff` to replace `map_eq_nil_iff` which is the same but with `.Nil` instead of `= nil`
- [`Walk/Decomp`] Added `nil_rotate` to replace `rotate_eq_nil` which is the same but with `.Nil` instead of `= nil`

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

@@ -160,8 +160,8 @@ theorem IsTree.coe_singletonSubgraph (G : SimpleGraph V) (v : V) :
 
 theorem IsTree.coe_subgraphOfAdj {u v : V} (h : G.Adj u v) : G.subgraphOfAdj h |>.coe.IsTree := by
   refine ⟨Subgraph.subgraphOfAdj_connected h, fun w p hp ↦ ?_⟩
-  have : _ = _ := p.adj_snd <| nil_iff_eq_nil.not.mpr hp.ne_nil
-  have : _ = _ := p.adj_penultimate <| nil_iff_eq_nil.not.mpr hp.ne_nil
+  have : _ = _ := p.adj_snd hp.not_nil
+  have : _ = _ := p.adj_penultimate hp.not_nil
   #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
   (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
   It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
@@ -301,7 +301,7 @@ theorem IsAcyclic.isPath_iff_isChain (hG : G.IsAcyclic) {v w : V} (p : G.Walk v
     have hcc := List.isChain_cons.mp (edges_cons _ _ ▸ h)
     refine cons_isPath_iff head tail |>.mpr ⟨ih hcc.2, ?_⟩
     rcases tail.length.eq_zero_or_pos with h' | h'
-    · simp [nil_iff_support_eq.mp (nil_iff_length_eq.mpr h'), head.ne]
+    · simp [nil_iff_support_eq.mp (length_eq_zero_iff.mp h'), head.ne]
     · by_contra hh
       apply hG <| cons head (tail.takeUntil u' hh)
       simp only [isCycle_def, isTrail_def, edges_cons, List.nodup_cons, ne_eq, reduceCtorEq,

Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean

@@ -98,7 +98,7 @@ lemma IsEdgeReachable.le_degree [Fintype (G.neighborSet u)] (h : G.IsEdgeReachab
   by_contra! hh
   obtain ⟨w, _⟩ :=
     @h (G.incidenceSet u) (by simpa [← Set.coe_fintypeCard, ENat.coe_lt_coe]) |>.exists_isPath
-  simpa using w.adj_snd <| by grind [Walk.nil_iff_length_eq, Walk.eq_of_length_eq_zero]
+  simpa using w.adj_snd <| mt Walk.Nil.eq huv
 
 lemma IsEdgeConnected.le_degree [Fintype (G.neighborSet u)] [Nontrivial V]
     (h : G.IsEdgeConnected k) : k ≤ G.degree u := by

Mathlib/Combinatorics/SimpleGraph/Metric.lean

@@ -73,9 +73,8 @@ theorem edist_le (p : G.Walk u v) :
 protected alias Walk.edist_le := edist_le
 
 @[simp]
-theorem edist_eq_zero_iff :
-    G.edist u v = 0 ↔ u = v := by
-  apply Iff.intro <;> simp [edist, ENat.iInf_eq_zero]
+theorem edist_eq_zero_iff : G.edist u v = 0 ↔ u = v := by
+  simp [edist]
 
 @[simp]
 theorem edist_self : edist G v v = 0 :=
@@ -380,7 +379,7 @@ of length at least two: the first and third nodes are different and not connecte
 lemma Walk.exists_adj_adj_not_adj_ne {p : G.Walk v w} (hp : p.length = G.dist v w)
     (hl : 1 < G.dist v w) : ∃ (x a b : V), G.Adj x a ∧ G.Adj a b ∧ ¬ G.Adj x b ∧ x ≠ b := by
   use v, p.getVert 1, p.getVert 2
-  have hnp : ¬p.Nil := by simpa [nil_iff_length_eq, hp] using Nat.ne_zero_of_lt hl
+  have hnp : ¬p.Nil := by grind [Nil.length_eq_zero]
   have : p.tail.tail.length < p.tail.length := by
     rw [← p.tail.length_tail_add_one (by
       simp only [not_nil_iff_lt_length, ← p.length_tail_add_one hnp] at hp ⊢

Mathlib/Combinatorics/SimpleGraph/Paths.lean

@@ -415,9 +415,9 @@ lemma IsPath.getVert_eq_start_iff_of_not_nil {i : ℕ} {p : G.Walk u w} (hp : p.
 
 lemma IsPath.getVert_eq_start_iff {i : ℕ} {p : G.Walk u w} (hp : p.IsPath) (hi : i ≤ p.length) :
     p.getVert i = u ↔ i = 0 := by
-  by_cases h' : p.Nil
-  · simp_all [nil_iff_length_eq.mp h']
-  · exact hp.getVert_eq_start_iff_of_not_nil h'
+  cases p
+  · simpa using hi
+  · exact hp.getVert_eq_start_iff_of_not_nil not_nil_cons
 
 lemma IsPath.getVert_eq_end_iff {i : ℕ} {p : G.Walk u w} (hp : p.IsPath) (hi : i ≤ p.length) :
     p.getVert i = w ↔ i = p.length := by
@@ -854,8 +854,8 @@ alias ⟨_, map_isTrail_of_injective⟩ := map_isTrail_iff_of_injective
 
 theorem map_isCycle_iff_of_injective {p : G.Walk u u} (hinj : Function.Injective f) :
     (p.map f).IsCycle ↔ p.IsCycle := by
-  rw [isCycle_def, isCycle_def, map_isTrail_iff_of_injective hinj, Ne, map_eq_nil_iff,
-    support_map, ← List.map_tail, List.nodup_map_iff hinj]
+  rw [isCycle_def, isCycle_def, map_isTrail_iff_of_injective hinj, ne_eq, ne_eq, eq_nil_iff_nil,
+    eq_nil_iff_nil, nil_map_iff, support_map, ← List.map_tail, List.nodup_map_iff hinj]
 
 alias ⟨_, IsCycle.map⟩ := map_isCycle_iff_of_injective
 

Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean

@@ -101,17 +101,13 @@ theorem eq_of_length_eq_zero {u v : V} : ∀ {p : G.Walk u v}, p.length = 0 →
 theorem adj_of_length_eq_one {u v : V} : ∀ {p : G.Walk u v}, p.length = 1 → G.Adj u v
   | cons h nil, _ => h
 
-@[simp]
 theorem exists_length_eq_zero_iff {u v : V} : (∃ p : G.Walk u v, p.length = 0) ↔ u = v :=
   ⟨fun ⟨_, h⟩ ↦ (eq_of_length_eq_zero h), (· ▸ ⟨nil, rfl⟩)⟩
 
 @[simp]
 lemma exists_length_eq_one_iff {u v : V} : (∃ (p : G.Walk u v), p.length = 1) ↔ G.Adj u v :=
   ⟨fun ⟨_, hp⟩ ↦ adj_of_length_eq_one hp, (⟨·.toWalk, by simp⟩)⟩
 
-@[simp]
-theorem length_eq_zero_iff {u : V} {p : G.Walk u u} : p.length = 0 ↔ p = nil := by cases p <;> simp
-
 /-- The `support` of a walk is the list of vertices it visits in order. -/
 def support {u v : V} : G.Walk u v → List V
   | nil => [u]
@@ -367,9 +363,16 @@ lemma darts_eq_nil {p : G.Walk v w} : p.darts = [] ↔ p.Nil := by
 lemma edges_eq_nil {p : G.Walk v w} : p.edges = [] ↔ p.Nil := by
   cases p <;> simp
 
-lemma nil_iff_length_eq {p : G.Walk v w} : p.Nil ↔ p.length = 0 := by
+@[simp]
+theorem length_eq_zero_iff {p : G.Walk u v} : p.length = 0 ↔ p.Nil := by
   cases p <;> simp
 
+alias ⟨_, Nil.length_eq_zero⟩ := length_eq_zero_iff
+
+@[deprecated length_eq_zero_iff (since := "2026-05-11")]
+lemma nil_iff_length_eq {p : G.Walk v w} : p.Nil ↔ p.length = 0 :=
+  length_eq_zero_iff.symm
+
 lemma not_nil_iff_lt_length {p : G.Walk v w} : ¬ p.Nil ↔ 0 < p.length := by
   cases p <;> simp
 
@@ -378,16 +381,25 @@ lemma not_nil_iff {p : G.Walk v w} :
   cases p <;> simp [*]
 
 /-- A walk with its endpoints defeq is `Nil` if and only if it is equal to `nil`. -/
-lemma nil_iff_eq_nil : ∀ {p : G.Walk v v}, p.Nil ↔ p = nil
-  | .nil | .cons _ _ => by simp
+@[simp]
+theorem eq_nil_iff_nil {p : G.Walk v v} : p = nil ↔ p.Nil := by
+  cases p <;> simp
+
+alias ⟨_, Nil.eq_nil⟩ := eq_nil_iff_nil
 
-alias ⟨Nil.eq_nil, _⟩ := nil_iff_eq_nil
+@[deprecated eq_nil_iff_nil (since := "2026-05-11")]
+lemma nil_iff_eq_nil : ∀ {p : G.Walk v v}, p.Nil ↔ p = nil :=
+  eq_nil_iff_nil.symm
 
 lemma nil_of_subsingleton [Subsingleton V] (p : G.Walk v w) : p.Nil :=
   match p with
   | nil => Nil.nil
   | cons h w => Unique.eq_default G ▸ h |>.elim
 
+@[simp]
+theorem exists_nil_iff {u v : V} : (∃ p : G.Walk u v, p.Nil) ↔ u = v :=
+  ⟨fun ⟨_, h⟩ ↦ h.eq, (· ▸ ⟨nil, .nil⟩)⟩
+
 /-- The recursion principle for nonempty walks -/
 @[elab_as_elim]
 def notNilRec {motive : {u w : V} → (p : G.Walk u w) → (h : ¬ p.Nil) → Sort*}

Mathlib/Combinatorics/SimpleGraph/Walk/Counting.lean

@@ -32,25 +32,28 @@ namespace SimpleGraph
 
 variable {V : Type u} (G : SimpleGraph V)
 
-theorem set_walk_self_length_zero_eq (u : V) : {p : G.Walk u u | p.length = 0} = {Walk.nil} := by
-  simp
+theorem Walk.setOf_length_eq_zero (u : V) : {p : G.Walk u u | p.length = 0} = {.nil} := by
+  simp [Walk.length_eq_zero_iff, ← Walk.eq_nil_iff_nil]
 
-theorem set_walk_length_zero_eq_of_ne {u v : V} (h : u ≠ v) :
-    {p : G.Walk u v | p.length = 0} = ∅ := by
-  ext p
-  simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false]
-  exact fun h' => absurd (Walk.eq_of_length_eq_zero h') h
+@[deprecated (since := "2026-05-12")]
+alias set_walk_self_length_zero_eq := Walk.setOf_length_eq_zero
+
+theorem Walk.setOf_length_eq_zero_of_ne {u v : V} (h : u ≠ v) :
+    {p : G.Walk u v | p.length = 0} = ∅ :=
+  Set.eq_empty_of_forall_notMem (h <| ·.eq_of_length_eq_zero ·)
+
+@[deprecated (since := "2026-05-12")]
+alias set_walk_length_zero_eq_of_ne := Walk.setOf_length_eq_zero_of_ne
 
-theorem set_walk_length_succ_eq (u v : V) (n : ℕ) :
-    {p : G.Walk u v | p.length = n.succ} =
+theorem Walk.setOf_length_eq_add_one (u v : V) (n : ℕ) :
+    {p : G.Walk u v | p.length = n + 1} =
       ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' : G.Walk w v | p'.length = n} := by
   ext p
   cases p with
   | nil => simp [eq_comm]
-  | cons huw pwv =>
-    simp only [Nat.succ_eq_add_one, Set.mem_setOf_eq, Walk.length_cons, add_left_inj,
-      Set.mem_iUnion, Set.mem_image]
-    grind
+  | cons huw pwv => grind [length_cons, Set.mem_iUnion]
+
+@[deprecated (since := "2026-05-12")] alias set_walk_length_succ_eq := Walk.setOf_length_eq_add_one
 
 /-- Walks of length two from `u` to `v` correspond bijectively to common neighbours of `u` and `v`.
 Note that `u` and `v` may be the same. -/
@@ -86,10 +89,9 @@ def finsetWalkLength (n : ℕ) (u v : V) : Finset (G.Walk u v) :=
 theorem coe_finsetWalkLength_eq (n : ℕ) (u v : V) :
     (G.finsetWalkLength n u v : Set (G.Walk u v)) = {p : G.Walk u v | p.length = n} := by
   induction n generalizing u v with
-  | zero =>
-    obtain rfl | huv := eq_or_ne u v <;> simp [finsetWalkLength, set_walk_length_zero_eq_of_ne, *]
+  | zero => grind [finsetWalkLength, Walk.length_eq_zero_iff, Walk.eq_nil_iff_nil, Walk.Nil.eq]
   | succ n ih =>
-    simp only [finsetWalkLength, set_walk_length_succ_eq, Finset.coe_biUnion, Finset.mem_coe,
+    simp only [finsetWalkLength, Walk.setOf_length_eq_add_one, Finset.coe_biUnion, Finset.mem_coe,
       Finset.mem_univ, Set.iUnion_true, Finset.coe_map, Set.iUnion_coe_set]
     congr!
     grind

Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean

@@ -239,9 +239,9 @@ lemma getVert_takeUntil {u v : V} {n : ℕ} {p : G.Walk u v} (hw : w ∈ p.suppo
 lemma snd_takeUntil (hsu : w ≠ u) (p : G.Walk u v) (h : w ∈ p.support) :
     (p.takeUntil w h).snd = p.snd := by
   apply p.getVert_takeUntil h
-  by_contra! hc
-  simp only [Nat.lt_one_iff, ← nil_iff_length_eq, nil_takeUntil] at hc
-  exact hsu hc.symm
+  contrapose hsu
+  symm
+  simpa [length_eq_zero_iff] using hsu
 
 lemma getVert_length_takeUntil {p : G.Walk v w} (h : u ∈ p.support) :
     p.getVert (p.takeUntil _ h).length = u := by
@@ -313,9 +313,13 @@ theorem rotate_edges (c : G.Walk v v) (u : V) (h) : (c.rotate u h).edges ~r c.ed
 @[simp] lemma length_rotate (c : G.Walk v v) (u : V) (h) : (c.rotate u h).length = c.length := by
   simpa using (rotate_edges c u h).perm.length_eq
 
-@[simp] lemma rotate_eq_nil {c : G.Walk v v} {u : V} (h) : c.rotate u h = nil ↔ c = nil := by
+@[simp]
+theorem nil_rotate {c : G.Walk v v} (h) : (c.rotate u h).Nil ↔ c.Nil := by
   simp [← length_eq_zero_iff]
 
+@[deprecated nil_rotate (since := "2026-05-11")]
+lemma rotate_eq_nil {c : G.Walk v v} (h) : c.rotate u h = nil ↔ c = nil := by simp
+
 end WalkDecomp
 
 /-- Given a walk `p` and a node in the support, there exists a natural `n`, such that given node

Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean

@@ -75,7 +75,12 @@ theorem map_eq_of_eq {f : G →g G'} (f' : G →g G') (h : f = f') :
   subst_vars
   rfl
 
+variable {p} in
 @[simp]
+theorem nil_map_iff : (p.map f).Nil ↔ p.Nil := by
+  cases p <;> simp
+
+@[deprecated nil_map_iff (since := "2026-05-12")]
 theorem map_eq_nil_iff {p : G.Walk u u} : p.map f = nil ↔ p = nil := by cases p <;> simp
 
 @[simp]

Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean

@@ -653,7 +653,7 @@ lemma drop_zero {u v} (p : G.Walk u v) :
 
 lemma nil_drop_of_length_le {u v n} {p : G.Walk u v} (h : p.length ≤ n) :
     (p.drop n).Nil := by
-  rw [nil_iff_length_eq, drop_length, Nat.sub_eq_zero_of_le h]
+  rw [← length_eq_zero_iff, drop_length, Nat.sub_eq_zero_of_le h]
 
 lemma drop_support_eq_support_drop_min {u v} (p : G.Walk u v) (n : ℕ) :
     (p.drop n).support = p.support.drop (n ⊓ p.length) := by
@@ -702,8 +702,8 @@ lemma dropLast_concat {t u v} (p : G.Walk u v) (h : G.Adj v t) :
     (p.concat h).dropLast = p.copy rfl (by simp) := by
   induction p
   · rfl
-  · simp_rw [concat_cons]
-    rw [dropLast_cons_of_not_nil] <;> simp [*, nil_iff_length_eq]
+  · rw! [concat_cons, dropLast_cons_of_not_nil] <;>
+      simp [*, ← length_eq_zero_iff]
 
 lemma cons_tail_eq (p : G.Walk u v) (hp : ¬ p.Nil) :
     cons (p.adj_snd hp) p.tail = p := by
@@ -756,11 +756,8 @@ protected lemma Nil.dropLast {p : G.Walk v w} (hp : p.Nil) : p.dropLast.Nil := b
   subst_vars
   rfl
 
-lemma Nil.eq_copy_nil {p : G.Walk u v} (h : p.Nil) :
-    p = Walk.nil.copy rfl h.eq := by
-  have := h.eq
-  subst this
-  simp [nil_iff_eq_nil.mp h]
+lemma Nil.eq_copy_nil {p : G.Walk u v} (h : p.Nil) : p = Walk.nil.copy rfl h.eq := by
+  grind [eq_nil_iff_nil, copy_rfl_rfl]
 
 lemma drop_of_length_le {u v n} {p : G.Walk u v} (h : p.length ≤ n) :
     p.drop n = nil.copy rfl (p.getVert_of_length_le h) :=

Mathlib/Combinatorics/SimpleGraph/Walk/Traversal.lean

@@ -178,11 +178,8 @@ lemma penultimate_cons_of_not_nil (h : G.Adj u v) (p : G.Walk v w) (hp : ¬ p.Ni
   p.notNilRec (by simp) hp h
 
 @[simp]
-lemma adj_penultimate {p : G.Walk v w} (hp : ¬ p.Nil) :
-    G.Adj p.penultimate w := by
-  conv => rhs; rw [← getVert_length p]
-  rw [nil_iff_length_eq] at hp
-  convert adj_getVert_succ _ _ <;> lia
+lemma adj_penultimate {p : G.Walk v w} (hp : ¬ p.Nil) : G.Adj p.penultimate w := by
+  grind [getVert_length, length_eq_zero_iff, adj_getVert_succ]
 
 lemma penultimate_mem_dropLast_support {p : G.Walk u v} (h : ¬p.Nil) :
     p.penultimate ∈ p.support.dropLast := by