From 34ca34e7f9ca17a5eac7e950a54c88b9b6fdb4b3 Mon Sep 17 00:00:00 2001
From: 8e7 <justsoft.jsoft@gmail.com>
Date: Tue, 14 Apr 2026 10:27:40 +0800
Subject: [PATCH 1/9] feat(Combinatorics/SimpleGraph/Acyclic): add star graph

---
 .../Combinatorics/SimpleGraph/Acyclic.lean    | 63 +++++++++++++++++++
 1 file changed, 63 insertions(+)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index e9a1b809ead728..7246bdc173c24e 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -655,4 +655,67 @@ lemma isAcyclic_iff_pairwise_not_isEdgeReachable_two :
   · refine isAcyclic_iff_forall_adj_isBridge.mpr fun _ _ hadj ↦ ?_
     exact isBridge_iff_adj_and_not_isEdgeConnected_two.mpr ⟨hadj, h hadj.ne⟩
 
+section Star
+
+/-- The starGraph graph on `V` centered at `r`: every non-center vertex is adjacent to `r`. -/
+def starGraph (r : V) : SimpleGraph V :=
+  SimpleGraph.fromRel (fun x _ => x = r)
+
+instance [DecidableEq V] (r : V) : DecidableRel (starGraph r).Adj := by
+  unfold starGraph; infer_instance
+
+@[simp]
+lemma starGraph_adj {r x y : V} : (starGraph r).Adj x y ↔ x ≠ y ∧ (x = r ∨ y = r) := by
+  unfold starGraph
+  simp [SimpleGraph.fromRel]
+
+/-- If v ≠ r, then v is adjacent to r. -/
+lemma starGraph_center_adj {r v : V} (h : v ≠ r) : (starGraph r).Adj r v :=
+  starGraph_adj.mpr ⟨h.symm, Or.inl rfl⟩
+
+private lemma starGraph_isPreconnected (r : V) : (starGraph r).Preconnected := by
+  have h_reach : ∀ v, (starGraph r).Reachable r v := by
+    intro v
+    by_cases! h : v = r
+    · subst h; exact Reachable.rfl
+    · exact (starGraph_center_adj h).reachable
+  exact fun u v => (h_reach u).symm.trans (h_reach v)
+
+private lemma starGraph_isAcyclic (r : V) : (starGraph r).IsAcyclic := by
+  rw [isAcyclic_iff_forall_adj_isBridge]
+  intro v w hadj
+  refine isBridge_iff.mpr ⟨hadj, ?_⟩
+  rw [starGraph_adj] at hadj
+  wlog! h : v = r
+  · have hw : w = r := hadj.2.resolve_left h
+    replace hadj : w ≠ v ∧ (w = r ∨ v = r) := ⟨hadj.1.symm, hadj.2.symm⟩
+    rw [reachable_comm, Sym2.eq_swap]
+    exact this r hadj hw
+  · subst h
+    apply not_reachable_of_neighborSet_right_eq_empty hadj.1
+    ext x; aesop
+
+/-- A starGraph graph is a tree. -/
+lemma starGraph_isTree [Nonempty V] (r : V) : (starGraph r).IsTree := by
+  refine ⟨Connected.mk (starGraph_isPreconnected r), starGraph_isAcyclic r⟩
+
+/-- Every non-center vertex of a starGraph has degree one. -/
+lemma starGraph_not_center_imp_degree_one [Fintype V] [DecidableEq V] {r v : V} (h : v ≠ r) :
+    (starGraph r).degree v = 1 := by
+  rw [degree_eq_one_iff_existsUnique_adj]
+  use r
+  simp only [starGraph_adj, ne_eq, or_true, and_true, and_imp]
+  exact ⟨h, fun y _ hx => hx.resolve_left h⟩
+
+/-- The center vertex of a starGraph has degree (card V) - 1. -/
+lemma starGraph_center_degree [Nonempty V] [Fintype V] [DecidableEq V] {r : V} :
+    (starGraph r).degree r = Fintype.card V - 1 := by
+  rw [degree, neighborFinset_eq_filter (starGraph r)]
+  simp only [starGraph_adj, ne_eq, true_or, and_true]
+  have : ({w | ¬r = w} : Finset V) = Finset.univ.erase r := by
+    ext v; simp [eq_comm]
+  rw [this, Finset.card_erase_of_mem (Finset.mem_univ r), Finset.card_univ]
+
+end Star
+
 end SimpleGraph

