feat(SimpleGraph): distance equal or greater than two in terms of common neighborhood (leanprover-community#35657)

Two lemmas classifying distances between two vertices according two their common neighborhood. This is the fork version of leanprover-community#12278.

Author: Rida-Hamadani

Mathlib/Combinatorics/SimpleGraph/Metric.lean

@@ -145,6 +145,36 @@ lemma edist_le_one_iff_adj_or_eq : G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v :=
     rw [(Order.one_le_iff_pos.mpr h).ge_iff_eq']
     exact edist_eq_one_iff_adj
 
+lemma edist_eq_two_iff {u v : V} :
+    G.edist u v = 2 ↔ u ≠ v ∧ ¬ G.Adj u v ∧ (G.commonNeighbors u v).Nonempty := by
+  refine ⟨fun h ↦ ⟨?_, ?_, ?_⟩, fun h ↦ le_antisymm ?_ ?_⟩
+  · simp +decide [← G.edist_eq_zero_iff.not (b := u = v), h]
+  · simp +decide [← edist_eq_one_iff_adj, h]
+  · obtain ⟨w, hw⟩ := exists_walk_of_edist_eq_coe h
+    use w.getVert 1
+    suffices w.getVert 1 ∈ G.commonNeighbors (w.getVert 0) (w.getVert w.length) by simpa
+    refine hw ▸ G.mem_commonNeighbors.mp ?_
+    exact ⟨w.adj_getVert_succ (by simp [hw]), (w.adj_getVert_succ (by simp [hw])).symm⟩
+  · obtain ⟨w, hw⟩ := h.2.2
+    rw [mem_commonNeighbors] at hw
+    have := (Walk.cons hw.1 <| .cons hw.2.symm .nil).edist_le
+    simp_all
+  · by_contra! hc
+    cases ENat.le_one_iff_eq_zero_or_eq_one.mp (Order.le_of_lt_succ hc) <;> simp_all
+
+lemma two_lt_edist_iff {u v : V} :
+    2 < G.edist u v ↔ u ≠ v ∧ ¬ G.Adj u v ∧ (G.commonNeighbors u v) = ∅ := by
+  refine ⟨fun h ↦ ?_, fun h ↦ lt_of_le_of_ne ?_ (Ne.symm ?_)⟩
+  · have hn : u ≠ v := fun hc ↦ by simp [hc] at h
+    have : ¬ G.Adj u v := fun hc ↦ by simp +decide [edist_eq_one_iff_adj.mpr hc] at h
+    use hn, this
+    by_contra! hc
+    simp [edist_eq_two_iff.mpr ⟨hn, this, hc⟩] at h
+  · rw [← one_add_one_eq_two]
+    refine Order.add_one_le_of_lt <| lt_of_le_of_ne ?_ ?_
+    <;> grind [Order.one_le_iff_pos, pos_iff_ne_zero, edist_eq_zero_iff, edist_eq_one_iff_adj]
+  · simp_all [edist_eq_two_iff]
+
 lemma edist_bot_of_ne (h : u ≠ v) : (⊥ : SimpleGraph V).edist u v = ⊤ := by
   rwa [ne_eq, ← reachable_bot.not, ← edist_ne_top_iff_reachable.not, not_not] at h
 

Mathlib/Data/ENat/Basic.lean

@@ -303,6 +303,12 @@ theorem one_le_iff_ne_zero : 1 ≤ n ↔ n ≠ 0 :=
 lemma lt_one_iff_eq_zero : n < 1 ↔ n = 0 :=
   not_le.symm.trans one_le_iff_ne_zero.not_left
 
+lemma le_one_iff_eq_zero_or_eq_one : n ≤ 1 ↔ n = 0 ∨ n = 1 := by
+  refine ⟨fun h ↦ ?_, fun h ↦ by cases h <;> simp_all⟩
+  cases n
+  · simp at h
+  · rwa [← lt_one_iff_eq_zero, ← le_iff_lt_or_eq]
+
 theorem lt_add_one_iff (hm : n ≠ ⊤) : m < n + 1 ↔ m ≤ n :=
   Order.lt_add_one_iff_of_not_isMax (not_isMax_iff_ne_top.mpr hm)