chore: address review comments and sync with master

Author: 0xTerencePrime

Mathlib/Combinatorics/SimpleGraph/Connectivity/VertexConnectivity.lean

@@ -17,7 +17,7 @@ This file defines k-vertex connectivity for simple graphs.
 * `SimpleGraph.IsVertexReachable`: Two vertices are `k`-vertex-reachable if they remain reachable
   after removing strictly fewer than `k` other vertices.
 * `SimpleGraph.IsVertexConnected`: A graph is `k`-vertex-connected if it has more than `k`
-  vertices and any two distinct vertices are `k`-vertex-reachable.
+  vertices and any two vertices are `k`-vertex-reachable.
 -/
 
 @[expose] public section
@@ -26,28 +26,28 @@ namespace SimpleGraph
 
 variable {V : Type*} {G H : SimpleGraph V} {k l : ℕ∞} {u v : V}
 
-/-- `G.deleteVerts s` is the graph where all vertices in `s` are isolated. -/
-def deleteVerts (G : SimpleGraph V) (s : Set V) : SimpleGraph V where
+/-- `G.isolateVerts s` is the graph where all vertices in `s` are isolated. -/
+def isolateVerts (G : SimpleGraph V) (s : Set V) : SimpleGraph V where
   Adj u v := u ∉ s ∧ v ∉ s ∧ G.Adj u v
   symm _ _ h := ⟨h.2.1, h.1, h.2.2.symm⟩
 
 @[simp]
-lemma deleteVerts_empty : G.deleteVerts ∅ = G := by
-  ext; simp [deleteVerts]
+lemma isolateVerts_empty : G.isolateVerts ∅ = G := by
+  ext; simp [isolateVerts]
 
 @[simp]
-lemma deleteVerts_bot (s : Set V) : (⊥ : SimpleGraph V).deleteVerts s = ⊥ := by
-  ext; simp [deleteVerts]
+lemma isolateVerts_bot (s : Set V) : (⊥ : SimpleGraph V).isolateVerts s = ⊥ := by
+  ext; simp [isolateVerts]
 
 @[simp]
-lemma deleteVerts_le (s : Set V) : G.deleteVerts s ≤ G :=
+lemma isolateVerts_le (s : Set V) : G.isolateVerts s ≤ G :=
   fun _ _ h ↦ h.2.2
 
 variable (G k u v) in
 /-- Two vertices are `k`-vertex-reachable if they remain reachable after removing
 strictly fewer than `k` other vertices. -/
 def IsVertexReachable : Prop :=
-  ∀ ⦃s : Set V⦄, s.encard < k → u ∉ s → v ∉ s → (G.deleteVerts s).Reachable u v
+  ∀ ⦃s : Set V⦄, s.encard < k → u ∉ s → v ∉ s → (G.isolateVerts s).Reachable u v
 
 @[simp]
 lemma IsVertexReachable.refl (u : V) : G.IsVertexReachable k u u :=
@@ -71,71 +71,85 @@ lemma IsVertexReachable.anti (hkl : k ≤ l) (h : G.IsVertexReachable l u v) :
   fun _ hs ↦ h (hs.trans_le hkl)
 
 @[simp]
-protected lemma IsVertexReachable.zero : G.IsVertexReachable 0 u v :=
-  fun _ hs ↦ absurd hs (not_lt_of_ge (zero_le _))
+lemma IsVertexReachable.zero : G.IsVertexReachable 0 u v :=
+  fun _ hs ↦ absurd hs not_lt_zero
 
 lemma IsVertexReachable.of_adj (h : G.Adj u v) (k : ℕ∞) : G.IsVertexReachable k u v :=
   fun _ _ hu hv ↦ (Adj.reachable ⟨hu, hv, h⟩)
 
+alias _root_.SimpleGraph.Adj.isVertexReachable := IsVertexReachable.of_adj
+
 /-- A vertex pair is reachable if it is `k`-vertex-reachable for `k ≠ 0`. -/
-lemma IsVertexReachable.reachable {hk : k ≠ 0} (h : G.IsVertexReachable k u v) :
+lemma IsVertexReachable.reachable (hk : k ≠ 0) (h : G.IsVertexReachable k u v) :
     G.Reachable u v := by
-  have := pos_iff_ne_zero.mpr hk
-  specialize h (s := ∅) (by simpa) (by simp) (by simp)
-  rwa [deleteVerts_empty] at h
+  rw [← G.isolateVerts_empty]
+  apply h <;> simp [pos_of_ne_zero hk]
 
-variable (G k) in
+variable (G) (k : ℕ∞) in
 /-- A graph is `k`-vertex-connected if it has more than `k` vertices
-and any two distinct vertices are `k`-vertex-reachable. -/
-def IsVertexConnected [Fintype V] (k : ℕ) : Prop :=
-  k < Fintype.card V ∧ ∀ u v : V, u ≠ v → G.IsVertexReachable k u v
+and any two vertices are `k`-vertex-reachable. -/
+def IsVertexConnected : Prop :=
+  k + 1 ≤ ENat.card V ∧ ∀ u v : V, G.IsVertexReachable k u v
 
 @[simp]