From e672972d782d036c42e55429c08066fe5d4e9710 Mon Sep 17 00:00:00 2001
From: 8e7 <justsoft.jsoft@gmail.com>
Date: Tue, 14 Apr 2026 11:22:59 +0800
Subject: [PATCH 2/9] Fixing docstrings

---
 Mathlib/Combinatorics/SimpleGraph/Acyclic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index 7246bdc173c24e..700e395f69020f 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -657,7 +657,7 @@ lemma isAcyclic_iff_pairwise_not_isEdgeReachable_two :
 
 section Star
 
-/-- The starGraph graph on `V` centered at `r`: every non-center vertex is adjacent to `r`. -/
+/-- The star graph on `V` centered at `r`: every non-center vertex is adjacent to `r`. -/
 def starGraph (r : V) : SimpleGraph V :=
   SimpleGraph.fromRel (fun x _ => x = r)
 
@@ -695,7 +695,7 @@ private lemma starGraph_isAcyclic (r : V) : (starGraph r).IsAcyclic := by
     apply not_reachable_of_neighborSet_right_eq_empty hadj.1
     ext x; aesop
 
-/-- A starGraph graph is a tree. -/
+/-- A star graph is a tree. -/
 lemma starGraph_isTree [Nonempty V] (r : V) : (starGraph r).IsTree := by
   refine ⟨Connected.mk (starGraph_isPreconnected r), starGraph_isAcyclic r⟩
 

From cfa043990807788d7fa9be6c78f58ff25d496bf4 Mon Sep 17 00:00:00 2001
From: 8e7 <justsoft.jsoft@gmail.com>
Date: Tue, 14 Apr 2026 14:55:31 +0800
Subject: [PATCH 3/9] Golf proofs and set lemmas to public.

