feat(SimpleGraph): add universal vertex predicate (leanprover-community#38589)

Add the predicate `G.IsUniversal v` to indicate that `v` is a universal vertex, i.e. connected to all other vertices in `G`. This matches the recently added `G.IsIsolated v` predicate for isolated vertices.

Co-authored-by: Justin Lai <justsoft.jsoft@gmail.com>

Author: vlad902

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -1019,10 +1019,72 @@ theorem Adj.not_isIsolated_right (h : G.Adj u v) : ¬G.IsIsolated v :=
   h.symm.not_isIsolated_left
 
 @[simp]
-theorem isIsolated_bot : IsIsolated ⊥ v :=
+protected theorem IsIsolated.bot : IsIsolated ⊥ v :=
   neighborSet_eq_empty _ |>.mp neighborSet_bot
 
+@[deprecated (since := "2026-06-19")]
+alias isIsolated_bot := IsIsolated.bot
+
 theorem eq_bot_iff_isIsolated : G = ⊥ ↔ ∀ v, G.IsIsolated v := by
   simp [eq_bot_iff_forall_not_adj, ← neighborSet_eq_empty, Set.eq_empty_iff_forall_notMem]
 
+section IsUniversal
+
+variable {G}
+
+/-- A vertex in a graph is universal if it's adjacent to every other vertex. -/
+def IsUniversal (G : SimpleGraph V) (v : V) : Prop := ∀ ⦃w⦄, v ≠ w → G.Adj v w
+
+@[simp] lemma insert_neighborSet_eq_univ :
+    insert v (G.neighborSet v) = Set.univ ↔ G.IsUniversal v := by
+  simp only [Set.ext_iff, Set.mem_insert_iff, mem_neighborSet, IsUniversal]
+  grind
+
+@[simp] lemma neighborSet_eq_compl_singleton : G.neighborSet v = {v}ᶜ ↔ G.IsUniversal v := by
+  grind [insert_neighborSet_eq_univ, notMem_neighborSet_self]
+
+protected alias ⟨IsUniversal.of_neighborSet_eq, IsUniversal.neighborSet_eq⟩ :=
+  neighborSet_eq_compl_singleton
+
+@[simp]
+theorem IsUniversal.of_subsingleton [Subsingleton V] : G.IsUniversal v :=
+  fun _ hne ↦ False.elim <| hne (Subsingleton.elim ..)
+
+theorem IsUniversal.not_isIsolated [Nontrivial V] (h : G.IsUniversal v) (w : V) :
+    ¬G.IsIsolated w := by
+  by_cases h' : v = w
+  · obtain ⟨u, hu⟩ := exists_ne v
+    exact h' ▸ Adj.not_isIsolated_left (h hu.symm)
+  · exact Adj.not_isIsolated_right (h h')
+
+theorem IsIsolated.not_isUniversal [Nontrivial V] (h : G.IsIsolated v) (w : V) :
+    ¬G.IsUniversal w := by
+  contrapose! h
+  exact h.not_isIsolated v
+
+@[simp]
+theorem isUniversal_compl_iff_isIsolated : Gᶜ.IsUniversal v ↔ G.IsIsolated v := by
+  refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩
+  · simpa [hx] using h hx.ne
+  · simpa [hx] using h x
+
+alias ⟨IsIsolated.of_isUniversal_compl, _⟩ := isUniversal_compl_iff_isIsolated
+
+@[simp]
+theorem isIsolated_compl_iff_isUniversal : Gᶜ.IsIsolated v ↔ G.IsUniversal v := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · simpa using isUniversal_compl_iff_isIsolated.mpr h
+  · exact isUniversal_compl_iff_isIsolated.mp (by simpa)
+
+alias ⟨IsUniversal.of_isIsolated_compl, _⟩ := isIsolated_compl_iff_isUniversal
+
+theorem eq_top_iff_forall_isUniversal : G = ⊤ ↔ ∀ v, G.IsUniversal v := by
+  simp [eq_top_iff_forall_ne_adj, IsUniversal]
+
+@[simp]
+protected theorem IsUniversal.top : IsUniversal ⊤ v :=
+  eq_top_iff_forall_isUniversal.mp rfl v
+
+end IsUniversal
+
 end SimpleGraph

Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

@@ -197,6 +197,12 @@ lemma Reachable.degree_pos_right {G : SimpleGraph V} {u v : V} [Fintype (G.neigh
     (huv : u ≠ v) (hreach : G.Reachable u v) : 0 < G.degree v :=
   hreach.symm.degree_pos_left huv.symm
 
+lemma Reachable.of_isUniversal {G : SimpleGraph V} {u : V} (v : V) (h : G.IsUniversal u) :
+    G.Reachable u v := by
+  by_cases! h' : u = v
+  · exact h' ▸ Reachable.rfl
+  · exact (h h').reachable
+
 lemma not_reachable_of_neighborSet_left_eq_empty {G : SimpleGraph V} {u v : V} (huv : u ≠ v)
     (hu : G.neighborSet u = ∅) : ¬G.Reachable u v :=
   (Reachable.nonempty_neighborSet_left huv).mt (Set.not_nonempty_iff_eq_empty.mpr hu)
@@ -374,6 +380,11 @@ theorem connected_or_preconnected_compl : G.Connected ∨ Gᶜ.Preconnected := b
 theorem connected_or_connected_compl [Nonempty V] : G.Connected ∨ Gᶜ.Connected :=
   G.connected_or_preconnected_compl.elim .inl (.inr ⟨·⟩)
 
+variable {G v} in
+lemma Connected.of_isUniversal (h : G.IsUniversal v) : G.Connected := by
+  refine connected_iff _ |>.mpr ⟨fun u w ↦ ?_, ⟨v⟩⟩
+  exact (Reachable.of_isUniversal u h).symm.trans (Reachable.of_isUniversal w h)
+
 /-- The quotient of `V` by the `SimpleGraph.Reachable` relation gives the connected
 components of a graph. -/
 def ConnectedComponent := Quot G.Reachable

Mathlib/Combinatorics/SimpleGraph/Finite.lean

@@ -547,6 +547,28 @@ theorem card_commonNeighbors_top [DecidableEq V] {v w : V} (h : v ≠ w) :
     Fintype.card (commonNeighbors ⊤ v w) = Fintype.card V - 2 := by
   simp [commonNeighbors_top_eq, ← Set.toFinset_card, Finset.card_sdiff, h]
 
+@[simp] lemma insert_neighborFinset_eq_univ [DecidableEq V] [DecidableRel G.Adj] (v : V) :
+    insert v (G.neighborFinset v) = univ ↔ G.IsUniversal v := by
+  simp only [Finset.ext_iff, mem_insert, mem_neighborFinset, IsUniversal]
+  grind
+
+@[simp] lemma neighborFinset_eq_erase_univ [DecidableEq V] [DecidableRel G.Adj] (v : V) :
+    G.neighborFinset v = univ.erase v ↔ G.IsUniversal v := by
+  grind [insert_neighborFinset_eq_univ, notMem_neighborFinset_self]
+
+@[simp]
+lemma degree_eq_card_sub_one [DecidableRel G.Adj] (v : V) :
+    G.degree v = Fintype.card V - 1 ↔ G.IsUniversal v := by
+  classical
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · rw [← G.insert_neighborFinset_eq_univ v, ← Finset.card_eq_iff_eq_univ]
+    simp [h, Nat.sub_add_cancel <| Fintype.card_pos_iff.mpr ⟨v⟩]
+  · simp [← card_neighborFinset_eq_degree, (G.neighborFinset_eq_erase_univ v).mpr h]
+
+lemma degree_lt_card_sub_one [DecidableRel G.Adj] (v : V) :
+    G.degree v < Fintype.card V - 1 ↔ ¬ G.IsUniversal v := by
+  grind [degree_eq_card_sub_one, Nat.le_sub_one_of_lt <| G.degree_lt_card_verts v]
+
 end Finite
 
 namespace Iso

Mathlib/Combinatorics/SimpleGraph/Star.lean

@@ -43,6 +43,11 @@ instance [DecidableEq V] (r : V) : DecidableRel (starGraph r).Adj :=
 lemma starGraph_adj {r x y : V} : (starGraph r).Adj x y ↔ x ≠ y ∧ (x = r ∨ y = r) := by
   simp [starGraph, fromRel]
 
+@[simp]
+lemma isUniversal_starGraph_self {r : V} : (starGraph r).IsUniversal r := by
+  intro _ _
+  simpa
+
 /-- On (starGraph r), r is adjacent to v iff v ≠ r. -/
 lemma starGraph_adj_center_iff {r v : V} : (starGraph r).Adj r v ↔ r ≠ v := by simp
 
@@ -52,12 +57,8 @@ lemma starGraph_center_adj {r v : V} (h : r ≠ v) : (starGraph r).Adj r v :=
 lemma starGraph_center_adj' {r v : V} (h : r ≠ v) : (starGraph r).Adj v r :=
   (starGraph_center_adj h).symm
 
-lemma connected_starGraph (r : V) : (starGraph r).Connected := by
-  have (v : V) : (starGraph r).Reachable r v := by
-    by_cases! h : r = v
-    · exact h ▸ Reachable.rfl
-    · exact (starGraph_center_adj h).reachable
-  exact connected_iff _ |>.mpr ⟨fun u v ↦ (this u).symm.trans (this v), ⟨r⟩⟩
+lemma connected_starGraph (r : V) : (starGraph r).Connected :=
+  .of_isUniversal isUniversal_starGraph_self
 
 lemma isAcyclic_starGraph (r : V) : (starGraph r).IsAcyclic := by
   refine isAcyclic_iff_forall_adj_isBridge.mpr fun v w hadj ↦ ?_
@@ -81,6 +82,6 @@ lemma degree_starGraph_of_ne_center [Fintype V] [DecidableEq V] {r v : V} (h : v
 /-- The center vertex of a starGraph has degree (card V) - 1. -/
 lemma degree_starGraph_center [Fintype V] [DecidableEq V] {r : V} :
     (starGraph r).degree r = Fintype.card V - 1 := by
-  simp [degree, neighborFinset_eq_filter (starGraph r), starGraph_adj, Finset.univ.filter_ne r]
+  simp
 
 end SimpleGraph

Mathlib/Combinatorics/SimpleGraph/Tutte.lean

@@ -294,21 +294,21 @@ lemma exists_isTutteViolator (h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching)
     obtain ⟨p, hp⟩ := Reachable.exists_path_of_dist (K.connected_toSimpleGraph x y)
     obtain ⟨x, a, b, hxa, hxb, hnadjxb, hnxb⟩ := Walk.exists_adj_adj_not_adj_ne hp.2
       (p.reachable.one_lt_dist_of_ne_of_not_adj hxy.1 hxy.2)
-    simp only [ConnectedComponent.toSimpleGraph, deleteUniversalVerts, universalVerts, ne_eq,
+    simp only [ConnectedComponent.toSimpleGraph, deleteUniversalVerts, universalVerts,
       Subgraph.verts_top, comap_adj, Function.Embedding.coe_subtype,
       Subgraph.coe_adj, Subgraph.induce_adj, Subtype.coe_prop, Subgraph.top_adj, true_and]
       at hxa hxb hnadjxb
-    obtain ⟨c, hc⟩ : ∃ (c : V), (a : V) ≠ c ∧ ¬ Gmax.Adj c a := by
-      simpa [universalVerts] using a.1.2.2
-    have hbnec : b.val.val ≠ c := by rintro rfl; exact hc.2 hxb.symm
+    obtain ⟨c, hc⟩ : ∃ (c : V), (a : V) ≠ c ∧ ¬ Gmax.Adj a c := by
+      simpa [universalVerts, IsUniversal] using a.1.2.2
+    have hbnec : b.val.val ≠ c := by rintro rfl; exact hc.2 hxb
     obtain ⟨_, hG1⟩ := hMaximal _ <| left_lt_sup.mpr (by
       rw [edge_le_iff (v := x.1.1) (w := b.1.1)]
       simp [hnadjxb, Subtype.val_injective.ne <| Subtype.val_injective.ne hnxb])
     obtain ⟨_, hG2⟩ := hMaximal _ <| left_lt_sup.mpr (by
-      rwa [edge_le_iff (v := a.1.1) (w := c), adj_comm, not_or])
-    have hcnex : c ≠ x.val.val := by rintro rfl; exact hc.2 hxa
+      rwa [edge_le_iff (v := a.1.1) (w := c), not_or])
+    have hcnex : x.val.val ≠ c := by rintro rfl; exact hc.2 hxa.symm
     obtain ⟨Mcon, hMcon⟩ := tutte_exists_isPerfectMatching_of_near_matchings hxa
-      hxb hnadjxb (fun hadj ↦ hc.2 hadj.symm) (by lia) hcnex.symm hc.1 hbnec hG1 hG2
+      hxb hnadjxb (fun hadj ↦ hc.2 hadj) (by lia) hcnex hc.1 hbnec hG1 hG2
     exact hMatchingFree Mcon hMcon
 
 /-- **Tutte's theorem**

Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean

@@ -33,10 +33,10 @@ variable {V : Type*} {G : SimpleGraph V}
 /--
 The set of vertices that are connected to all other vertices.
 -/
-def universalVerts (G : SimpleGraph V) : Set V := {v : V | ∀ ⦃w⦄, v ≠ w → G.Adj w v}
+def universalVerts (G : SimpleGraph V) : Set V := {v : V | G.IsUniversal v}
 
 lemma isClique_universalVerts (G : SimpleGraph V) : G.IsClique G.universalVerts :=
-  fun _ _ _ hy hxy ↦ hy hxy.symm
+  fun _ hx _ _ hxy ↦ hx hxy
 
 /--
 The subgraph of `G` with the universal vertices removed.
@@ -53,7 +53,7 @@ lemma Subgraph.IsMatching.exists_of_universalVerts [Finite V] {s : Set V}
   obtain ⟨f⟩ : Nonempty (s ≃ t) := by
     rw [← Cardinal.eq, ← t.cast_ncard t.toFinite, ← s.cast_ncard s.toFinite, ht.2]
   letI hd := Set.disjoint_of_subset_left ht.1 h
-  have hadj (v : s) : G.Adj v (f v) := ht.1 (f v).2 (hd.ne_of_mem (f v).2 v.2)
+  have hadj (v : s) : G.Adj v (f v) := ht.1 (f v).2 (hd.ne_of_mem (f v).2 v.2) |>.symm
   exact Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv hd.symm f hadj
 
 lemma disjoint_image_val_universalVerts (s : Set G.deleteUniversalVerts.verts) :