From c6ec473cdf156b0a86f0e69603db036a88b13f41 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Fri, 6 Feb 2026 10:41:08 +0200
Subject: [PATCH 01/36] feat(Data/Sym/Sym2): `fromRel` equivalence with `Sigma`
 over a `Quotient`

---
 Mathlib/Data/Sym/Sym2.lean | 40 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
index 7eae49b65039e5..9446fe0fddde79 100644
--- a/Mathlib/Data/Sym/Sym2.lean
+++ b/Mathlib/Data/Sym/Sym2.lean
@@ -10,6 +10,7 @@ public import Mathlib.Data.Finset.Prod
 public import Mathlib.Data.SetLike.Basic
 public import Mathlib.Data.Sym.Basic
 public import Mathlib.Data.Sym.Sym2.Init
+import Mathlib.Tactic.DepRewrite
 
 /-!
 # The symmetric square
@@ -590,6 +591,11 @@ alias ⟨_, fromRel_mono⟩ := fromRel_mono_iff
 def fromRelOrderEmbedding : { r : α → α → Prop // Symmetric r } ↪o Set (Sym2 α) :=
   OrderEmbedding.ofMapLEIff (fun r ↦ Sym2.fromRel r.prop) fun _ _ ↦ fromRel_mono_iff ..
 
+theorem mem_fromRel_comap {r : β → β → Prop} (sym : Symmetric r) (f : α → β) (z : Sym2 α) :
+    z ∈ fromRel (sym.comap f) ↔ z.map f ∈ fromRel sym := by
+  cases z
+  simp
+
 theorem fromRel_bot : fromRel (fun (_ _ : α) z => z : Symmetric ⊥) = ∅ := by
   apply Set.eq_empty_of_forall_notMem fun e => _
   apply Sym2.ind
@@ -647,6 +653,40 @@ lemma fromRel_relationMap {r : α → α → Prop} (hr : Symmetric r) (f : α 
     forall_exists_index, and_imp]
   exact fun c d hcd hc hd ↦ ⟨d, c, hr hcd, hd, hc⟩
 
+/-- Non-dependent recursor on members of a `fromRel` set -/
+def fromRelNdrec {motive : Sort*} {sym : Symmetric r} (hz : z ∈ fromRel sym)
+    (f : (a b : α) → r a b → motive) (h : ∀ (a b : α) (h : r a b), f a b h = f b a (sym h)) :
+    motive :=
+  z.hrec (fun p ↦ f p.fst p.snd)
+    (fun _ _ ↦ Function.hfunext (sym.iff .. |>.eq) fun _ _ _ ↦ heq_of_eq <| h ..) hz
+
+/-- For a relation homomorphism `r →r r'` where `r` is symmetric, the `fromRel` set of `r` is
+equivalent to summing that set restricted to equivalence classes of `r'` using a `Subtype`,
+`Quot` version -/
+def _root_.Equiv.sigmaQuotFromRel (sym : Symmetric r) {r' : β → β → Prop} (f : r →r r') :
+    fromRel sym ≃ Σ q, fromRel <| sym.comap <| @Subtype.val α ((Quot.mk r' · = q) ∘ f) where
+  toFun z := fromRelNdrec z.prop
+    (fun a b h ↦ ⟨.mk r' <| f a, s(⟨a, rfl⟩, ⟨b, (Quot.sound <| f.map_rel h).symm⟩), h⟩)
+    fun a b h ↦ by
+      dsimp only
+      rw! [Quot.sound <| f.map_rel h, eq_swap]
+      rfl
+  invFun z := ⟨z.snd.val.map Subtype.val, mem_fromRel_comap sym .. |>.mp z.snd.prop⟩
+  left_inv z := by
+    rcases z with ⟨⟨⟩⟩
+    rfl
+  right_inv z := by
+    rcases z with ⟨q, ⟨⟨a, ha⟩, ⟨b, hb⟩⟩, h⟩
+    subst ha
+    rfl
+
+/-- For a relation homomorphism `r →r r'` where `r` is symmetric, the `fromRel` set of `r` is
+equivalent to summing that set restricted to equivalence classes of `r'` using a `Subtype`,
+`Quotient` version -/
+def _root_.Equiv.sigmaQuotientFromRel (sym : Symmetric r) {r' : Setoid β} (f : r →r r') :
+    fromRel sym ≃ Σ q, fromRel <| sym.comap <| @Subtype.val α ((Quotient.mk r' · = q) ∘ f) :=
+  .sigmaQuotFromRel sym f
+
 /-- The inverse to `Sym2.fromRel`. Given a set on `Sym2 α`, give a symmetric relation on `α`
 (see `Sym2.toRel_symmetric`). -/
 def ToRel (s : Set (Sym2 α)) (x y : α) : Prop :=

From 4980ed544eebdc1a31b67e7cd8d90a2def4aa278 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Fri, 6 Feb 2026 11:52:37 +0200
Subject: [PATCH 02/36] feat(Combinatorics/SimpleGraph/Acyclic): a graph is a
 tree iff it's acyclic and has exactly `n - 1` edges

---
 .../Combinatorics/SimpleGraph/Acyclic.lean    | 40 ++++++++++++++++++-
 .../SimpleGraph/Connectivity/Connected.lean   | 11 +++++
 Mathlib/Data/Sym/Sym2.lean                    | 40 +++++++++++++++++++
 Mathlib/Logic/Equiv/Basic.lean                | 14 +++++++
 Mathlib/Order/RelIso/Basic.lean               |  2 +
 5 files changed, 106 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index a9beb9b71f2092..da393d53e65ff2 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Kyle Miller. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kyle Miller
+Authors: Kyle Miller, Snir Broshi
 -/
 module
 
@@ -485,6 +485,44 @@ lemma isTree_iff_connected_and_card [Finite V] :
     ← edgeFinset_card, add_lt_add_iff_right]
   exact Finset.card_lt_card <| by simpa [deleteEdges, edgeFinset]
 
+/-- Every acyclic graph on `n` vertices with `c` connected components has exactly `n - c` edges -/
+lemma IsAcyclic.card_edgeSet_add_card_connectedComponent [Finite V] (h : G.IsAcyclic) :
+    Nat.card G.edgeSet + Nat.card G.ConnectedComponent = Nat.card V := by
+  have := Fintype.ofFinite G.ConnectedComponent
+  rw [Nat.card_congr G.verticesEquivSigmaConnectedComponent, Nat.card_sigma,
+    Nat.card_congr G.edgeSetEquivSigmaConnectedComponent, Nat.card_sigma,
+    ← Fintype.card_eq_nat_card, Fintype.card_eq_sum_ones, ← Finset.sum_add_distrib]
+  congr
+  ext
+  exact (isTree_iff_connected_and_card.mp <| h.isTree_connectedComponent _).right
+
+/-- An acyclic graph on `n` vertices has at most `n - 1` edges -/
+theorem IsAcyclic.card_edgeSet_add_one_le_card_vert [Finite V] [Nonempty V] (h : G.IsAcyclic) :
+    Nat.card G.edgeSet + 1 ≤ Nat.card V := by
+  grind [h.card_edgeSet_add_card_connectedComponent, Nat.card_pos]
+
+/-- A graph on `n` vertices with at least `n` edges is not acyclic -/
+theorem card_vert_le_card_edgeSet_isAcyclic [Finite V] [Nonempty V]
+    (h : Nat.card V ≤ Nat.card G.edgeSet) : ¬G.IsAcyclic := by
+  grind [IsAcyclic.card_edgeSet_add_one_le_card_vert]
+
+/-- A graph on `n` vertices with at least `n` edges has a cycle -/
+theorem card_vert_le_card_edgeSet_exists_isCycle [Finite V] [Nonempty V]
+    (h : Nat.card V ≤ Nat.card G.edgeSet) : ∃ (v : V) (c : G.Walk v v), c.IsCycle := by
+  grind [IsAcyclic, card_vert_le_card_edgeSet_isAcyclic h]
+
+/-- A graph on `n` vertices is a tree iff it is acyclic and has exactly `n - 1` edges -/
+theorem isTree_iff_isAcyclic_and_card_edgeSet_add_one_eq_card [Finite V] :
+    G.IsTree ↔ G.IsAcyclic ∧ Nat.card G.edgeSet + 1 = Nat.card V := by
+  have := Fintype.ofFinite V
+  have := Fintype.ofFinite G.edgeSet
+  refine ⟨fun h ↦ ⟨h.IsAcyclic, by simpa using h.card_edgeFinset⟩, fun ⟨h, _⟩ ↦ ⟨?_, h⟩⟩
+  refine { preconnected a b := ?_, nonempty := by grind [Nat.card_pos_iff] }
+  suffices G.Reachable = ⊤ by simp [this]
+  rw [← G.reachable_is_equivalence.eqvGen_eq]
+  refine Quot.subsingleton_iff _ |>.mp <| Nat.card_eq_one_iff_unique.mp ?_ |>.left
+  grind [h.card_edgeSet_add_card_connectedComponent]
+
 /-- The minimum degree of all vertices in a nontrivial tree is one. -/
 lemma IsTree.minDegree_eq_one_of_nontrivial (h : G.IsTree) [Fintype V] [Nontrivial V]
     [DecidableRel G.Adj] : G.minDegree = 1 := by
diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
index 87e75862e31ff0..de73db9c492606 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
@@ -681,6 +681,17 @@ theorem maximal_connected_induce_iff (s : Set V) :
 
 end ConnectedComponent
 
+variable (G) in
+/-- The vertices of a graph are partitioned among its connected components -/
+def verticesEquivSigmaConnectedComponent : V ≃ Σ (c : G.ConnectedComponent), c :=
+  .sigmaQuot G.Reachable
+
+variable (G) in
+/-- The edges of a graph are partitioned among its connected components -/
+def edgeSetEquivSigmaConnectedComponent :
+    G.edgeSet ≃ Σ (c : G.ConnectedComponent), c.toSimpleGraph.edgeSet :=
+  .sigmaQuotFromRel G.symm <| .ofLE <| fun _ _ ↦ Adj.reachable
+
 /-- Given graph homomorphisms from each connected component of `G` to `H`, this is the graph
 homomorphism from `G` to `H`. -/
 @[simps]
diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
index 7eae49b65039e5..9446fe0fddde79 100644
--- a/Mathlib/Data/Sym/Sym2.lean
+++ b/Mathlib/Data/Sym/Sym2.lean
@@ -10,6 +10,7 @@ public import Mathlib.Data.Finset.Prod
 public import Mathlib.Data.SetLike.Basic
 public import Mathlib.Data.Sym.Basic
 public import Mathlib.Data.Sym.Sym2.Init
+import Mathlib.Tactic.DepRewrite
 
 /-!
 # The symmetric square
@@ -590,6 +591,11 @@ alias ⟨_, fromRel_mono⟩ := fromRel_mono_iff
 def fromRelOrderEmbedding : { r : α → α → Prop // Symmetric r } ↪o Set (Sym2 α) :=
   OrderEmbedding.ofMapLEIff (fun r ↦ Sym2.fromRel r.prop) fun _ _ ↦ fromRel_mono_iff ..
 
+theorem mem_fromRel_comap {r : β → β → Prop} (sym : Symmetric r) (f : α → β) (z : Sym2 α) :
+    z ∈ fromRel (sym.comap f) ↔ z.map f ∈ fromRel sym := by
+  cases z
+  simp
+
 theorem fromRel_bot : fromRel (fun (_ _ : α) z => z : Symmetric ⊥) = ∅ := by
   apply Set.eq_empty_of_forall_notMem fun e => _
   apply Sym2.ind
@@ -647,6 +653,40 @@ lemma fromRel_relationMap {r : α → α → Prop} (hr : Symmetric r) (f : α 
     forall_exists_index, and_imp]
   exact fun c d hcd hc hd ↦ ⟨d, c, hr hcd, hd, hc⟩
 
+/-- Non-dependent recursor on members of a `fromRel` set -/
+def fromRelNdrec {motive : Sort*} {sym : Symmetric r} (hz : z ∈ fromRel sym)
+    (f : (a b : α) → r a b → motive) (h : ∀ (a b : α) (h : r a b), f a b h = f b a (sym h)) :
+    motive :=
+  z.hrec (fun p ↦ f p.fst p.snd)
+    (fun _ _ ↦ Function.hfunext (sym.iff .. |>.eq) fun _ _ _ ↦ heq_of_eq <| h ..) hz
+
+/-- For a relation homomorphism `r →r r'` where `r` is symmetric, the `fromRel` set of `r` is
+equivalent to summing that set restricted to equivalence classes of `r'` using a `Subtype`,
+`Quot` version -/
+def _root_.Equiv.sigmaQuotFromRel (sym : Symmetric r) {r' : β → β → Prop} (f : r →r r') :
+    fromRel sym ≃ Σ q, fromRel <| sym.comap <| @Subtype.val α ((Quot.mk r' · = q) ∘ f) where
+  toFun z := fromRelNdrec z.prop
+    (fun a b h ↦ ⟨.mk r' <| f a, s(⟨a, rfl⟩, ⟨b, (Quot.sound <| f.map_rel h).symm⟩), h⟩)
+    fun a b h ↦ by
+      dsimp only
+      rw! [Quot.sound <| f.map_rel h, eq_swap]
+      rfl
+  invFun z := ⟨z.snd.val.map Subtype.val, mem_fromRel_comap sym .. |>.mp z.snd.prop⟩
+  left_inv z := by
+    rcases z with ⟨⟨⟩⟩
+    rfl
+  right_inv z := by
+    rcases z with ⟨q, ⟨⟨a, ha⟩, ⟨b, hb⟩⟩, h⟩
+    subst ha
+    rfl
+
+/-- For a relation homomorphism `r →r r'` where `r` is symmetric, the `fromRel` set of `r` is
+equivalent to summing that set restricted to equivalence classes of `r'` using a `Subtype`,
+`Quotient` version -/
+def _root_.Equiv.sigmaQuotientFromRel (sym : Symmetric r) {r' : Setoid β} (f : r →r r') :
+    fromRel sym ≃ Σ q, fromRel <| sym.comap <| @Subtype.val α ((Quotient.mk r' · = q) ∘ f) :=
+  .sigmaQuotFromRel sym f
+
 /-- The inverse to `Sym2.fromRel`. Given a set on `Sym2 α`, give a symmetric relation on `α`
 (see `Sym2.toRel_symmetric`). -/
 def ToRel (s : Set (Sym2 α)) (x y : α) : Prop :=
diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean
index c416f19729ae36..da821640c7ac6d 100644
--- a/Mathlib/Logic/Equiv/Basic.lean
+++ b/Mathlib/Logic/Equiv/Basic.lean
@@ -438,6 +438,20 @@ def sigmaSubtype {α : Type*} {β : α → Type*} (a : α) :
   left_inv := fun ⟨a, h⟩ ↦ by cases h; simp
   right_inv b := by simp
 
+/-- A sigma over a quotient summing the equivalence classes is equivalent to the original type,
+`Quot` version -/
+@[simps]
+def sigmaQuot {α : Type*} (r : α → α → Prop) : α ≃ Σ q, { x // Quot.mk r x = q } where
+  toFun x := ⟨.mk r x, x, rfl⟩
+  invFun x := x.snd.val
+  left_inv _ := rfl
+  right_inv x := Sigma.subtype_ext x.snd.prop rfl
+
+/-- A sigma over a quotient summing the equivalence classes is equivalent to the original type,
+`Quotient` version -/
+@[simps!]
+def sigmaQuotient {α : Type*} (r : Setoid α) : α ≃ Σ q, { x // Quotient.mk r x = q } :=
+  .sigmaQuot r
 
 section
 attribute [local simp] Trans.trans sigmaAssoc subtypeSigmaEquiv uniqueSigma eqRec_eq_cast
diff --git a/Mathlib/Order/RelIso/Basic.lean b/Mathlib/Order/RelIso/Basic.lean
index ec8ef02594052b..472ac4cdef6efd 100644
--- a/Mathlib/Order/RelIso/Basic.lean
+++ b/Mathlib/Order/RelIso/Basic.lean
@@ -144,6 +144,8 @@ protected def id (r : α → α → Prop) : r →r r :=
 protected def comp (g : s →r t) (f : r →r s) : r →r t :=
   ⟨fun x => g (f x), fun h => g.2 (f.2 h)⟩
 
+protected def ofLE {r' : α → α → Prop} (le : r ≤ r') : r →r r' := ⟨id, @le⟩
+
 /-- A relation homomorphism is also a relation homomorphism between dual relations. -/
 @[simps]
 protected def swap (f : r →r s) : swap r →r swap s :=

From cf038ba38ca53678c6babc838d9373497e292faa Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Fri, 6 Feb 2026 12:14:01 +0200
Subject: [PATCH 03/36] `RelHom.ofLE` docstring

---
 Mathlib/Order/RelIso/Basic.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Order/RelIso/Basic.lean b/Mathlib/Order/RelIso/Basic.lean
index 472ac4cdef6efd..067abc10915280 100644
--- a/Mathlib/Order/RelIso/Basic.lean
+++ b/Mathlib/Order/RelIso/Basic.lean
@@ -144,6 +144,7 @@ protected def id (r : α → α → Prop) : r →r r :=
 protected def comp (g : s →r t) (f : r →r s) : r →r t :=
   ⟨fun x => g (f x), fun h => g.2 (f.2 h)⟩
 
+/-- The identity relation homomorphism between subrelations -/
 protected def ofLE {r' : α → α → Prop} (le : r ≤ r') : r →r r' := ⟨id, @le⟩
 
 /-- A relation homomorphism is also a relation homomorphism between dual relations. -/

From 68b3331ce93374056e3a1e1c21368e03260de1f2 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 7 Feb 2026 01:08:36 +0200
Subject: [PATCH 04/36] replace `Equiv.sigmaQuot` with `Equiv.sigmaFiberEquiv`
 and tag `simps`

---
 .../SimpleGraph/Connectivity/Connected.lean        |  4 +++-
 Mathlib/Logic/Equiv/Basic.lean                     | 14 --------------
 2 files changed, 3 insertions(+), 15 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
index de73db9c492606..fdfe0d1640bad7 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
@@ -683,11 +683,13 @@ end ConnectedComponent
 
 variable (G) in
 /-- The vertices of a graph are partitioned among its connected components -/
+@[simps!]
 def verticesEquivSigmaConnectedComponent : V ≃ Σ (c : G.ConnectedComponent), c :=
-  .sigmaQuot G.Reachable
+  .symm <| .sigmaFiberEquiv <| Quot.mk G.Reachable
 
 variable (G) in
 /-- The edges of a graph are partitioned among its connected components -/
+@[simps!]
 def edgeSetEquivSigmaConnectedComponent :
     G.edgeSet ≃ Σ (c : G.ConnectedComponent), c.toSimpleGraph.edgeSet :=
   .sigmaQuotFromRel G.symm <| .ofLE <| fun _ _ ↦ Adj.reachable
diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean
index da821640c7ac6d..c416f19729ae36 100644
--- a/Mathlib/Logic/Equiv/Basic.lean
+++ b/Mathlib/Logic/Equiv/Basic.lean
@@ -438,20 +438,6 @@ def sigmaSubtype {α : Type*} {β : α → Type*} (a : α) :
   left_inv := fun ⟨a, h⟩ ↦ by cases h; simp
   right_inv b := by simp
 
-/-- A sigma over a quotient summing the equivalence classes is equivalent to the original type,
-`Quot` version -/
-@[simps]
-def sigmaQuot {α : Type*} (r : α → α → Prop) : α ≃ Σ q, { x // Quot.mk r x = q } where
-  toFun x := ⟨.mk r x, x, rfl⟩
-  invFun x := x.snd.val
-  left_inv _ := rfl
-  right_inv x := Sigma.subtype_ext x.snd.prop rfl
-
-/-- A sigma over a quotient summing the equivalence classes is equivalent to the original type,
-`Quotient` version -/
-@[simps!]
-def sigmaQuotient {α : Type*} (r : Setoid α) : α ≃ Σ q, { x // Quotient.mk r x = q } :=
-  .sigmaQuot r
 
 section
 attribute [local simp] Trans.trans sigmaAssoc subtypeSigmaEquiv uniqueSigma eqRec_eq_cast

From c29bf8bb63b9a30555ee2e9f27f819638eeb1942 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 7 Feb 2026 01:18:34 +0200
Subject: [PATCH 05/36] make the type of `q` explicit in `Sigma` binders

---
 Mathlib/Data/Sym/Sym2.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
index 9446fe0fddde79..4385cabf988976 100644
--- a/Mathlib/Data/Sym/Sym2.lean
+++ b/Mathlib/Data/Sym/Sym2.lean
@@ -664,7 +664,7 @@ def fromRelNdrec {motive : Sort*} {sym : Symmetric r} (hz : z ∈ fromRel sym)
 equivalent to summing that set restricted to equivalence classes of `r'` using a `Subtype`,
 `Quot` version -/
 def _root_.Equiv.sigmaQuotFromRel (sym : Symmetric r) {r' : β → β → Prop} (f : r →r r') :
-    fromRel sym ≃ Σ q, fromRel <| sym.comap <| @Subtype.val α ((Quot.mk r' · = q) ∘ f) where
+    fromRel sym ≃ Σ q : Quot r', fromRel <| sym.comap <| @Subtype.val α ((.mk r' · = q) ∘ f) where
   toFun z := fromRelNdrec z.prop
     (fun a b h ↦ ⟨.mk r' <| f a, s(⟨a, rfl⟩, ⟨b, (Quot.sound <| f.map_rel h).symm⟩), h⟩)
     fun a b h ↦ by
@@ -684,7 +684,7 @@ def _root_.Equiv.sigmaQuotFromRel (sym : Symmetric r) {r' : β → β → Prop}
 equivalent to summing that set restricted to equivalence classes of `r'` using a `Subtype`,
 `Quotient` version -/
 def _root_.Equiv.sigmaQuotientFromRel (sym : Symmetric r) {r' : Setoid β} (f : r →r r') :
-    fromRel sym ≃ Σ q, fromRel <| sym.comap <| @Subtype.val α ((Quotient.mk r' · = q) ∘ f) :=
+    fromRel sym ≃ Σ q : Quotient r', fromRel <| sym.comap <| @Subtype.val α ((⟦·⟧ = q) ∘ f) :=
   .sigmaQuotFromRel sym f
 
 /-- The inverse to `Sym2.fromRel`. Given a set on `Sym2 α`, give a symmetric relation on `α`

From 743718388911b9b23ade9a96571b82d99ab23413 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 7 Feb 2026 01:34:27 +0200
Subject: [PATCH 06/36] replace `subst` with `rfl` in `rcases`

---
 Mathlib/Data/Sym/Sym2.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
index 4385cabf988976..3a94c7a2e4eeb9 100644
--- a/Mathlib/Data/Sym/Sym2.lean
+++ b/Mathlib/Data/Sym/Sym2.lean
@@ -676,8 +676,7 @@ def _root_.Equiv.sigmaQuotFromRel (sym : Symmetric r) {r' : β → β → Prop}
     rcases z with ⟨⟨⟩⟩
     rfl
   right_inv z := by
-    rcases z with ⟨q, ⟨⟨a, ha⟩, ⟨b, hb⟩⟩, h⟩
-    subst ha
+    rcases z with ⟨q, ⟨⟨a, rfl⟩, ⟨b, hb⟩⟩, h⟩
     rfl
 
 /-- For a relation homomorphism `r →r r'` where `r` is symmetric, the `fromRel` set of `r` is

From 9e8cadcfe3d7493118aa86ebc761e56c87c2bc61 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 7 Feb 2026 02:15:49 +0200
Subject: [PATCH 07/36] generalize to fibers

---
 Mathlib/Data/Sym/Sym2.lean | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
index 3a94c7a2e4eeb9..deb6e51a349171 100644
--- a/Mathlib/Data/Sym/Sym2.lean
+++ b/Mathlib/Data/Sym/Sym2.lean
@@ -660,16 +660,15 @@ def fromRelNdrec {motive : Sort*} {sym : Symmetric r} (hz : z ∈ fromRel sym)
   z.hrec (fun p ↦ f p.fst p.snd)
     (fun _ _ ↦ Function.hfunext (sym.iff .. |>.eq) fun _ _ _ ↦ heq_of_eq <| h ..) hz
 
-/-- For a relation homomorphism `r →r r'` where `r` is symmetric, the `fromRel` set of `r` is
-equivalent to summing that set restricted to equivalence classes of `r'` using a `Subtype`,
-`Quot` version -/
-def _root_.Equiv.sigmaQuotFromRel (sym : Symmetric r) {r' : β → β → Prop} (f : r →r r') :
-    fromRel sym ≃ Σ q : Quot r', fromRel <| sym.comap <| @Subtype.val α ((.mk r' · = q) ∘ f) where
+/-- The `fromRel` set of a symmetric relation `r` is equivalent to summing that set restricted to
+fibers of `f` -/
+def _root_.Equiv.sigmaFiberFromRel (sym : Symmetric r) {f : α → β} (hf : r ≤ Setoid.ker f) :
+    fromRel sym ≃ Σ b : β, fromRel <| sym.comap <| @Subtype.val α (f · = b) where
   toFun z := fromRelNdrec z.prop
-    (fun a b h ↦ ⟨.mk r' <| f a, s(⟨a, rfl⟩, ⟨b, (Quot.sound <| f.map_rel h).symm⟩), h⟩)
+    (fun a b h ↦ ⟨f a, s(⟨a, rfl⟩, ⟨b, (hf _ _ h).symm⟩), h⟩)
     fun a b h ↦ by
       dsimp only
-      rw! [Quot.sound <| f.map_rel h, eq_swap]
+      rw! [hf _ _ h, eq_swap]
       rfl
   invFun z := ⟨z.snd.val.map Subtype.val, mem_fromRel_comap sym .. |>.mp z.snd.prop⟩
   left_inv z := by
@@ -679,6 +678,13 @@ def _root_.Equiv.sigmaQuotFromRel (sym : Symmetric r) {r' : β → β → Prop}
     rcases z with ⟨q, ⟨⟨a, rfl⟩, ⟨b, hb⟩⟩, h⟩
     rfl
 
+/-- For a relation homomorphism `r →r r'` where `r` is symmetric, the `fromRel` set of `r` is
+equivalent to summing that set restricted to equivalence classes of `r'` using a `Subtype`,
+`Quot` version -/
+def _root_.Equiv.sigmaQuotFromRel (sym : Symmetric r) {r' : β → β → Prop} (f : r →r r') :
+    fromRel sym ≃ Σ q : Quot r', fromRel <| sym.comap <| @Subtype.val α ((.mk r' · = q) ∘ f) :=
+  .sigmaFiberFromRel sym fun _ _ h ↦ Quot.sound <| f.map_rel h
+
 /-- For a relation homomorphism `r →r r'` where `r` is symmetric, the `fromRel` set of `r` is
 equivalent to summing that set restricted to equivalence classes of `r'` using a `Subtype`,
 `Quotient` version -/

From 353130b18c7428b6947327c863ef670a457bdb36 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 7 Feb 2026 02:17:38 +0200
Subject: [PATCH 08/36] no need to \comp in the quotients version because we
 got rid of the parentheses

---
 Mathlib/Data/Sym/Sym2.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
index deb6e51a349171..ac622318d0c4ce 100644
--- a/Mathlib/Data/Sym/Sym2.lean
+++ b/Mathlib/Data/Sym/Sym2.lean
@@ -689,7 +689,7 @@ def _root_.Equiv.sigmaQuotFromRel (sym : Symmetric r) {r' : β → β → Prop}
 equivalent to summing that set restricted to equivalence classes of `r'` using a `Subtype`,
 `Quotient` version -/
 def _root_.Equiv.sigmaQuotientFromRel (sym : Symmetric r) {r' : Setoid β} (f : r →r r') :
-    fromRel sym ≃ Σ q : Quotient r', fromRel <| sym.comap <| @Subtype.val α ((⟦·⟧ = q) ∘ f) :=
+    fromRel sym ≃ Σ q : Quotient r', fromRel <| sym.comap <| @Subtype.val α (⟦f ·⟧ = q) :=
   .sigmaQuotFromRel sym f
 
 /-- The inverse to `Sym2.fromRel`. Given a set on `Sym2 α`, give a symmetric relation on `α`

From 294e917a6c8c304f6dfec75a5e3b197290594210 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 7 Feb 2026 02:20:51 +0200
Subject: [PATCH 09/36] improve `Symmetric.comap` + `Subtype.val` spelling

---
 Mathlib/Data/Sym/Sym2.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
index ac622318d0c4ce..2b30796aa5d8d8 100644
--- a/Mathlib/Data/Sym/Sym2.lean
+++ b/Mathlib/Data/Sym/Sym2.lean
@@ -663,7 +663,7 @@ def fromRelNdrec {motive : Sort*} {sym : Symmetric r} (hz : z ∈ fromRel sym)
 /-- The `fromRel` set of a symmetric relation `r` is equivalent to summing that set restricted to
 fibers of `f` -/
 def _root_.Equiv.sigmaFiberFromRel (sym : Symmetric r) {f : α → β} (hf : r ≤ Setoid.ker f) :
-    fromRel sym ≃ Σ b : β, fromRel <| sym.comap <| @Subtype.val α (f · = b) where
+    fromRel sym ≃ Σ b : β, fromRel (α := { x // f x = b }) <| sym.comap (↑) where
   toFun z := fromRelNdrec z.prop
     (fun a b h ↦ ⟨f a, s(⟨a, rfl⟩, ⟨b, (hf _ _ h).symm⟩), h⟩)
     fun a b h ↦ by
@@ -682,14 +682,14 @@ def _root_.Equiv.sigmaFiberFromRel (sym : Symmetric r) {f : α → β} (hf : r 
 equivalent to summing that set restricted to equivalence classes of `r'` using a `Subtype`,
 `Quot` version -/
 def _root_.Equiv.sigmaQuotFromRel (sym : Symmetric r) {r' : β → β → Prop} (f : r →r r') :
-    fromRel sym ≃ Σ q : Quot r', fromRel <| sym.comap <| @Subtype.val α ((.mk r' · = q) ∘ f) :=
+    fromRel sym ≃ Σ q : Quot r', fromRel (α := { x // .mk r' (f x) = q }) <| sym.comap (↑) :=
   .sigmaFiberFromRel sym fun _ _ h ↦ Quot.sound <| f.map_rel h
 
 /-- For a relation homomorphism `r →r r'` where `r` is symmetric, the `fromRel` set of `r` is
 equivalent to summing that set restricted to equivalence classes of `r'` using a `Subtype`,
 `Quotient` version -/
 def _root_.Equiv.sigmaQuotientFromRel (sym : Symmetric r) {r' : Setoid β} (f : r →r r') :
-    fromRel sym ≃ Σ q : Quotient r', fromRel <| sym.comap <| @Subtype.val α (⟦f ·⟧ = q) :=
+    fromRel sym ≃ Σ q : Quotient r', fromRel (α := { x // ⟦f x⟧ = q }) <| sym.comap (↑) :=
   .sigmaQuotFromRel sym f
 
 /-- The inverse to `Sym2.fromRel`. Given a set on `Sym2 α`, give a symmetric relation on `α`

From e1df04b0b995068d1b5fad33e4d429ecbee3e5b8 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 7 Feb 2026 02:56:07 +0200
Subject: [PATCH 10/36] cosmetic changes

---
 Mathlib/Data/Sym/Sym2.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
index 2b30796aa5d8d8..ee9283d3374c4b 100644
--- a/Mathlib/Data/Sym/Sym2.lean
+++ b/Mathlib/Data/Sym/Sym2.lean
@@ -663,19 +663,19 @@ def fromRelNdrec {motive : Sort*} {sym : Symmetric r} (hz : z ∈ fromRel sym)
 /-- The `fromRel` set of a symmetric relation `r` is equivalent to summing that set restricted to
 fibers of `f` -/
 def _root_.Equiv.sigmaFiberFromRel (sym : Symmetric r) {f : α → β} (hf : r ≤ Setoid.ker f) :
-    fromRel sym ≃ Σ b : β, fromRel (α := { x // f x = b }) <| sym.comap (↑) where
+    fromRel sym ≃ Σ b : β, fromRel (α := { a // f a = b }) <| sym.comap (↑) where
   toFun z := fromRelNdrec z.prop
-    (fun a b h ↦ ⟨f a, s(⟨a, rfl⟩, ⟨b, (hf _ _ h).symm⟩), h⟩)
-    fun a b h ↦ by
+    (fun a₁ a₂ h ↦ ⟨f a₁, s(⟨a₁, rfl⟩, ⟨a₂, hf a₁ a₂ h |>.symm⟩), h⟩)
+    fun a₁ a₂ h ↦ by
       dsimp only
-      rw! [hf _ _ h, eq_swap]
+      rw! [hf a₁ a₂ h, eq_swap]
       rfl
   invFun z := ⟨z.snd.val.map Subtype.val, mem_fromRel_comap sym .. |>.mp z.snd.prop⟩
   left_inv z := by
-    rcases z with ⟨⟨⟩⟩
+    rcases z with ⟨⟨a₁, a₂⟩, h⟩
     rfl
   right_inv z := by
-    rcases z with ⟨q, ⟨⟨a, rfl⟩, ⟨b, hb⟩⟩, h⟩
+    rcases z with ⟨b, ⟨⟨a₁, rfl⟩, ⟨a₂, ha₂⟩⟩, h⟩
     rfl
 
 /-- For a relation homomorphism `r →r r'` where `r` is symmetric, the `fromRel` set of `r` is

From 7c870cfa547cba64b8e2ed11d419479150141a57 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 14 Feb 2026 03:11:17 +0200
Subject: [PATCH 11/36] fix merge

---
 Mathlib/Data/Sym/Sym2.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
index d8a021f7deb45c..3c1646d80aa51a 100644
--- a/Mathlib/Data/Sym/Sym2.lean
+++ b/Mathlib/Data/Sym/Sym2.lean
@@ -10,7 +10,6 @@ public import Mathlib.Data.Finset.Prod
 public import Mathlib.Data.SetLike.Basic
 public import Mathlib.Data.Sym.Basic
 public import Mathlib.Data.Sym.Sym2.Init
-import Mathlib.Tactic.DepRewrite
 
 /-!
 # The symmetric square

From 1b2c614ba2fd02f410c3c13744f092c162755206 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 14 Feb 2026 04:28:49 +0200
Subject: [PATCH 12/36] =?UTF-8?q?"every"=20=E2=86=92=20"an"?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 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 0df6c0ce63cd14..524dc9807db45e 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -509,7 +509,7 @@ lemma isTree_iff_connected_and_card [Finite V] :
     ← edgeFinset_card, add_lt_add_iff_right]
   exact Finset.card_lt_card <| by simpa [deleteEdges, edgeFinset]
 
-/-- Every acyclic graph on `n` vertices with `c` connected components has exactly `n - c` edges -/
+/-- An acyclic graph on `n` vertices with `c` connected components has exactly `n - c` edges -/
 lemma IsAcyclic.card_edgeSet_add_card_connectedComponent [Finite V] (h : G.IsAcyclic) :
     Nat.card G.edgeSet + Nat.card G.ConnectedComponent = Nat.card V := by
   have := Fintype.ofFinite G.ConnectedComponent

From 26389a6fbcaddc017a8ac390cfb3d4d059046485 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 14 Feb 2026 04:30:41 +0200
Subject: [PATCH 13/36] remove redundant `<|`

---
 Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
index fdfe0d1640bad7..5708fc7d8cd134 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
@@ -692,7 +692,7 @@ variable (G) in
 @[simps!]
 def edgeSetEquivSigmaConnectedComponent :
     G.edgeSet ≃ Σ (c : G.ConnectedComponent), c.toSimpleGraph.edgeSet :=
-  .sigmaQuotFromRel G.symm <| .ofLE <| fun _ _ ↦ Adj.reachable
+  .sigmaQuotFromRel G.symm <| .ofLE fun _ _ ↦ Adj.reachable
 
 /-- Given graph homomorphisms from each connected component of `G` to `H`, this is the graph
 homomorphism from `G` to `H`. -/

From 87bad13dea47dd6ba5000d925dd3d36cf87fbc8a Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Mon, 16 Feb 2026 21:29:01 +0200
Subject: [PATCH 14/36] fix after the signature of `Sym2.hrec` changed in
 master

---
 Mathlib/Data/Sym/Sym2.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
index f02cabad66fda1..0811dfec8ceb22 100644
--- a/Mathlib/Data/Sym/Sym2.lean
+++ b/Mathlib/Data/Sym/Sym2.lean
@@ -673,8 +673,7 @@ lemma fromRel_relationMap {r : α → α → Prop} (hr : Symmetric r) (f : α 
 def fromRelNdrec {motive : Sort*} {sym : Symmetric r} (hz : z ∈ fromRel sym)
     (f : (a b : α) → r a b → motive) (h : ∀ (a b : α) (h : r a b), f a b h = f b a (sym h)) :
     motive :=
-  z.hrec (fun p ↦ f p.fst p.snd)
-    (fun _ _ ↦ Function.hfunext (sym.iff .. |>.eq) fun _ _ _ ↦ heq_of_eq <| h ..) hz
+  z.hrec f (fun _ _ ↦ Function.hfunext (sym.iff .. |>.eq) fun _ _ _ ↦ heq_of_eq <| h ..) hz
 
 /-- The `fromRel` set of a symmetric relation `r` is equivalent to summing that set restricted to
 fibers of `f` -/

From eee507f60cdf751dede8d77a8e7b70d8c220b203 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Mon, 2 Mar 2026 09:21:35 +0200
Subject: [PATCH 15/36] fix because `grind` broke somehow

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

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index b83133aa45cb68..e5d6aeb023091a 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -508,7 +508,9 @@ theorem IsAcyclic.card_edgeSet_add_one_le_card_vert [Finite V] [Nonempty V] (h :
 /-- A graph on `n` vertices with at least `n` edges is not acyclic -/
 theorem card_vert_le_card_edgeSet_isAcyclic [Finite V] [Nonempty V]
     (h : Nat.card V ≤ Nat.card G.edgeSet) : ¬G.IsAcyclic := by
-  grind [IsAcyclic.card_edgeSet_add_one_le_card_vert]
+  intro h
+  have := h.card_edgeSet_add_one_le_card_vert
+  lia
 
 /-- A graph on `n` vertices with at least `n` edges has a cycle -/
 theorem card_vert_le_card_edgeSet_exists_isCycle [Finite V] [Nonempty V]

From 32ebd1aaa1c8cd7c98aa458e23c17b6602d418e8 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Mon, 2 Mar 2026 09:26:22 +0200
Subject: [PATCH 16/36] might as well

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

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index e5d6aeb023091a..3118e81b651031 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -507,10 +507,8 @@ theorem IsAcyclic.card_edgeSet_add_one_le_card_vert [Finite V] [Nonempty V] (h :
 
 /-- A graph on `n` vertices with at least `n` edges is not acyclic -/
 theorem card_vert_le_card_edgeSet_isAcyclic [Finite V] [Nonempty V]
-    (h : Nat.card V ≤ Nat.card G.edgeSet) : ¬G.IsAcyclic := by
-  intro h
-  have := h.card_edgeSet_add_one_le_card_vert
-  lia
+    (h : Nat.card V ≤ Nat.card G.edgeSet) : ¬G.IsAcyclic :=
+  (Nat.not_le_of_lt ·.card_edgeSet_add_one_le_card_vert h)
 
 /-- A graph on `n` vertices with at least `n` edges has a cycle -/
 theorem card_vert_le_card_edgeSet_exists_isCycle [Finite V] [Nonempty V]

From be182cb1af054374877223bb17d30a30e335c98d Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 21 Mar 2026 01:49:07 +0200
Subject: [PATCH 17/36] `IsTree.IsAcyclic` is deprecated

---
 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 e082696cfa8637..6f2f008513c4cc 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -528,7 +528,7 @@ theorem isTree_iff_isAcyclic_and_card_edgeSet_add_one_eq_card [Finite V] :
     G.IsTree ↔ G.IsAcyclic ∧ Nat.card G.edgeSet + 1 = Nat.card V := by
   have := Fintype.ofFinite V
   have := Fintype.ofFinite G.edgeSet
-  refine ⟨fun h ↦ ⟨h.IsAcyclic, by simpa using h.card_edgeFinset⟩, fun ⟨h, _⟩ ↦ ⟨?_, h⟩⟩
+  refine ⟨fun h ↦ ⟨h.isAcyclic, by simpa using h.card_edgeFinset⟩, fun ⟨h, _⟩ ↦ ⟨?_, h⟩⟩
   refine { preconnected a b := ?_, nonempty := by grind [Nat.card_pos_iff] }
   suffices G.Reachable = ⊤ by simp [this]
   rw [← G.reachable_is_equivalence.eqvGen_eq]

From c277057d7be4985deb727ee8c2ebaebd992a06fc Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Thu, 16 Apr 2026 18:28:13 +0300
Subject: [PATCH 18/36] use `fromRelNdrec` in bipartite graphs, see comment:

https://github.com/leanprover-community/mathlib4/pull/34315#discussion_r2773069054
---
 Mathlib/Combinatorics/SimpleGraph/Bipartite.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Bipartite.lean b/Mathlib/Combinatorics/SimpleGraph/Bipartite.lean
index b85d785a27d8f2..128effc7769131 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Bipartite.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Bipartite.lean
@@ -477,13 +477,13 @@ theorem encard_edgeSet_completeBipartiteGraph :
 def IsBipartiteWith.edgeSetEmbeddingCompleteBipartiteGraph [DecidableRel (· ∈ · : V → Set V → _)]
     (hG : G.IsBipartiteWith s t) : G.edgeSet ↪ (completeBipartiteGraph s t).edgeSet where
   toFun := fun ⟨e, he⟩ ↦
-    e.hrec (fun u v h ↦ hG.mem_of_adj h |>.by_cases
+    e.fromRelNdrec he (sym := G.symm) (fun u v h ↦ hG.mem_of_adj h |>.by_cases
       (fun h ↦ ⟨s(.inl ⟨u, h.left⟩, .inr ⟨v, h.right⟩), .inl ⟨rfl, rfl⟩⟩)
       (fun h ↦ ⟨s(.inl ⟨v, h.right⟩, .inr ⟨u, h.left⟩), .inl ⟨rfl, rfl⟩⟩)
-    ) (fun _ _ ↦ Function.hfunext (by grind) <| by grind [Or.by_cases, hG.disjoint]) he
+    ) <| by grind [Or.by_cases, hG.disjoint]
   inj' := by
     rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
-    change (if _ : _ then _ else _) = (if _ : _ then _ else _) → _
+    change (dite ..) = (dite ..) → _
     grind
 
 end completeBipartiteGraph

From f02f013404889046d757e5f158b515eb1d629246 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Wed, 29 Apr 2026 04:03:27 +0300
Subject: [PATCH 19/36] make `z` explicit to avoid hidden pretty-prints

---
 Mathlib/Data/Sym/Sym2.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
index 18c609ceed237b..caa3bd3e0b5abe 100644
--- a/Mathlib/Data/Sym/Sym2.lean
+++ b/Mathlib/Data/Sym/Sym2.lean
@@ -665,7 +665,7 @@ lemma fromRel_relationMap {r : α → α → Prop} (hr : Symmetric r) (f : α 
   exact fun c d hcd hc hd ↦ ⟨d, c, hr hcd, hd, hc⟩
 
 /-- Non-dependent recursor on members of a `fromRel` set -/
-def fromRelNdrec {motive : Sort*} {sym : Symmetric r} (hz : z ∈ fromRel sym)
+def fromRelNdrec {motive : Sort*} {sym : Symmetric r} (z : Sym2 α) (hz : z ∈ fromRel sym)
     (f : (a b : α) → r a b → motive) (h : ∀ (a b : α) (h : r a b), f a b h = f b a (sym h)) :
     motive :=
   z.hrec f (fun _ _ ↦ Function.hfunext (sym.iff .. |>.eq) fun _ _ _ ↦ heq_of_eq <| h ..) hz
@@ -674,7 +674,7 @@ def fromRelNdrec {motive : Sort*} {sym : Symmetric r} (hz : z ∈ fromRel sym)
 fibers of `f` -/
 def _root_.Equiv.sigmaFiberFromRel (sym : Symmetric r) {f : α → β} (hf : r ≤ Setoid.ker f) :
     fromRel sym ≃ Σ b : β, fromRel (α := { a // f a = b }) <| sym.comap (↑) where
-  toFun z := fromRelNdrec z.prop
+  toFun z := z.val.fromRelNdrec z.prop
     (fun a₁ a₂ h ↦ ⟨f a₁, s(⟨a₁, rfl⟩, ⟨a₂, hf a₁ a₂ h |>.symm⟩), h⟩)
     fun a₁ a₂ h ↦ by
       dsimp only

From b57791db4fa45dcb5fd67ebe772516c95332f49e Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Wed, 29 Apr 2026 04:04:13 +0300
Subject: [PATCH 20/36] add simp lemmas, changed `sigmaQuotientFromRel` proof
 to avoid `Quot` showing up in the `simps!`-generated lemmas

---
 Mathlib/Data/Sym/Sym2.lean | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
index caa3bd3e0b5abe..7c45f527c43e2c 100644
--- a/Mathlib/Data/Sym/Sym2.lean
+++ b/Mathlib/Data/Sym/Sym2.lean
@@ -670,8 +670,15 @@ def fromRelNdrec {motive : Sort*} {sym : Symmetric r} (z : Sym2 α) (hz : z ∈
     motive :=
   z.hrec f (fun _ _ ↦ Function.hfunext (sym.iff .. |>.eq) fun _ _ _ ↦ heq_of_eq <| h ..) hz
 
+@[simp]
+theorem fromRelNdrec_mk {motive : Sort*} {sym : Symmetric r} {a b : α} (hz : r a b)
+    (f : (a b : α) → r a b → motive) (h : ∀ (a b : α) (h : r a b), f a b h = f b a (sym h)) :
+    fromRelNdrec s(a, b) hz f h = f a b hz :=
+  rfl
+
 /-- The `fromRel` set of a symmetric relation `r` is equivalent to summing that set restricted to
 fibers of `f` -/
+@[simps]
 def _root_.Equiv.sigmaFiberFromRel (sym : Symmetric r) {f : α → β} (hf : r ≤ Setoid.ker f) :
     fromRel sym ≃ Σ b : β, fromRel (α := { a // f a = b }) <| sym.comap (↑) where
   toFun z := z.val.fromRelNdrec z.prop
@@ -691,6 +698,7 @@ def _root_.Equiv.sigmaFiberFromRel (sym : Symmetric r) {f : α → β} (hf : r 
 /-- For a relation homomorphism `r →r r'` where `r` is symmetric, the `fromRel` set of `r` is
 equivalent to summing that set restricted to equivalence classes of `r'` using a `Subtype`,
 `Quot` version -/
+@[simps!]
 def _root_.Equiv.sigmaQuotFromRel (sym : Symmetric r) {r' : β → β → Prop} (f : r →r r') :
     fromRel sym ≃ Σ q : Quot r', fromRel (α := { x // .mk r' (f x) = q }) <| sym.comap (↑) :=
   .sigmaFiberFromRel sym fun _ _ h ↦ Quot.sound <| f.map_rel h
@@ -698,9 +706,10 @@ def _root_.Equiv.sigmaQuotFromRel (sym : Symmetric r) {r' : β → β → Prop}
 /-- For a relation homomorphism `r →r r'` where `r` is symmetric, the `fromRel` set of `r` is
 equivalent to summing that set restricted to equivalence classes of `r'` using a `Subtype`,
 `Quotient` version -/
+@[simps!]
 def _root_.Equiv.sigmaQuotientFromRel (sym : Symmetric r) {r' : Setoid β} (f : r →r r') :
     fromRel sym ≃ Σ q : Quotient r', fromRel (α := { x // ⟦f x⟧ = q }) <| sym.comap (↑) :=
-  .sigmaQuotFromRel sym f
+  .sigmaFiberFromRel sym fun _ _ h ↦ Quotient.sound <| f.map_rel h
 
 /-- The inverse to `Sym2.fromRel`. Given a set on `Sym2 α`, give a symmetric relation on `α`
 (see `Sym2.toRel_symmetric`). -/

From fa03e4b51557d55a4d152becf4137db864b4767d Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Thu, 30 Apr 2026 20:50:53 +0300
Subject: [PATCH 21/36] update docstring of `sigmaFiberFromRel`

Add equivalence for fromRel set of symmetric relations.
---
 Mathlib/Data/Sym/Sym2.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
index 7c45f527c43e2c..6864bb064518ff 100644
--- a/Mathlib/Data/Sym/Sym2.lean
+++ b/Mathlib/Data/Sym/Sym2.lean
@@ -677,7 +677,7 @@ theorem fromRelNdrec_mk {motive : Sort*} {sym : Symmetric r} {a b : α} (hz : r
   rfl
 
 /-- The `fromRel` set of a symmetric relation `r` is equivalent to summing that set restricted to
-fibers of `f` -/
+fibers of a function `f`, given that `f` agrees on elements related by `r`. -/
 @[simps]
 def _root_.Equiv.sigmaFiberFromRel (sym : Symmetric r) {f : α → β} (hf : r ≤ Setoid.ker f) :
     fromRel sym ≃ Σ b : β, fromRel (α := { a // f a = b }) <| sym.comap (↑) where

From 9bc5dd654852cfa8e1665200549853068f270816 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Tue, 2 Jun 2026 07:13:49 +0300
Subject: [PATCH 22/36] `dsimp` is now redundant

---
 Mathlib/Data/Sym/Sym2.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
index 4b0530f4223ca2..9c73ce812ac32a 100644
--- a/Mathlib/Data/Sym/Sym2.lean
+++ b/Mathlib/Data/Sym/Sym2.lean
@@ -675,10 +675,9 @@ def _root_.Equiv.sigmaFiberFromRel (sym : Symmetric r) {f : α → β} (hf : r 
   toFun z := z.val.fromRelNdrec z.prop
     (fun a₁ a₂ h ↦ ⟨f a₁, s(⟨a₁, rfl⟩, ⟨a₂, hf a₁ a₂ h |>.symm⟩), h⟩)
     fun a₁ a₂ h ↦ by
-      dsimp only
       rw! [hf a₁ a₂ h, eq_swap]
       rfl
-  invFun z := ⟨z.snd.val.map Subtype.val, mem_fromRel_comap sym .. |>.mp z.snd.prop⟩
+  invFun z := ⟨z.snd.val.map (↑), mem_fromRel_comap sym .. |>.mp z.snd.prop⟩
   left_inv z := by
     rcases z with ⟨⟨a₁, a₂⟩, h⟩
     rfl

From 9e3daecaf36b17495b70ff75350706fc21223dad Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Tue, 2 Jun 2026 07:30:56 +0300
Subject: [PATCH 23/36] strange fixes

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

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index 77d20461b6eee2..aed88f4797fa50 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -550,12 +550,12 @@ theorem isTree_iff_isAcyclic_and_card_edgeSet_add_one_eq_card [Finite V] :
     G.IsTree ↔ G.IsAcyclic ∧ Nat.card G.edgeSet + 1 = Nat.card V := by
   have := Fintype.ofFinite V
   have := Fintype.ofFinite G.edgeSet
-  refine ⟨fun h ↦ ⟨h.isAcyclic, by simpa using h.card_edgeFinset⟩, fun ⟨h, _⟩ ↦ ⟨?_, h⟩⟩
-  refine { preconnected a b := ?_, nonempty := by grind [Nat.card_pos_iff] }
+  refine ⟨fun h ↦ ⟨h.isAcyclic, by simpa [edgeFinset] using h.card_edgeFinset⟩, ?_⟩
+  refine fun ⟨h, _⟩ ↦ ⟨{ preconnected a b := ?_, nonempty := by grind [Nat.card_pos_iff] }, h⟩
   suffices G.Reachable = ⊤ by simp [this]
   rw [← G.reachable_is_equivalence.eqvGen_eq]
   refine Quot.subsingleton_iff _ |>.mp <| Nat.card_eq_one_iff_unique.mp ?_ |>.left
-  grind [h.card_edgeSet_add_card_connectedComponent]
+  grind [h.card_edgeSet_add_card_connectedComponent, ConnectedComponent]
 
 /-- The minimum degree of all vertices in a nontrivial tree is one. -/
 lemma IsTree.minDegree_eq_one_of_nontrivial (h : G.IsTree) [Fintype V] [Nontrivial V]

From 5c983604213a593af065012fcfb054da453cbb7f Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Mon, 15 Jun 2026 16:56:13 +0300
Subject: [PATCH 24/36] `Nat.card G.edgeSet` -> `G.edgeSet.ncard`

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

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index 7e1d7d4c926811..fd0ff9372680b8 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -513,10 +513,10 @@ lemma isTree_iff_connected_and_card [Finite V] :
   exact Finset.card_lt_card <| by simpa [deleteEdges, edgeFinset]
 
 /-- An acyclic graph on `n` vertices with `c` connected components has exactly `n - c` edges -/
-lemma IsAcyclic.card_edgeSet_add_card_connectedComponent [Finite V] (h : G.IsAcyclic) :
-    Nat.card G.edgeSet + Nat.card G.ConnectedComponent = Nat.card V := by
+theorem IsAcyclic.card_edgeSet_add_card_connectedComponent [Finite V] (h : G.IsAcyclic) :
+    G.edgeSet.ncard + Nat.card G.ConnectedComponent = Nat.card V := by
   have := Fintype.ofFinite G.ConnectedComponent
-  rw [Nat.card_congr G.verticesEquivSigmaConnectedComponent, Nat.card_sigma,
+  rw [Nat.card_congr G.verticesEquivSigmaConnectedComponent, Nat.card_sigma, ← Nat.card_coe_set_eq,
     Nat.card_congr G.edgeSetEquivSigmaConnectedComponent, Nat.card_sigma,
     ← Fintype.card_eq_nat_card, Fintype.card_eq_sum_ones, ← Finset.sum_add_distrib]
   congr
@@ -525,22 +525,22 @@ lemma IsAcyclic.card_edgeSet_add_card_connectedComponent [Finite V] (h : G.IsAcy
 
 /-- An acyclic graph on `n` vertices has at most `n - 1` edges -/
 theorem IsAcyclic.card_edgeSet_add_one_le_card_vert [Finite V] [Nonempty V] (h : G.IsAcyclic) :
-    Nat.card G.edgeSet + 1 ≤ Nat.card V := by
+    G.edgeSet.ncard + 1 ≤ Nat.card V := by
   grind [h.card_edgeSet_add_card_connectedComponent, Nat.card_pos]
 
 /-- A graph on `n` vertices with at least `n` edges is not acyclic -/
 theorem card_vert_le_card_edgeSet_isAcyclic [Finite V] [Nonempty V]
-    (h : Nat.card V ≤ Nat.card G.edgeSet) : ¬G.IsAcyclic :=
+    (h : Nat.card V ≤ G.edgeSet.ncard) : ¬G.IsAcyclic :=
   (Nat.not_le_of_lt ·.card_edgeSet_add_one_le_card_vert h)
 
 /-- A graph on `n` vertices with at least `n` edges has a cycle -/
 theorem card_vert_le_card_edgeSet_exists_isCycle [Finite V] [Nonempty V]
-    (h : Nat.card V ≤ Nat.card G.edgeSet) : ∃ (v : V) (c : G.Walk v v), c.IsCycle := by
+    (h : Nat.card V ≤ G.edgeSet.ncard) : ∃ (v : V) (c : G.Walk v v), c.IsCycle := by
   grind [IsAcyclic, card_vert_le_card_edgeSet_isAcyclic h]
 
 /-- A graph on `n` vertices is a tree iff it is acyclic and has exactly `n - 1` edges -/
 theorem isTree_iff_isAcyclic_and_card_edgeSet_add_one_eq_card [Finite V] :
-    G.IsTree ↔ G.IsAcyclic ∧ Nat.card G.edgeSet + 1 = Nat.card V := by
+    G.IsTree ↔ G.IsAcyclic ∧ G.edgeSet.ncard + 1 = Nat.card V := by
   have := Fintype.ofFinite V
   have := Fintype.ofFinite G.edgeSet
   refine ⟨fun h ↦ ⟨h.isAcyclic, by simpa [edgeFinset] using h.card_edgeFinset⟩, ?_⟩

From 2ebd30d4748f674451a32d52245ffa34f8d760c9 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Mon, 15 Jun 2026 20:25:04 +0300
Subject: [PATCH 25/36] `G.edgeSet.ncard + 1 = Nat.card V` in a finite tree

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

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index fd0ff9372680b8..4d771cd75139ac 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -488,6 +488,12 @@ lemma Connected.exists_isTree_le (h : G.Connected) : ∃ T ≤ G, IsTree T := by
   obtain ⟨F, hF⟩ := G.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic bot_le isAcyclic_bot
   grind [IsTree, Connected, preconnected_iff_reachable_eq_top]
 
+theorem connected_iff_natCard_connectedComponent_eq_one :
+    G.Connected ↔ Nat.card G.ConnectedComponent = 1 := by
+  have : G.ConnectedComponent = Quotient G.reachableSetoid := rfl
+  simp_rw [connected_iff, preconnected_iff_reachable_eq_top, Nat.card_eq_one_iff_unique, this,
+    nonempty_quotient_iff, Quotient.subsingleton_iff, reachableSetoid, Setoid.mk_eq_top]
+
 /-- Every connected graph on `n` vertices has at least `n-1` edges. -/
 lemma Connected.card_vert_le_card_edgeSet_add_one (h : G.Connected) :
     Nat.card V ≤ Nat.card G.edgeSet + 1 := by
@@ -528,6 +534,10 @@ theorem IsAcyclic.card_edgeSet_add_one_le_card_vert [Finite V] [Nonempty V] (h :
     G.edgeSet.ncard + 1 ≤ Nat.card V := by
   grind [h.card_edgeSet_add_card_connectedComponent, Nat.card_pos]
 
+theorem IsTree.ncard_edgeSet [Finite V] (hG : G.IsTree) : G.edgeSet.ncard + 1 = Nat.card V := by
+  rw [← hG.isAcyclic.card_edgeSet_add_card_connectedComponent,
+    connected_iff_natCard_connectedComponent_eq_one.mp hG.connected]
+
 /-- A graph on `n` vertices with at least `n` edges is not acyclic -/
 theorem card_vert_le_card_edgeSet_isAcyclic [Finite V] [Nonempty V]
     (h : Nat.card V ≤ G.edgeSet.ncard) : ¬G.IsAcyclic :=

From e952ebd1465396b16e8ef9ada371bc0d25a39de8 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Thu, 18 Jun 2026 17:53:02 +0300
Subject: [PATCH 26/36] `card_edgeSet` -> `ncard_edgeSet` in names

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

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index 4d771cd75139ac..0ed747c6bd3121 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -519,7 +519,7 @@ lemma isTree_iff_connected_and_card [Finite V] :
   exact Finset.card_lt_card <| by simpa [deleteEdges, edgeFinset]
 
 /-- An acyclic graph on `n` vertices with `c` connected components has exactly `n - c` edges -/
-theorem IsAcyclic.card_edgeSet_add_card_connectedComponent [Finite V] (h : G.IsAcyclic) :
+theorem IsAcyclic.ncard_edgeSet_add_card_connectedComponent [Finite V] (h : G.IsAcyclic) :
     G.edgeSet.ncard + Nat.card G.ConnectedComponent = Nat.card V := by
   have := Fintype.ofFinite G.ConnectedComponent
   rw [Nat.card_congr G.verticesEquivSigmaConnectedComponent, Nat.card_sigma, ← Nat.card_coe_set_eq,
@@ -530,26 +530,26 @@ theorem IsAcyclic.card_edgeSet_add_card_connectedComponent [Finite V] (h : G.IsA
   exact (isTree_iff_connected_and_card.mp <| h.isTree_connectedComponent _).right
 
 /-- An acyclic graph on `n` vertices has at most `n - 1` edges -/
-theorem IsAcyclic.card_edgeSet_add_one_le_card_vert [Finite V] [Nonempty V] (h : G.IsAcyclic) :
+theorem IsAcyclic.ncard_edgeSet_add_one_le_card_vert [Finite V] [Nonempty V] (h : G.IsAcyclic) :
     G.edgeSet.ncard + 1 ≤ Nat.card V := by
-  grind [h.card_edgeSet_add_card_connectedComponent, Nat.card_pos]
+  grind [h.ncard_edgeSet_add_card_connectedComponent, Nat.card_pos]
 
 theorem IsTree.ncard_edgeSet [Finite V] (hG : G.IsTree) : G.edgeSet.ncard + 1 = Nat.card V := by
-  rw [← hG.isAcyclic.card_edgeSet_add_card_connectedComponent,
+  rw [← hG.isAcyclic.ncard_edgeSet_add_card_connectedComponent,
     connected_iff_natCard_connectedComponent_eq_one.mp hG.connected]
 
 /-- A graph on `n` vertices with at least `n` edges is not acyclic -/
-theorem card_vert_le_card_edgeSet_isAcyclic [Finite V] [Nonempty V]
+theorem card_vert_le_ncard_edgeSet_isAcyclic [Finite V] [Nonempty V]
     (h : Nat.card V ≤ G.edgeSet.ncard) : ¬G.IsAcyclic :=
-  (Nat.not_le_of_lt ·.card_edgeSet_add_one_le_card_vert h)
+  (Nat.not_le_of_lt ·.ncard_edgeSet_add_one_le_card_vert h)
 
 /-- A graph on `n` vertices with at least `n` edges has a cycle -/
-theorem card_vert_le_card_edgeSet_exists_isCycle [Finite V] [Nonempty V]
+theorem card_vert_le_ncard_edgeSet_exists_isCycle [Finite V] [Nonempty V]
     (h : Nat.card V ≤ G.edgeSet.ncard) : ∃ (v : V) (c : G.Walk v v), c.IsCycle := by
-  grind [IsAcyclic, card_vert_le_card_edgeSet_isAcyclic h]
+  grind [IsAcyclic, card_vert_le_ncard_edgeSet_isAcyclic h]
 
 /-- A graph on `n` vertices is a tree iff it is acyclic and has exactly `n - 1` edges -/
-theorem isTree_iff_isAcyclic_and_card_edgeSet_add_one_eq_card [Finite V] :
+theorem isTree_iff_isAcyclic_and_ncard_edgeSet_add_one_eq_card [Finite V] :
     G.IsTree ↔ G.IsAcyclic ∧ G.edgeSet.ncard + 1 = Nat.card V := by
   have := Fintype.ofFinite V
   have := Fintype.ofFinite G.edgeSet
@@ -558,7 +558,7 @@ theorem isTree_iff_isAcyclic_and_card_edgeSet_add_one_eq_card [Finite V] :
   suffices G.Reachable = ⊤ by simp [this]
   rw [← G.reachable_is_equivalence.eqvGen_eq]
   refine Quot.subsingleton_iff _ |>.mp <| Nat.card_eq_one_iff_unique.mp ?_ |>.left
-  grind [h.card_edgeSet_add_card_connectedComponent, ConnectedComponent]
+  grind [h.ncard_edgeSet_add_card_connectedComponent, ConnectedComponent]
 
 /-- The minimum degree of all vertices in a nontrivial tree is one. -/
 lemma IsTree.minDegree_eq_one_of_nontrivial (h : G.IsTree) [Fintype V] [Nontrivial V]

From fbff91bf2ae4f4b48a6add1099ba7440e37b585a Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Thu, 18 Jun 2026 18:09:56 +0300
Subject: [PATCH 27/36] delete `card_vert_le_ncard_edgeSet_isAcyclic`

---
 Mathlib/Combinatorics/SimpleGraph/Acyclic.lean | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index 0ed747c6bd3121..6d3603610f4f2f 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -538,15 +538,12 @@ theorem IsTree.ncard_edgeSet [Finite V] (hG : G.IsTree) : G.edgeSet.ncard + 1 =
   rw [← hG.isAcyclic.ncard_edgeSet_add_card_connectedComponent,
     connected_iff_natCard_connectedComponent_eq_one.mp hG.connected]
 
-/-- A graph on `n` vertices with at least `n` edges is not acyclic -/
-theorem card_vert_le_ncard_edgeSet_isAcyclic [Finite V] [Nonempty V]
-    (h : Nat.card V ≤ G.edgeSet.ncard) : ¬G.IsAcyclic :=
-  (Nat.not_le_of_lt ·.ncard_edgeSet_add_one_le_card_vert h)
-
 /-- A graph on `n` vertices with at least `n` edges has a cycle -/
 theorem card_vert_le_ncard_edgeSet_exists_isCycle [Finite V] [Nonempty V]
     (h : Nat.card V ≤ G.edgeSet.ncard) : ∃ (v : V) (c : G.Walk v v), c.IsCycle := by
-  grind [IsAcyclic, card_vert_le_ncard_edgeSet_isAcyclic h]
+  suffices ¬G.IsAcyclic by grind [IsAcyclic]
+  apply mt IsAcyclic.ncard_edgeSet_add_one_le_card_vert
+  lia
 
 /-- A graph on `n` vertices is a tree iff it is acyclic and has exactly `n - 1` edges -/
 theorem isTree_iff_isAcyclic_and_ncard_edgeSet_add_one_eq_card [Finite V] :

From ea26511002ddab1ff39dd622e80902cbb4dd2dcf Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Thu, 18 Jun 2026 18:11:29 +0300
Subject: [PATCH 28/36] rename `card_vert_le_ncard_edgeSet_exists_isCycle` ->
 `exists_isCycle_of_card_le`

---
 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 6d3603610f4f2f..d2dfba196c4dfd 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -539,7 +539,7 @@ theorem IsTree.ncard_edgeSet [Finite V] (hG : G.IsTree) : G.edgeSet.ncard + 1 =
     connected_iff_natCard_connectedComponent_eq_one.mp hG.connected]
 
 /-- A graph on `n` vertices with at least `n` edges has a cycle -/
-theorem card_vert_le_ncard_edgeSet_exists_isCycle [Finite V] [Nonempty V]
+theorem exists_isCycle_of_card_le [Finite V] [Nonempty V]
     (h : Nat.card V ≤ G.edgeSet.ncard) : ∃ (v : V) (c : G.Walk v v), c.IsCycle := by
   suffices ¬G.IsAcyclic by grind [IsAcyclic]
   apply mt IsAcyclic.ncard_edgeSet_add_one_le_card_vert

From 43c05db471fe57e7ded9877a573f0f2f3c93c6db Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Thu, 18 Jun 2026 18:12:31 +0300
Subject: [PATCH 29/36] more name fixes

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

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index d2dfba196c4dfd..8c20b07d27e17a 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -488,7 +488,7 @@ lemma Connected.exists_isTree_le (h : G.Connected) : ∃ T ≤ G, IsTree T := by
   obtain ⟨F, hF⟩ := G.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic bot_le isAcyclic_bot
   grind [IsTree, Connected, preconnected_iff_reachable_eq_top]
 
-theorem connected_iff_natCard_connectedComponent_eq_one :
+theorem connected_iff_card_connectedComponent_eq_one :
     G.Connected ↔ Nat.card G.ConnectedComponent = 1 := by
   have : G.ConnectedComponent = Quotient G.reachableSetoid := rfl
   simp_rw [connected_iff, preconnected_iff_reachable_eq_top, Nat.card_eq_one_iff_unique, this,
@@ -530,19 +530,20 @@ theorem IsAcyclic.ncard_edgeSet_add_card_connectedComponent [Finite V] (h : G.Is
   exact (isTree_iff_connected_and_card.mp <| h.isTree_connectedComponent _).right
 
 /-- An acyclic graph on `n` vertices has at most `n - 1` edges -/
-theorem IsAcyclic.ncard_edgeSet_add_one_le_card_vert [Finite V] [Nonempty V] (h : G.IsAcyclic) :
+theorem IsAcyclic.ncard_edgeSet_add_one_le_card [Finite V] [Nonempty V] (h : G.IsAcyclic) :
     G.edgeSet.ncard + 1 ≤ Nat.card V := by
   grind [h.ncard_edgeSet_add_card_connectedComponent, Nat.card_pos]
 
-theorem IsTree.ncard_edgeSet [Finite V] (hG : G.IsTree) : G.edgeSet.ncard + 1 = Nat.card V := by
+theorem IsTree.ncard_edgeSet_add_one [Finite V] (hG : G.IsTree) :
+    G.edgeSet.ncard + 1 = Nat.card V := by
   rw [← hG.isAcyclic.ncard_edgeSet_add_card_connectedComponent,
-    connected_iff_natCard_connectedComponent_eq_one.mp hG.connected]
+    connected_iff_card_connectedComponent_eq_one.mp hG.connected]
 
 /-- A graph on `n` vertices with at least `n` edges has a cycle -/
 theorem exists_isCycle_of_card_le [Finite V] [Nonempty V]
     (h : Nat.card V ≤ G.edgeSet.ncard) : ∃ (v : V) (c : G.Walk v v), c.IsCycle := by
   suffices ¬G.IsAcyclic by grind [IsAcyclic]
-  apply mt IsAcyclic.ncard_edgeSet_add_one_le_card_vert
+  apply mt IsAcyclic.ncard_edgeSet_add_one_le_card
   lia
 
 /-- A graph on `n` vertices is a tree iff it is acyclic and has exactly `n - 1` edges -/

From 87fd089e52d82b87700075a0e6316b419eab3f59 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Thu, 18 Jun 2026 18:15:50 +0300
Subject: [PATCH 30/36] `Quot.mk G.Reachable` -> `G.connectedComponentMk`

---
 Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
index 7b95c9114a6d1a..e440d35f0a19b1 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
@@ -699,7 +699,7 @@ variable (G) in
 /-- The vertices of a graph are partitioned among its connected components -/
 @[simps!]
 def verticesEquivSigmaConnectedComponent : V ≃ Σ (c : G.ConnectedComponent), c :=
-  .symm <| .sigmaFiberEquiv <| Quot.mk G.Reachable
+  .symm <| .sigmaFiberEquiv G.connectedComponentMk
 
 variable (G) in
 /-- The edges of a graph are partitioned among its connected components -/

From f60f58a24b483d1fbab62c75fc0fff856a496e3d Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Thu, 18 Jun 2026 18:45:26 +0300
Subject: [PATCH 31/36] `IsTree.ncard_edgeSet_add_one` follows directly from
 the finset version

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

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index 8c20b07d27e17a..c2e9c621b97073 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -365,6 +365,12 @@ lemma IsTree.card_edgeFinset [Fintype V] [Fintype G.edgeSet] (hG : G.IsTree) :
       refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
       simp [h.ne]
 
+theorem IsTree.ncard_edgeSet_add_one [Finite V] (hG : G.IsTree) :
+    G.edgeSet.ncard + 1 = Nat.card V := by
+  have := Fintype.ofFinite V
+  have := Fintype.ofFinite G.edgeSet
+  simpa [edgeFinset] using hG.card_edgeFinset
+
 /-- A minimally connected graph is a tree. -/
 lemma isTree_of_minimal_connected (h : Minimal Connected G) : IsTree G := by
   rw [isTree_iff, and_iff_right h.prop, isAcyclic_iff_forall_adj_isBridge]
@@ -509,8 +515,7 @@ lemma isTree_iff_connected_and_card [Finite V] :
     G.IsTree ↔ G.Connected ∧ Nat.card G.edgeSet + 1 = Nat.card V := by
   have := Fintype.ofFinite V
   classical
-  refine ⟨fun h ↦ ⟨h.connected, by simpa [edgeFinset] using h.card_edgeFinset⟩,
-    fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩
+  refine ⟨fun h ↦ ⟨h.connected, h.ncard_edgeSet_add_one⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩
   simp_rw [isAcyclic_iff_forall_adj_isBridge]
   refine fun x y h ↦ by_contra fun hbr ↦
     (h₁.connected_delete_edge_of_not_isBridge hbr).card_vert_le_card_edgeSet_add_one.not_gt ?_
@@ -534,11 +539,6 @@ theorem IsAcyclic.ncard_edgeSet_add_one_le_card [Finite V] [Nonempty V] (h : G.I
     G.edgeSet.ncard + 1 ≤ Nat.card V := by
   grind [h.ncard_edgeSet_add_card_connectedComponent, Nat.card_pos]
 
-theorem IsTree.ncard_edgeSet_add_one [Finite V] (hG : G.IsTree) :
-    G.edgeSet.ncard + 1 = Nat.card V := by
-  rw [← hG.isAcyclic.ncard_edgeSet_add_card_connectedComponent,
-    connected_iff_card_connectedComponent_eq_one.mp hG.connected]
-
 /-- A graph on `n` vertices with at least `n` edges has a cycle -/
 theorem exists_isCycle_of_card_le [Finite V] [Nonempty V]
     (h : Nat.card V ≤ G.edgeSet.ncard) : ∃ (v : V) (c : G.Walk v v), c.IsCycle := by
@@ -551,7 +551,7 @@ theorem isTree_iff_isAcyclic_and_ncard_edgeSet_add_one_eq_card [Finite V] :
     G.IsTree ↔ G.IsAcyclic ∧ G.edgeSet.ncard + 1 = Nat.card V := by
   have := Fintype.ofFinite V
   have := Fintype.ofFinite G.edgeSet
-  refine ⟨fun h ↦ ⟨h.isAcyclic, by simpa [edgeFinset] using h.card_edgeFinset⟩, ?_⟩
+  refine ⟨fun h ↦ ⟨h.isAcyclic, h.ncard_edgeSet_add_one⟩, ?_⟩
   refine fun ⟨h, _⟩ ↦ ⟨{ preconnected a b := ?_, nonempty := by grind [Nat.card_pos_iff] }, h⟩
   suffices G.Reachable = ⊤ by simp [this]
   rw [← G.reachable_is_equivalence.eqvGen_eq]

From fc3fa5a51efcca633572ccee22673763c539f4d2 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Thu, 18 Jun 2026 18:54:12 +0300
Subject: [PATCH 32/36] golf
 `isTree_iff_isAcyclic_and_ncard_edgeSet_add_one_eq_card`

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

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index c2e9c621b97073..a504294d2318b0 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -549,14 +549,8 @@ theorem exists_isCycle_of_card_le [Finite V] [Nonempty V]
 /-- A graph on `n` vertices is a tree iff it is acyclic and has exactly `n - 1` edges -/
 theorem isTree_iff_isAcyclic_and_ncard_edgeSet_add_one_eq_card [Finite V] :
     G.IsTree ↔ G.IsAcyclic ∧ G.edgeSet.ncard + 1 = Nat.card V := by
-  have := Fintype.ofFinite V
-  have := Fintype.ofFinite G.edgeSet
-  refine ⟨fun h ↦ ⟨h.isAcyclic, h.ncard_edgeSet_add_one⟩, ?_⟩
-  refine fun ⟨h, _⟩ ↦ ⟨{ preconnected a b := ?_, nonempty := by grind [Nat.card_pos_iff] }, h⟩
-  suffices G.Reachable = ⊤ by simp [this]
-  rw [← G.reachable_is_equivalence.eqvGen_eq]
-  refine Quot.subsingleton_iff _ |>.mp <| Nat.card_eq_one_iff_unique.mp ?_ |>.left
-  grind [h.ncard_edgeSet_add_card_connectedComponent, ConnectedComponent]
+  refine ⟨fun h ↦ ⟨h.isAcyclic, h.ncard_edgeSet_add_one⟩, fun ⟨h, _⟩ ↦ ⟨?_, h⟩⟩
+  grind [connected_iff_card_connectedComponent_eq_one, h.ncard_edgeSet_add_card_connectedComponent]
 
 /-- The minimum degree of all vertices in a nontrivial tree is one. -/
 lemma IsTree.minDegree_eq_one_of_nontrivial (h : G.IsTree) [Fintype V] [Nontrivial V]

From 7eabf4ad985cf882e3da59205c55fc36f4360e73 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 11 Jul 2026 22:33:30 +0300
Subject: [PATCH 33/36] Apply suggestions from code review

docstring periods

Co-authored-by: Rida Hamadani <mridahamadani@gmail.com>
---
 Mathlib/Combinatorics/SimpleGraph/Acyclic.lean | 8 ++++----
 Mathlib/Order/RelIso/Basic.lean                | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index a504294d2318b0..d2bf9fa74a4a78 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -523,7 +523,7 @@ lemma isTree_iff_connected_and_card [Finite V] :
     ← edgeFinset_card, add_lt_add_iff_right]
   exact Finset.card_lt_card <| by simpa [deleteEdges, edgeFinset]
 
-/-- An acyclic graph on `n` vertices with `c` connected components has exactly `n - c` edges -/
+/-- An acyclic graph on `n` vertices with `c` connected components has exactly `n - c` edges. -/
 theorem IsAcyclic.ncard_edgeSet_add_card_connectedComponent [Finite V] (h : G.IsAcyclic) :
     G.edgeSet.ncard + Nat.card G.ConnectedComponent = Nat.card V := by
   have := Fintype.ofFinite G.ConnectedComponent
@@ -534,19 +534,19 @@ theorem IsAcyclic.ncard_edgeSet_add_card_connectedComponent [Finite V] (h : G.Is
   ext
   exact (isTree_iff_connected_and_card.mp <| h.isTree_connectedComponent _).right
 
-/-- An acyclic graph on `n` vertices has at most `n - 1` edges -/
+/-- An acyclic graph on `n` vertices has at most `n - 1` edges. -/
 theorem IsAcyclic.ncard_edgeSet_add_one_le_card [Finite V] [Nonempty V] (h : G.IsAcyclic) :
     G.edgeSet.ncard + 1 ≤ Nat.card V := by
   grind [h.ncard_edgeSet_add_card_connectedComponent, Nat.card_pos]
 
-/-- A graph on `n` vertices with at least `n` edges has a cycle -/
+/-- A graph on `n` vertices with at least `n` edges has a cycle. -/
 theorem exists_isCycle_of_card_le [Finite V] [Nonempty V]
     (h : Nat.card V ≤ G.edgeSet.ncard) : ∃ (v : V) (c : G.Walk v v), c.IsCycle := by
   suffices ¬G.IsAcyclic by grind [IsAcyclic]
   apply mt IsAcyclic.ncard_edgeSet_add_one_le_card
   lia
 
-/-- A graph on `n` vertices is a tree iff it is acyclic and has exactly `n - 1` edges -/
+/-- A graph on `n` vertices is a tree iff it is acyclic and has exactly `n - 1` edges. -/
 theorem isTree_iff_isAcyclic_and_ncard_edgeSet_add_one_eq_card [Finite V] :
     G.IsTree ↔ G.IsAcyclic ∧ G.edgeSet.ncard + 1 = Nat.card V := by
   refine ⟨fun h ↦ ⟨h.isAcyclic, h.ncard_edgeSet_add_one⟩, fun ⟨h, _⟩ ↦ ⟨?_, h⟩⟩
diff --git a/Mathlib/Order/RelIso/Basic.lean b/Mathlib/Order/RelIso/Basic.lean
index 1504ccdfedfbba..50e416fe7ed4ac 100644
--- a/Mathlib/Order/RelIso/Basic.lean
+++ b/Mathlib/Order/RelIso/Basic.lean
@@ -144,7 +144,7 @@ protected def id (r : α → α → Prop) : r →r r :=
 protected def comp (g : s →r t) (f : r →r s) : r →r t :=
   ⟨fun x => g (f x), fun h => g.2 (f.2 h)⟩
 
-/-- The identity relation homomorphism between subrelations -/
+/-- The identity relation homomorphism between subrelations. -/
 @[simps]
 protected def ofLE {r' : α → α → Prop} (le : r ≤ r') : r →r r' :=
   ⟨id, @le⟩

From 884695788210d36fa498eb4e2cb67f5d0de30d65 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 11 Jul 2026 22:41:23 +0300
Subject: [PATCH 34/36] more docstring periods

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

diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
index aaff91506bcb64..fba756f64d3edc 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
@@ -707,13 +707,13 @@ theorem maximal_connected_induce_iff (s : Set V) :
 end ConnectedComponent
 
 variable (G) in
-/-- The vertices of a graph are partitioned among its connected components -/
+/-- The vertices of a graph are partitioned among its connected components. -/
 @[simps!]
 def verticesEquivSigmaConnectedComponent : V ≃ Σ (c : G.ConnectedComponent), c :=
   .symm <| .sigmaFiberEquiv G.connectedComponentMk
 
 variable (G) in
-/-- The edges of a graph are partitioned among its connected components -/
+/-- The edges of a graph are partitioned among its connected components. -/
 @[simps!]
 def edgeSetEquivSigmaConnectedComponent :
     G.edgeSet ≃ Σ (c : G.ConnectedComponent), c.toSimpleGraph.edgeSet :=

From f2906dcbe96dde8bc7ace271a92f92a4a0302c73 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 11 Jul 2026 22:51:09 +0300
Subject: [PATCH 35/36] small golf to
 `ncard_edgeSet_add_card_connectedComponent`

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

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index 74a1a551842b89..0246e39524c1b3 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -508,9 +508,8 @@ theorem IsAcyclic.ncard_edgeSet_add_card_connectedComponent [Finite V] (h : G.Is
   rw [Nat.card_congr G.verticesEquivSigmaConnectedComponent, Nat.card_sigma, ← Nat.card_coe_set_eq,
     Nat.card_congr G.edgeSetEquivSigmaConnectedComponent, Nat.card_sigma,
     ← Fintype.card_eq_nat_card, Fintype.card_eq_sum_ones, ← Finset.sum_add_distrib]
-  congr
-  ext
-  exact (isTree_iff_connected_and_card.mp <| h.isTree_connectedComponent _).right
+  congr!
+  exact h.isTree_connectedComponent _ |>.ncard_edgeSet_add_one
 
 /-- An acyclic graph on `n` vertices has at most `n - 1` edges. -/
 theorem IsAcyclic.ncard_edgeSet_add_one_le_card [Finite V] [Nonempty V] (h : G.IsAcyclic) :

From 8379122c7030283f41faf9e289504f38b8725a55 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Sat, 11 Jul 2026 23:11:00 +0300
Subject: [PATCH 36/36] extract the summations of connected component sizes to
 lemmas

---
 Mathlib/Combinatorics/SimpleGraph/Acyclic.lean | 18 ++++++++++++++----
 .../SimpleGraph/Connectivity/Connected.lean    |  4 ++--
 2 files changed, 16 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
index 0246e39524c1b3..c3f3fd8afbd4e3 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
@@ -478,6 +478,17 @@ theorem connected_iff_card_connectedComponent_eq_one :
   simp_rw [connected_iff, preconnected_iff_reachable_eq_top, Nat.card_eq_one_iff_unique, this,
     nonempty_quotient_iff, Quotient.subsingleton_iff, reachableSetoid, Setoid.mk_eq_top]
 
+variable (G) in
+theorem sum_connectedComponent_ncard_supp [Finite V] [Fintype G.ConnectedComponent] :
+    ∑ c : G.ConnectedComponent, c.supp.ncard = Nat.card V := by
+  rw [Nat.card_congr G.verticesEquivSigmaConnectedComponent, Nat.card_sigma]
+  rfl
+
+variable (G) in
+theorem sum_connectedComponent_ncard_edgeSet [Finite V] [Fintype G.ConnectedComponent] :
+    ∑ c : G.ConnectedComponent, c.toSimpleGraph.edgeSet.ncard = G.edgeSet.ncard := by
+  simpa [Nat.card_sigma] using Nat.card_congr G.edgeSetEquivSigmaConnectedComponent.symm
+
 /-- Every connected graph on `n` vertices has at least `n-1` edges. -/
 lemma Connected.card_vert_le_card_edgeSet_add_one (h : G.Connected) :
     Nat.card V ≤ Nat.card G.edgeSet + 1 := by
@@ -505,11 +516,10 @@ lemma isTree_iff_connected_and_card [Finite V] :
 theorem IsAcyclic.ncard_edgeSet_add_card_connectedComponent [Finite V] (h : G.IsAcyclic) :
     G.edgeSet.ncard + Nat.card G.ConnectedComponent = Nat.card V := by
   have := Fintype.ofFinite G.ConnectedComponent
-  rw [Nat.card_congr G.verticesEquivSigmaConnectedComponent, Nat.card_sigma, ← Nat.card_coe_set_eq,
-    Nat.card_congr G.edgeSetEquivSigmaConnectedComponent, Nat.card_sigma,
+  rw [← sum_connectedComponent_ncard_edgeSet, ← G.sum_connectedComponent_ncard_supp,
     ← Fintype.card_eq_nat_card, Fintype.card_eq_sum_ones, ← Finset.sum_add_distrib]
-  congr!
-  exact h.isTree_connectedComponent _ |>.ncard_edgeSet_add_one
+  simp_rw [h.isTree_connectedComponent _ |>.ncard_edgeSet_add_one]
+  rfl
 
 /-- An acyclic graph on `n` vertices has at most `n - 1` edges. -/
 theorem IsAcyclic.ncard_edgeSet_add_one_le_card [Finite V] [Nonempty V] (h : G.IsAcyclic) :
diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
index fba756f64d3edc..fe1cd2a528770e 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
@@ -709,14 +709,14 @@ end ConnectedComponent
 variable (G) in
 /-- The vertices of a graph are partitioned among its connected components. -/
 @[simps!]
-def verticesEquivSigmaConnectedComponent : V ≃ Σ (c : G.ConnectedComponent), c :=
+def verticesEquivSigmaConnectedComponent : V ≃ Σ c : G.ConnectedComponent, c :=
   .symm <| .sigmaFiberEquiv G.connectedComponentMk
 
 variable (G) in
 /-- The edges of a graph are partitioned among its connected components. -/
 @[simps!]
 def edgeSetEquivSigmaConnectedComponent :
-    G.edgeSet ≃ Σ (c : G.ConnectedComponent), c.toSimpleGraph.edgeSet :=
+    G.edgeSet ≃ Σ c : G.ConnectedComponent, c.toSimpleGraph.edgeSet :=
   .sigmaQuotFromRel G.symm <| .ofLE fun _ _ ↦ Adj.reachable
 
 /-- Given graph homomorphisms from each connected component of `G` to `H`, this is the graph