-lemma isVertexConnected_zero [Fintype V] : G.IsVertexConnected 0 ↔ Nonempty V := by
-  simp [IsVertexConnected, Fintype.card_pos_iff]
+lemma isVertexConnected_zero : G.IsVertexConnected 0 ↔ Nonempty V := by
+  rw [IsVertexConnected]
+  have h0 : (0 : ℕ∞) + 1 = 1 := rfl
+  rw [h0]
+  simp [ENat.one_le_card_iff_nonempty]
 
 /-- 1-vertex-connectivity is equivalent to being a connected graph with at least 2 vertices. -/
-@[simp]
-protected lemma isVertexConnected_one [Fintype V] :
-    G.IsVertexConnected 1 ↔ 1 < Fintype.card V ∧ G.Connected := by
-  classical
+lemma isVertexConnected_one :
+    G.IsVertexConnected 1 ↔ 2 ≤ ENat.card V ∧ G.Connected := by
+  rw [IsVertexConnected]
+  have h1 : (1 : ℕ∞) + 1 = 2 := rfl
+  rw [h1]
   constructor
   · rintro ⟨h_card, h_reach⟩
     refine ⟨h_card, ?_⟩
     rw [connected_iff_exists_forall_reachable]
-    have := Fintype.card_pos_iff.1 (zero_lt_one.trans h_card)
-    rcases this with ⟨x⟩
-    refine ⟨x, fun y ↦ ?_⟩
-    by_cases hxy : x = y
-    · subst hxy; exact .refl _
-    · specialize h_reach x y hxy
-      simpa using h_reach (s := ∅) (by simp)
+    have h_ne : Nonempty V := by
+      rw [← ENat.one_le_card_iff_nonempty]
+      exact (self_le_add_right (1 : ℕ∞) 1).trans h_card
+    rcases h_ne with ⟨x⟩
+    refine ⟨x, fun y ↦ (h_reach x y).reachable (by simp)⟩
   · rintro ⟨h_card, h_conn⟩
-    refine ⟨h_card, fun u v huv ↦ ?_⟩
-    intro s hs hu hv
+    refine ⟨h_card, fun u v s hs _ _ ↦ ?_⟩
     have : s = ∅ := by
       rw [← Set.encard_eq_zero, ← ENat.lt_one_iff_eq_zero]
-      exact_mod_cast hs
+      exact hs
     subst this
-    rw [deleteVerts_empty]
+    rw [isolateVerts_empty]
     exact h_conn.preconnected u v
 
 /-- Vertex connectivity is antitonic in `k`. -/
-@[gcongr]
-lemma IsVertexConnected.anti [Fintype V] {k l : ℕ} (hkl : l ≤ k) (hc : G.IsVertexConnected k) :
-    G.IsVertexConnected l :=
-  ⟨hkl.trans_lt hc.1, fun u v huv ↦ (hc.2 u v huv).anti (Nat.cast_le.mpr hkl)⟩
+lemma IsVertexConnected.anti {k l : ℕ∞} (hkl : l ≤ k) (hc : G.IsVertexConnected k) :
+    G.IsVertexConnected l := by
+  constructor
+  · let h_le := add_le_add_right hkl 1
+    let h_card := hc.1
+    have h1 : l + 1 = 1 + l := add_comm ..
+    have h2 : k + 1 = 1 + k := add_comm ..
+    rw [h1]
+    rw [h2] at h_card
+    exact h_le.trans h_card
+  · exact fun u v ↦ (hc.2 u v).anti hkl
 
 /-- Vertex connectivity is monotonic in the graph. -/
-@[gcongr]
-lemma IsVertexConnected.mono [Fintype V] {k : ℕ} (hGH : G ≤ H) (hc : G.IsVertexConnected k) :
+lemma IsVertexConnected.mono {k : ℕ∞} (hGH : G ≤ H) (hc : G.IsVertexConnected k) :
     H.IsVertexConnected k :=
-  ⟨hc.1, fun u v huv ↦ (hc.2 u v huv).mono hGH⟩
+  ⟨hc.1, fun u v ↦ (hc.2 u v).mono hGH⟩
 
 /-- The complete graph on `n` vertices is `(n-1)`-vertex-connected. -/
-lemma isVertexConnected_completeGraph [Fintype V] [Nonempty V] :
-    (⊤ : SimpleGraph V).IsVertexConnected (Fintype.card V - 1) :=
-  ⟨Nat.sub_lt Fintype.card_pos Nat.zero_lt_one,
-   fun u v huv ↦ IsVertexReachable.of_adj (by simp [huv]) _⟩
+lemma isVertexConnected_top [Fintype V] [Nonempty V] :
+    (⊤ : SimpleGraph V).IsVertexConnected (Fintype.card V - 1) := by
+  constructor
+  · rw [ENat.card_eq_coe_fintype_card]
+    norm_cast
+    exact Nat.sub_add_cancel Fintype.card_pos |>.le
+  · intro u v
+    by_cases h : u = v
+    · subst h; exact .refl _
+    · exact IsVertexReachable.of_adj h _
 
 end SimpleGraph