From d9c853b93556f41e86f0e2f5883b74ba1532b239 Mon Sep 17 00:00:00 2001
From: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Thu, 30 Nov 2023 02:18:08 +0000
Subject: [PATCH] feat: number of edges in a complete graph (#8631)

---
 Mathlib/Combinatorics/SimpleGraph/Basic.lean  | 26 ++++++++++++++++++-
 .../Combinatorics/SimpleGraph/DegreeSum.lean  |  3 +--
 Mathlib/Data/Sym/Sym2.lean                    |  3 +++
 3 files changed, 29 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean
index 161701af76331..b254a8b6a7d54 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Basic.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Basic.lean
@@ -6,7 +6,7 @@ Authors: Aaron Anderson, Jalex Stark, Kyle Miller, Alena Gusakov, Hunter Monroe
 import Mathlib.Combinatorics.SimpleGraph.Init
 import Mathlib.Data.Rel
 import Mathlib.Data.Set.Finite
-import Mathlib.Data.Sym.Sym2
+import Mathlib.Data.Sym.Card
 
 #align_import combinatorics.simple_graph.basic from "leanprover-community/mathlib"@"c6ef6387ede9983aee397d442974e61f89dfd87b"
 
@@ -539,6 +539,14 @@ theorem edgeSet_bot : (⊥ : SimpleGraph V).edgeSet = ∅ :=
   Sym2.fromRel_bot
 #align simple_graph.edge_set_bot SimpleGraph.edgeSet_bot
 
+@[simp]
+theorem edgeSet_top : (⊤ : SimpleGraph V).edgeSet = {e | ¬e.IsDiag} :=
+  Sym2.fromRel_ne
+
+@[simp]
+theorem edgeSet_subset_setOf_not_isDiag : G.edgeSet ⊆ {e | ¬e.IsDiag} :=
+  fun _ h => (Sym2.fromRel_irreflexive (sym := G.symm)).mp G.loopless h
+
 @[simp]
 theorem edgeSet_sup : (G₁ ⊔ G₂).edgeSet = G₁.edgeSet ∪ G₂.edgeSet := by
   ext ⟨x, y⟩
@@ -967,6 +975,22 @@ theorem edgeSet_univ_card : (univ : Finset G.edgeSet).card = G.edgeFinset.card :
   Fintype.card_of_subtype G.edgeFinset fun _ => mem_edgeFinset
 #align simple_graph.edge_set_univ_card SimpleGraph.edgeSet_univ_card
 
+variable [Fintype V] [DecidableEq V]
+
+@[simp]
+theorem edgeFinset_top : (⊤ : SimpleGraph V).edgeFinset = univ.filter fun e => ¬e.IsDiag := by
+  rw [← coe_inj]; simp
+
+/-- The complete graph on `n` vertices has `n.choose 2` edges. -/
+theorem card_edgeFinset_top_eq_card_choose_two :
+    (⊤ : SimpleGraph V).edgeFinset.card = (Fintype.card V).choose 2 := by
+  simp_rw [Set.toFinset_card, edgeSet_top, Set.coe_setOf, ← Sym2.card_subtype_not_diag]
+
+/-- Any graph on `n` vertices has at most `n.choose 2` edges. -/
+theorem card_edgeFinset_le_card_choose_two : G.edgeFinset.card ≤ (Fintype.card V).choose 2 := by
+  rw [← card_edgeFinset_top_eq_card_choose_two]
+  exact card_le_of_subset (edgeFinset_mono le_top)
+
 end EdgeFinset
 
 @[simp]
diff --git a/Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean b/Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
index 8a7a15a9053d4..4e9e3055bee8f 100644
--- a/Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
@@ -39,8 +39,7 @@ simple graphs, sums, degree-sum formula, handshaking lemma
 
 
 open Finset
-
-open BigOperators
+open scoped BigOperators
 
 namespace SimpleGraph
 
diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
index 439c581c2d543..d41efad7d50e2 100644
--- a/Mathlib/Data/Sym/Sym2.lean
+++ b/Mathlib/Data/Sym/Sym2.lean
@@ -515,6 +515,9 @@ theorem fromRel_top : fromRel (fun (x y : α) z => z : Symmetric ⊤) = Set.univ
   simp [-Set.top_eq_univ, Prop.top_eq_true]
 #align sym2.from_rel_top Sym2.fromRel_top
 
+theorem fromRel_ne : fromRel (fun (x y : α) z => z.symm : Symmetric Ne) = {z | ¬IsDiag z} := by
+  ext z; exact z.ind (by simp)
+
 theorem fromRel_irreflexive {sym : Symmetric r} :
     Irreflexive r ↔ ∀ {z}, z ∈ fromRel sym → ¬IsDiag z :=
   { mp := by intro h; apply Sym2.ind; aesop