feat(Combinatorics/SimpleGraph): add theorem SimpleGraph.Connected.diff_dist_adj (#27468)

This contribution was created as part of the Utrecht Summerschool "Formalizing Mathematics in Lean" in July 2025.

Author: IvanRenison

Mathlib/Combinatorics/SimpleGraph/Metric.lean

@@ -247,6 +247,14 @@ theorem dist_eq_one_iff_adj : G.dist u v = 1 ↔ G.Adj u v := by
   rw [dist, ENat.toNat_eq_iff, ENat.coe_one, edist_eq_one_iff_adj]
   decide
 
+theorem Connected.diff_dist_adj (hG : G.Connected) (hadj : G.Adj v w) :
+    G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1 := by
+  have : G.dist v w = 1 := dist_eq_one_iff_adj.mpr hadj
+  have : G.dist w v = 1 := dist_eq_one_iff_adj.mpr hadj.symm
+  have : G.dist u w ≤ G.dist u v + G.dist v w := hG.dist_triangle
+  have : G.dist u v ≤ G.dist u w + G.dist w v := hG.dist_triangle
+  omega
+
 theorem Walk.isPath_of_length_eq_dist (p : G.Walk u v) (hp : p.length = G.dist u v) :
     p.IsPath := by
   classical