feat(Combinatorics/SimpleGraph/Acyclic): IsAcyclic -> IsBipartite (#32568)

This generalizes the existing `IsTree` -> `IsBipartite` result.

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

@@ -454,27 +454,36 @@ lemma Connected.exists_preconnected_induce_compl_singleton_of_finite [Finite V]
   obtain ⟨v, hv⟩ := hconn.exists_connected_induce_compl_singleton_of_finite_nontrivial
   exact ⟨v, hv.preconnected⟩
 
-lemma IsTree.dist_ne_of_adj (hG : G.IsTree) (u : V) {v w : V} (hadj : G.Adj v w) :
-    G.dist u v ≠ G.dist u w := by
-  obtain ⟨p, hp, hp'⟩ := hG.isConnected.exists_path_of_dist u v
-  obtain ⟨q, hq, hq'⟩ := hG.isConnected.exists_path_of_dist u w
+lemma IsAcyclic.dist_ne_of_adj (hG : G.IsAcyclic) {u v w : V} (hadj : G.Adj v w)
+    (hreach : G.Reachable u v) : G.dist u v ≠ G.dist u w := by
+  obtain ⟨p, hp, hp'⟩ := hreach.exists_path_of_dist
+  obtain ⟨q, hq, hq'⟩ := hreach.trans hadj.reachable |>.exists_path_of_dist
   rw [← hp', ← hq']
   by_cases hw : w ∈ p.support
-  · rw [hG.IsAcyclic.path_concat hq hp hadj.symm hw, q.length_concat]
+  · rw [hG.path_concat hq hp hadj.symm hw, q.length_concat]
     exact q.length.ne_add_one.symm
-  · have hv : v ∈ q.support := hG.IsAcyclic.mem_support_of_ne_mem_support_of_adj_of_isPath hq hp
+  · have hv : v ∈ q.support := hG.mem_support_of_ne_mem_support_of_adj_of_isPath hq hp
       hadj.symm hw
-    rw [hG.IsAcyclic.path_concat hp hq hadj hv, p.length_concat]
+    rw [hG.path_concat hp hq hadj hv, p.length_concat]
     exact p.length.ne_add_one
 
-lemma IsTree.diff_dist_adj (hG : G.IsTree) (u : V) {v w : V} (hadj : SimpleGraph.Adj G v w) :
-    G.dist u v = G.dist u w + 1 ∨ G.dist u v + 1 = G.dist u w := by
-  grind [dist_ne_of_adj, Connected.diff_dist_adj, IsTree]
+lemma IsTree.dist_ne_of_adj (hG : G.IsTree) (u : V) {v w : V} (hadj : G.Adj v w) :
+    G.dist u v ≠ G.dist u w :=
+  hG.IsAcyclic.dist_ne_of_adj hadj <| hG.isConnected u v
+
+lemma IsAcyclic.dist_eq_dist_add_one_of_adj_of_reachable
+    (hG : G.IsAcyclic) (u : V) {v w : V} (hadj : G.Adj v w) (hreach : G.Reachable u v) :
+    G.dist u v = G.dist u w + 1 ∨ G.dist u w = G.dist u v + 1 := by
+  grind [dist_ne_of_adj, Adj.diff_dist_adj]
+
+lemma IsTree.dist_eq_dist_add_one_of_adj (hG : G.IsTree) (u : V) {v w : V} (hadj : G.Adj v w) :
+    G.dist u v = G.dist u w + 1 ∨ G.dist u w = G.dist u v + 1 := by
+  grind [dist_ne_of_adj, Adj.diff_dist_adj]
 
 /-- The unique two-coloring of a tree that colors the given vertex with zero -/
 noncomputable def IsTree.coloringTwoOfVert (hG : G.IsTree) (u : V) : G.Coloring (Fin 2) :=
   Coloring.mk (fun v ↦ ⟨G.dist u v % 2, Nat.mod_lt (G.dist u v) Nat.zero_lt_two⟩) <| by
-    grind [diff_dist_adj]
+    grind [dist_eq_dist_add_one_of_adj]
 
 /-- Arbitrary coloring with two colors for a tree -/
 noncomputable def IsTree.coloringTwo (hG : G.IsTree) : G.Coloring (Fin 2) :=
@@ -483,4 +492,23 @@ noncomputable def IsTree.coloringTwo (hG : G.IsTree) : G.Coloring (Fin 2) :=
 lemma IsTree.isBipartite (hG : G.IsTree) : G.IsBipartite :=
   ⟨hG.coloringTwo⟩
 
+/-- The unique two-coloring of a forest that colors the given vertices with zero -/
+noncomputable def IsAcyclic.coloringTwoOfVerts (hG : G.IsAcyclic) (verts : G.ConnectedComponent → V)
+    (h : ∀ C, verts C ∈ C) : G.Coloring (Fin 2) where
+  toFun v :=
+    let u := verts <| G.connectedComponentMk v
+    ⟨G.dist u v % 2, Nat.mod_lt (G.dist u v) Nat.zero_lt_two⟩
+  map_rel' := by
+    intro u v hadj
+    have := ConnectedComponent.sound hadj.reachable
+    have := hG.dist_eq_dist_add_one_of_adj_of_reachable _ hadj <| ConnectedComponent.exact <| h _
+    grind [top_adj]
+
+/-- Arbitrary coloring with two colors for a forest -/
+noncomputable def IsAcyclic.coloringTwo (hG : G.IsAcyclic) : G.Coloring (Fin 2) :=
+  hG.coloringTwoOfVerts (·.nonempty_supp.some) (·.nonempty_supp.some_mem)
+
+lemma IsAcyclic.isBipartite (hG : G.IsAcyclic) : G.IsBipartite :=
+  ⟨hG.coloringTwo⟩
+
 end SimpleGraph

Mathlib/Combinatorics/SimpleGraph/Metric.lean

@@ -172,6 +172,10 @@ variable {G} {u v w : V}
 theorem dist_eq_sInf : G.dist u v = sInf (Set.range (Walk.length : G.Walk u v → ℕ)) :=
   ENat.iInf_toNat
 
+@[grind =]
+lemma Reachable.coe_dist_eq_edist (h : G.Reachable u v) : G.dist u v = G.edist u v :=
+  ENat.coe_toNat <| edist_ne_top_iff_reachable.mpr h
+
 protected theorem Reachable.exists_walk_length_eq_dist (hr : G.Reachable u v) :
     ∃ p : G.Walk u v, p.length = G.dist u v :=
   dist_eq_sInf ▸ Nat.sInf_mem (Set.range_nonempty_iff_nonempty.mpr hr)
@@ -187,6 +191,7 @@ theorem dist_le (p : G.Walk u v) : G.dist u v ≤ p.length :=
 theorem dist_eq_zero_iff_eq_or_not_reachable :
     G.dist u v = 0 ↔ u = v ∨ ¬G.Reachable u v := by simp [dist_eq_sInf, Nat.sInf_eq_zero, Reachable]
 
+@[simp, grind =]
 theorem dist_self : dist G v v = 0 := by simp
 
 protected theorem Reachable.dist_eq_zero_iff (hr : G.Reachable u v) :
@@ -230,6 +235,20 @@ protected theorem Connected.dist_triangle (hconn : G.Connected) :
   rw [← hp, ← hq, ← Walk.length_append]
   apply dist_le
 
+lemma Reachable.dist_triangle_left (h : G.Reachable u v) (w) :
+    G.dist u w ≤ G.dist u v + G.dist v w := by
+  by_cases! h' : ¬G.Reachable u w
+  · grind [dist_eq_zero_iff_eq_or_not_reachable]
+  rw [← ENat.coe_le_coe, ENat.coe_add]
+  grind [SimpleGraph.edist_triangle, Reachable.trans, Reachable.symm]
+
+lemma Reachable.dist_triangle_right (h : G.Reachable v w) (u) :
+    G.dist u w ≤ G.dist u v + G.dist v w := by
+  by_cases! h' : ¬G.Reachable u w
+  · grind [dist_eq_zero_iff_eq_or_not_reachable]
+  rw [← ENat.coe_le_coe, ENat.coe_add]
+  grind [SimpleGraph.edist_triangle, Reachable.trans, Reachable.symm]
+
 theorem dist_comm : G.dist u v = G.dist v u := by
   rw [dist, dist, edist_comm]
 
@@ -251,12 +270,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) :
+theorem Adj.diff_dist_adj (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
+  by_cases! huw : ¬G.Reachable u w
+  · grind [dist_eq_zero_iff_eq_or_not_reachable, Reachable.trans, Adj.reachable]
   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
+  have : G.dist u w ≤ G.dist u v + G.dist v w := hadj.reachable.dist_triangle_right u
+  have : G.dist u v ≤ G.dist u w + G.dist w v := huw.dist_triangle_left v
   lia
 
 theorem Walk.isPath_of_length_eq_dist (p : G.Walk u v) (hp : p.length = G.dist u v) :