---
 .../Combinatorics/SimpleGraph/Acyclic.lean    | 35 ++++++++-----------
 1 file changed, 15 insertions(+), 20 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index 700e395f69020f..7704fb332f649d 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -670,45 +670,40 @@ lemma starGraph_adj {r x y : V} : (starGraph r).Adj x y ↔ x ≠ y ∧ (x = r 
   simp [SimpleGraph.fromRel]
 
 /-- If v ≠ r, then v is adjacent to r. -/
-lemma starGraph_center_adj {r v : V} (h : v ≠ r) : (starGraph r).Adj r v :=
-  starGraph_adj.mpr ⟨h.symm, Or.inl rfl⟩
+lemma starGraph_center_adj {r v : V} (h : r ≠ v) : (starGraph r).Adj r v :=
+  starGraph_adj.mpr ⟨h, Or.inl rfl⟩
 
-private lemma starGraph_isPreconnected (r : V) : (starGraph r).Preconnected := by
-  have h_reach : ∀ v, (starGraph r).Reachable r v := by
+lemma starGraph_isConnected (r : V) : (starGraph r).Connected := by
+  have : ∀ v, (starGraph r).Reachable r v := by
     intro v
-    by_cases! h : v = r
-    · subst h; exact Reachable.rfl
+    by_cases! h : r = v
+    · exact h ▸ Reachable.rfl
     · exact (starGraph_center_adj h).reachable
-  exact fun u v => (h_reach u).symm.trans (h_reach v)
+  exact connected_iff _ |>.mpr ⟨fun u v => (this u).symm.trans (this v), ⟨r⟩⟩
 
-private lemma starGraph_isAcyclic (r : V) : (starGraph r).IsAcyclic := by
-  rw [isAcyclic_iff_forall_adj_isBridge]
-  intro v w hadj
-  refine isBridge_iff.mpr ⟨hadj, ?_⟩
+lemma starGraph_isAcyclic (r : V) : (starGraph r).IsAcyclic := by
+  refine isAcyclic_iff_forall_adj_isBridge.mpr fun v w hadj ↦ isBridge_iff.mpr ⟨hadj, ?_⟩
   rw [starGraph_adj] at hadj
   wlog! h : v = r
   · have hw : w = r := hadj.2.resolve_left h
     replace hadj : w ≠ v ∧ (w = r ∨ v = r) := ⟨hadj.1.symm, hadj.2.symm⟩
     rw [reachable_comm, Sym2.eq_swap]
-    exact this r hadj hw
+    exact this r w v hadj hw
   · subst h
     apply not_reachable_of_neighborSet_right_eq_empty hadj.1
     ext x; aesop
 
 /-- A star graph is a tree. -/
-lemma starGraph_isTree [Nonempty V] (r : V) : (starGraph r).IsTree := by
-  refine ⟨Connected.mk (starGraph_isPreconnected r), starGraph_isAcyclic r⟩
+lemma starGraph_isTree (r : V) : (starGraph r).IsTree := by
+  refine ⟨starGraph_isConnected r, starGraph_isAcyclic r⟩
 
 /-- Every non-center vertex of a starGraph has degree one. -/
 lemma starGraph_not_center_imp_degree_one [Fintype V] [DecidableEq V] {r v : V} (h : v ≠ r) :
-    (starGraph r).degree v = 1 := by
-  rw [degree_eq_one_iff_existsUnique_adj]
-  use r
-  simp only [starGraph_adj, ne_eq, or_true, and_true, and_imp]
-  exact ⟨h, fun y _ hx => hx.resolve_left h⟩
+    (starGraph r).degree v = 1 :=
+  degree_eq_one_iff_existsUnique_adj.mpr ⟨r, by simp [h], by grind [starGraph_adj]⟩
 
 /-- The center vertex of a starGraph has degree (card V) - 1. -/
-lemma starGraph_center_degree [Nonempty V] [Fintype V] [DecidableEq V] {r : V} :
+lemma starGraph_center_degree [Fintype V] [DecidableEq V] {r : V} :
     (starGraph r).degree r = Fintype.card V - 1 := by
   rw [degree, neighborFinset_eq_filter (starGraph r)]
   simp only [starGraph_adj, ne_eq, true_or, and_true]

From eebb8e1c3abadc5243ac56df280c5d5b8403adc4 Mon Sep 17 00:00:00 2001
From: 8e7 <30542113+8e7@users.noreply.github.com>
Date: Tue, 14 Apr 2026 15:37:00 +0800
Subject: [PATCH 4/9] Update Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

Co-authored-by: Vlad Tsyrklevich <vlad902@gmail.com>
---
 Mathlib/Combinatorics/SimpleGraph/Acyclic.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index 9e56dcd5a6a9b8..5f0cd29a9e5fce 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -686,8 +686,7 @@ lemma starGraph_center_adj {r v : V} (h : r ≠ v) : (starGraph r).Adj r v :=
   starGraph_adj.mpr ⟨h, Or.inl rfl⟩
 
 lemma starGraph_isConnected (r : V) : (starGraph r).Connected := by
-  have : ∀ v, (starGraph r).Reachable r v := by
-    intro v
+  have (v : V) : (starGraph r).Reachable r v := by
     by_cases! h : r = v
     · exact h ▸ Reachable.rfl
     · exact (starGraph_center_adj h).reachable

From d3c02331c216b9a7c8e5739d87a204a0e8945e43 Mon Sep 17 00:00:00 2001
From: 8e7 <justsoft.jsoft@gmail.com>
Date: Tue, 14 Apr 2026 15:53:27 +0800
Subject: [PATCH 5/9] Fix lemma naming

---
 Mathlib/Combinatorics/SimpleGraph/Acyclic.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index 9e56dcd5a6a9b8..546427d986d47a 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -685,7 +685,7 @@ lemma starGraph_adj {r x y : V} : (starGraph r).Adj x y ↔ x ≠ y ∧ (x = r 
 lemma starGraph_center_adj {r v : V} (h : r ≠ v) : (starGraph r).Adj r v :=
   starGraph_adj.mpr ⟨h, Or.inl rfl⟩
 
-lemma starGraph_isConnected (r : V) : (starGraph r).Connected := by
+lemma connected_starGraph (r : V) : (starGraph r).Connected := by
   have : ∀ v, (starGraph r).Reachable r v := by
     intro v
     by_cases! h : r = v
@@ -693,7 +693,7 @@ lemma starGraph_isConnected (r : V) : (starGraph r).Connected := by
     · exact (starGraph_center_adj h).reachable
   exact connected_iff _ |>.mpr ⟨fun u v => (this u).symm.trans (this v), ⟨r⟩⟩
 
-lemma starGraph_isAcyclic (r : V) : (starGraph r).IsAcyclic := by
+lemma isAcyclic_starGraph (r : V) : (starGraph r).IsAcyclic := by
   refine isAcyclic_iff_forall_adj_isBridge.mpr fun v w hadj ↦ isBridge_iff.mpr ⟨hadj, ?_⟩
   rw [starGraph_adj] at hadj
   wlog! h : v = r
@@ -706,8 +706,8 @@ lemma starGraph_isAcyclic (r : V) : (starGraph r).IsAcyclic := by
     ext x; aesop
 
 /-- A star graph is a tree. -/
-lemma starGraph_isTree (r : V) : (starGraph r).IsTree := by
-  refine ⟨starGraph_isConnected r, starGraph_isAcyclic r⟩
+lemma isTree_starGraph (r : V) : (starGraph r).IsTree := by
+  refine ⟨connected_starGraph r, isAcyclic_starGraph r⟩
 
 /-- Every non-center vertex of a starGraph has degree one. -/
 lemma starGraph_not_center_imp_degree_one [Fintype V] [DecidableEq V] {r v : V} (h : v ≠ r) :

From 18da22a43c3fbaff1e45cb42945cbe26867855be Mon Sep 17 00:00:00 2001
From: 8e7 <30542113+8e7@users.noreply.github.com>
Date: Wed, 15 Apr 2026 10:16:19 +0800
Subject: [PATCH 6/9] Apply suggestion from @SnirBroshi

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
---
 Mathlib/Combinatorics/SimpleGraph/Acyclic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index ef39d87b3294bb..cd8e04077a0f4b 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -671,7 +671,7 @@ section Star
 
 /-- The star graph on `V` centered at `r`: every non-center vertex is adjacent to `r`. -/
 def starGraph (r : V) : SimpleGraph V :=
-  SimpleGraph.fromRel (fun x _ => x = r)
+ .fromRel fun v _ ↦ v = r
 
 instance [DecidableEq V] (r : V) : DecidableRel (starGraph r).Adj := by
   unfold starGraph; infer_instance

From 43129976e04a5c0b0d4153b5c137e7679639299b Mon Sep 17 00:00:00 2001
From: 8e7 <30542113+8e7@users.noreply.github.com>
Date: Wed, 15 Apr 2026 10:17:23 +0800
Subject: [PATCH 7/9] Apply suggestions from code review
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Iván Renison <85908989+IvanRenison@users.noreply.github.com>
---
 Mathlib/Combinatorics/SimpleGraph/Acyclic.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index cd8e04077a0f4b..8caf618b3f2c91 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -678,8 +678,7 @@ instance [DecidableEq V] (r : V) : DecidableRel (starGraph r).Adj := by
 
 @[simp]
 lemma starGraph_adj {r x y : V} : (starGraph r).Adj x y ↔ x ≠ y ∧ (x = r ∨ y = r) := by
-  unfold starGraph
-  simp [SimpleGraph.fromRel]
+  simp [starGraph, fromRel]
 
 /-- If v ≠ r, then v is adjacent to r. -/
 lemma starGraph_center_adj {r v : V} (h : r ≠ v) : (starGraph r).Adj r v :=
@@ -709,12 +708,12 @@ lemma isTree_starGraph (r : V) : (starGraph r).IsTree := by
   refine ⟨connected_starGraph r, isAcyclic_starGraph r⟩
 
 /-- Every non-center vertex of a starGraph has degree one. -/
-lemma starGraph_not_center_imp_degree_one [Fintype V] [DecidableEq V] {r v : V} (h : v ≠ r) :
+lemma degree_starGraph_of_ne_center [Fintype V] [DecidableEq V] {r v : V} (h : v ≠ r) :
     (starGraph r).degree v = 1 :=
   degree_eq_one_iff_existsUnique_adj.mpr ⟨r, by simp [h], by grind [starGraph_adj]⟩
 
 /-- The center vertex of a starGraph has degree (card V) - 1. -/
-lemma starGraph_center_degree [Fintype V] [DecidableEq V] {r : V} :
+lemma degree_starGraph_center [Fintype V] [DecidableEq V] {r : V} :
     (starGraph r).degree r = Fintype.card V - 1 := by
   rw [degree, neighborFinset_eq_filter (starGraph r)]
   simp only [starGraph_adj, ne_eq, true_or, and_true]

From 76e69e1c8701a01ed3ccfe9d2e5b61e10e25f6f1 Mon Sep 17 00:00:00 2001
From: 8e7 <justsoft.jsoft@gmail.com>
Date: Wed, 15 Apr 2026 10:31:33 +0800
Subject: [PATCH 8/9] minor change: use inferInstanceAs, add symmetric
 starGraph_center_adj'

---
 Mathlib/Combinatorics/SimpleGraph/Acyclic.lean | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index 8caf618b3f2c91..813d671b71208b 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -673,23 +673,26 @@ section Star
 def starGraph (r : V) : SimpleGraph V :=
  .fromRel fun v _ ↦ v = r
 
-instance [DecidableEq V] (r : V) : DecidableRel (starGraph r).Adj := by
-  unfold starGraph; infer_instance
+instance [DecidableEq V] (r : V) : DecidableRel (starGraph r).Adj :=
+  inferInstanceAs (DecidableRel fun x y ↦ x ≠ y ∧ (x = r ∨ y = r))
 
 @[simp]
 lemma starGraph_adj {r x y : V} : (starGraph r).Adj x y ↔ x ≠ y ∧ (x = r ∨ y = r) := by
   simp [starGraph, fromRel]
 
-/-- If v ≠ r, then v is adjacent to r. -/
+/-- If r ≠ v, then v is adjacent to r. -/
 lemma starGraph_center_adj {r v : V} (h : r ≠ v) : (starGraph r).Adj r v :=
   starGraph_adj.mpr ⟨h, Or.inl rfl⟩
 
+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⟩⟩
+  exact connected_iff _ |>.mpr ⟨fun u v ↦ (this u).symm.trans (this v), ⟨r⟩⟩
 
 lemma isAcyclic_starGraph (r : V) : (starGraph r).IsAcyclic := by
   refine isAcyclic_iff_forall_adj_isBridge.mpr fun v w hadj ↦ isBridge_iff.mpr ⟨hadj, ?_⟩

From c1ee37d7923c806e8cb22ec48e005c142a6db515 Mon Sep 17 00:00:00 2001
From: 8e7 <justsoft.jsoft@gmail.com>
Date: Wed, 15 Apr 2026 11:40:06 +0800
Subject: [PATCH 9/9] refactor to StarGraph.lean

---
 Mathlib.lean                                  |  1 +
 .../Combinatorics/SimpleGraph/Acyclic.lean    | 59 ------------
 .../Combinatorics/SimpleGraph/StarGraph.lean  | 91 +++++++++++++++++++
 3 files changed, 92 insertions(+), 59 deletions(-)
 create mode 100644 Mathlib/Combinatorics/SimpleGraph/StarGraph.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 51561e14b0c337..5e5275ffbfc154 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3539,6 +3539,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise
 public import Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
 public import Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma
 public import Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
+public import Mathlib.Combinatorics.SimpleGraph.StarGraph
 public import Mathlib.Combinatorics.SimpleGraph.StronglyRegular
 public import Mathlib.Combinatorics.SimpleGraph.Subgraph
 public import Mathlib.Combinatorics.SimpleGraph.Sum
diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index 813d671b71208b..dc25d0afbcfa1a 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -667,63 +667,4 @@ lemma isAcyclic_iff_pairwise_not_isEdgeReachable_two :
   · refine isAcyclic_iff_forall_adj_isBridge.mpr fun _ _ hadj ↦ ?_
     exact isBridge_iff_adj_and_not_isEdgeConnected_two.mpr ⟨hadj, h hadj.ne⟩
 
-section Star
-
-/-- The star graph on `V` centered at `r`: every non-center vertex is adjacent to `r`. -/
-def starGraph (r : V) : SimpleGraph V :=
- .fromRel fun v _ ↦ v = r
-
-instance [DecidableEq V] (r : V) : DecidableRel (starGraph r).Adj :=
-  inferInstanceAs (DecidableRel fun x y ↦ x ≠ y ∧ (x = r ∨ y = r))
-
-@[simp]
-lemma starGraph_adj {r x y : V} : (starGraph r).Adj x y ↔ x ≠ y ∧ (x = r ∨ y = r) := by
-  simp [starGraph, fromRel]
-
-/-- If r ≠ v, then v is adjacent to r. -/
-lemma starGraph_center_adj {r v : V} (h : r ≠ v) : (starGraph r).Adj r v :=
-  starGraph_adj.mpr ⟨h, Or.inl rfl⟩
-
-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 isAcyclic_starGraph (r : V) : (starGraph r).IsAcyclic := by
-  refine isAcyclic_iff_forall_adj_isBridge.mpr fun v w hadj ↦ isBridge_iff.mpr ⟨hadj, ?_⟩
-  rw [starGraph_adj] at hadj
-  wlog! h : v = r
-  · have hw : w = r := hadj.2.resolve_left h
-    replace hadj : w ≠ v ∧ (w = r ∨ v = r) := ⟨hadj.1.symm, hadj.2.symm⟩
-    rw [reachable_comm, Sym2.eq_swap]
-    exact this r w v hadj hw
-  · subst h
-    apply not_reachable_of_neighborSet_right_eq_empty hadj.1
-    ext x; aesop
-
-/-- A star graph is a tree. -/
-lemma isTree_starGraph (r : V) : (starGraph r).IsTree := by
-  refine ⟨connected_starGraph r, isAcyclic_starGraph r⟩
-
-/-- Every non-center vertex of a starGraph has degree one. -/
-lemma degree_starGraph_of_ne_center [Fintype V] [DecidableEq V] {r v : V} (h : v ≠ r) :
-    (starGraph r).degree v = 1 :=
-  degree_eq_one_iff_existsUnique_adj.mpr ⟨r, by simp [h], by grind [starGraph_adj]⟩
-
-/-- 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
-  rw [degree, neighborFinset_eq_filter (starGraph r)]
-  simp only [starGraph_adj, ne_eq, true_or, and_true]
-  have : ({w | ¬r = w} : Finset V) = Finset.univ.erase r := by
-    ext v; simp [eq_comm]
-  rw [this, Finset.card_erase_of_mem (Finset.mem_univ r), Finset.card_univ]
-
-end Star
-
 end SimpleGraph
diff --git a/Mathlib/Combinatorics/SimpleGraph/StarGraph.lean b/Mathlib/Combinatorics/SimpleGraph/StarGraph.lean
new file mode 100644
index 00000000000000..6c0850c968d85f
--- /dev/null
+++ b/Mathlib/Combinatorics/SimpleGraph/StarGraph.lean
@@ -0,0 +1,91 @@
+/-
+Copyright (c) 2026 Justin Lai. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Justin Lai
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Acyclic
+public import Mathlib.Combinatorics.SimpleGraph.Metric
+
+/-!
+
+# Star Graphs
+
+## Main definitions
+
+* `SimpleGraph.starGraph r` is the star graph on V centered at r. Every non-center vertex is
+  adjacent to r.
+
+## Main statements
+
+* `SimpleGraph.isTree_starGraph` proves the star graph is a tree.
+
+
+## Tags
+
+star graph
+-/
+
+@[expose] public section
+
+namespace SimpleGraph
+
+variable {V V' : Type*} (G : SimpleGraph V) (G' : SimpleGraph V')
+
+/-- The star graph on `V` centered at `r`: every non-center vertex is adjacent to `r`. -/
+def starGraph (r : V) : SimpleGraph V :=
+ .fromRel fun v _ ↦ v = r
+
+instance [DecidableEq V] (r : V) : DecidableRel (starGraph r).Adj :=
+  inferInstanceAs (DecidableRel fun x y ↦ x ≠ y ∧ (x = r ∨ y = r))
+
+@[simp]
+lemma starGraph_adj {r x y : V} : (starGraph r).Adj x y ↔ x ≠ y ∧ (x = r ∨ y = r) := by
+  simp [starGraph, fromRel]
+
+/-- If r ≠ v, then v is adjacent to r. -/
+lemma starGraph_center_adj {r v : V} (h : r ≠ v) : (starGraph r).Adj r v :=
+  starGraph_adj.mpr ⟨h, Or.inl rfl⟩
+
+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 isAcyclic_starGraph (r : V) : (starGraph r).IsAcyclic := by
+  refine isAcyclic_iff_forall_adj_isBridge.mpr fun v w hadj ↦ isBridge_iff.mpr ⟨hadj, ?_⟩
+  rw [starGraph_adj] at hadj
+  wlog! h : v = r
+  · have hw : w = r := hadj.2.resolve_left h
+    replace hadj : w ≠ v ∧ (w = r ∨ v = r) := ⟨hadj.1.symm, hadj.2.symm⟩
+    rw [reachable_comm, Sym2.eq_swap]
+    exact this r w v hadj hw
+  · subst h
+    apply not_reachable_of_neighborSet_right_eq_empty hadj.1
+    ext x; aesop
+
+/-- A star graph is a tree. -/
+lemma isTree_starGraph (r : V) : (starGraph r).IsTree := by
+  refine ⟨connected_starGraph r, isAcyclic_starGraph r⟩
+
+/-- Every non-center vertex of a starGraph has degree one. -/
+lemma degree_starGraph_of_ne_center [Fintype V] [DecidableEq V] {r v : V} (h : v ≠ r) :
+    (starGraph r).degree v = 1 :=
+  degree_eq_one_iff_existsUnique_adj.mpr ⟨r, by simp [h], by grind [starGraph_adj]⟩
+
+/-- 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
+  rw [degree, neighborFinset_eq_filter (starGraph r)]
+  simp only [starGraph_adj, ne_eq, true_or, and_true]
+  have : ({w | ¬r = w} : Finset V) = Finset.univ.erase r := by
+    ext v; simp [eq_comm]
+  rw [this, Finset.card_erase_of_mem (Finset.mem_univ r), Finset.card_univ]
+
+end SimpleGraph