feat(Combinatorics/SimpleGraph/Finite): Set.ncard of neighborSet

Mathlib/Combinatorics/SimpleGraph/Finite.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Combinatorics.SimpleGraph.Maps
 public import Mathlib.Data.Finset.Max
+public import Mathlib.Data.Set.Card
 public import Mathlib.Data.Sym.Card
 
 /-!
@@ -125,7 +126,7 @@ theorem card_edgeSet : Fintype.card G.edgeSet = #G.edgeFinset :=
   .symm <| Set.toFinset_card _
 
 theorem edgeSet_univ_card : #(univ : Finset G.edgeSet) = #G.edgeFinset := by
-  simp [card_edgeSet]
+  simp [card_edgeSet, -Set.fintypeCard_eq_ncard]
 
 variable [Fintype V]
 
@@ -205,6 +206,14 @@ theorem card_neighborFinset_eq_degree : #(G.neighborFinset v) = G.degree v := rf
 theorem card_neighborSet_eq_degree : Fintype.card (G.neighborSet v) = G.degree v :=
   (Set.toFinset_card _).symm
 
+@[simp]
+theorem ncard_neighborSet : (G.neighborSet v).ncard = G.degree v := by
+  simp [← Set.fintypeCard_eq_ncard, card_neighborSet_eq_degree]
+
+@[simp]
+theorem encard_neighborSet : (G.neighborSet v).encard = G.degree v := by
+  simp [← Set.coe_fintypeCard]
+
 lemma degree_eq_zero : G.degree v = 0 ↔ G.IsIsolated v := by simp [← card_neighborFinset_eq_degree]
 lemma degree_pos : 0 < G.degree v ↔ ¬ G.IsIsolated v := by simp [← card_neighborFinset_eq_degree]
 
@@ -250,8 +259,7 @@ theorem degree_compl [Fintype (Gᶜ.neighborSet v)] [Fintype V] :
     Gᶜ.degree v = Fintype.card V - 1 - G.degree v := by
   classical
     rw [← card_neighborSet_union_compl_neighborSet G v, Set.toFinset_union]
-    simp [card_union_of_disjoint (Set.disjoint_toFinset.mpr (compl_neighborSet_disjoint G v)),
-      card_neighborSet_eq_degree]
+    simp [card_union_of_disjoint (Set.disjoint_toFinset.mpr (compl_neighborSet_disjoint G v))]
 
 instance incidenceSetFintype [DecidableEq V] : Fintype (G.incidenceSet v) :=
   Fintype.ofEquiv (G.neighborSet v) (G.incidenceSetEquivNeighborSet v).symm
@@ -264,6 +272,16 @@ theorem card_incidenceSet_eq_degree [DecidableEq V] :
     Fintype.card (G.incidenceSet v) = G.degree v := by
   rw [Fintype.card_congr (G.incidenceSetEquivNeighborSet v), card_neighborSet_eq_degree]
 
+@[simp]
+theorem ncard_incidenceSet : (G.incidenceSet v).ncard = G.degree v := by
+  classical
+  simp [← Set.fintypeCard_eq_ncard, card_incidenceSet_eq_degree]
+
+@[simp]
+theorem encard_incidenceSet : (G.incidenceSet v).encard = G.degree v := by
+  classical
+  simp [← Set.coe_fintypeCard]
+
 @[simp, norm_cast]
 theorem coe_incidenceFinset [DecidableEq V] :
     (G.incidenceFinset v : Set (Sym2 V)) = G.incidenceSet v := by
@@ -485,7 +503,7 @@ lemma minDegree_le_maxDegree [DecidableRel G.Adj] : G.minDegree ≤ G.maxDegree
 
 theorem IsRegularOfDegree.minDegree_eq [Nonempty V] [DecidableRel G.Adj] {d : ℕ}
     (h : G.IsRegularOfDegree d) : G.minDegree = d := by
-  simp [minDegree, h.degree_eq, Finset.image_const]
+  simp [minDegree, h.degree_eq, Finset.image_const, -ENat.some_eq_natCast]
 
 @[simp]
 lemma minDegree_bot_eq_zero : (⊥ : SimpleGraph V).minDegree = 0 :=
@@ -545,7 +563,13 @@ theorem Adj.card_commonNeighbors_lt_degree {G : SimpleGraph V} [DecidableRel G.A
 
 theorem card_commonNeighbors_top [DecidableEq V] {v w : V} (h : v ≠ w) :
     Fintype.card (commonNeighbors ⊤ v w) = Fintype.card V - 2 := by
-  simp [commonNeighbors_top_eq, ← Set.toFinset_card, Finset.card_sdiff, h]
+  simp [commonNeighbors_top_eq, ← Set.toFinset_card, Finset.card_sdiff, h,
+    -Set.fintypeCard_eq_ncard]
+
+omit [Fintype V] in
+theorem encard_commonNeighbors_top {u v : V} (h : u ≠ v) :
+    (commonNeighbors ⊤ u v).encard = ENat.card V - 2 := by
+  simp [commonNeighbors_top_eq, Set.encard_sdiff, Set.encard_pair h]
 
 @[simp] lemma insert_neighborFinset_eq_univ [DecidableEq V] [DecidableRel G.Adj] (v : V) :
     insert v (G.neighborFinset v) = univ ↔ G.IsUniversal v := by
@@ -689,6 +713,18 @@ theorem card_edgeFinset_map (f : V ↪ W) (G : SimpleGraph V) [DecidableRel G.Ad
   rw [edgeFinset_map]
   exact G.edgeFinset.card_map f.sym2Map
 
+theorem degree_map_apply {V W : Type*} (G : SimpleGraph V) (f : V ↪ W) (v : V)
+    [Fintype <| G.neighborSet v] [Fintype <| G.map f |>.neighborSet <| f v] :
+    (G.map f).degree (f v) = G.degree v := by
+  simp_rw [← ncard_neighborSet, neighborSet_map, Set.ncard_image_of_injective _ f.injective]
+
+theorem Embedding.degree_eq_of_neighborSet_subset_range {V V' : Type*} {G : SimpleGraph V}
+    {G' : SimpleGraph V'} {f : G ↪g G'} {v : V} [Fintype <| G.neighborSet v]
+    [Fintype <| G'.neighborSet <| f v] (h : G'.neighborSet (f v) ⊆ Set.range f) :
+    G'.degree (f v) = G.degree v := by
+  simp_rw [← ncard_neighborSet, ← Set.ncard_image_of_injective _ f.injective,
+    ← f.preimage_neighborSet, Set.image_preimage_eq_inter_range, Set.inter_eq_left.mpr h]
+
 end Map
 
 end SimpleGraph

Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean

@@ -106,7 +106,8 @@ variable [NonAssocSemiring R] [DecidableEq α] [DecidableRel G.Adj] {a : α} {e
 
 theorem sum_incMatrix_apply [Fintype (Sym2 α)] [Fintype (neighborSet G a)] :
     ∑ e, G.incMatrix R a e = G.degree a := by
-  simp [incMatrix_apply', sum_boole, Set.filter_mem_univ_eq_toFinset, card_incidenceSet_eq_degree]
+  simp [incMatrix_apply', sum_boole, Set.filter_mem_univ_eq_toFinset, card_incidenceSet_eq_degree,
+    -Set.fintypeCard_eq_ncard]
 
 set_option backward.isDefEq.respectTransparency false in
 theorem incMatrix_mul_transpose_diag [Fintype (Sym2 α)] [Fintype (neighborSet G a)] :

Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

@@ -875,7 +875,7 @@ theorem card_neighborSet_toSubgraph (G H : SimpleGraph V) (h : H ≤ G)
 lemma degree_toSubgraph (G H : SimpleGraph V) (h : H ≤ G) {v : V}
     [Fintype ↑((toSubgraph H h).neighborSet v)] [Fintype ↑(H.neighborSet v)] :
     (toSubgraph H h).degree v = H.degree v := by
-  simp [Subgraph.degree, card_neighborSet_toSubgraph]
+  simp [Subgraph.degree, card_neighborSet_toSubgraph, -Set.fintypeCard_eq_ncard]
 
 section MkProperties