diff --git a/Mathlib.lean b/Mathlib.lean
index b2b7f153003840..0332a3827f022c 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3651,6 +3651,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp
 public import Mathlib.Combinatorics.SimpleGraph.Copy
 public import Mathlib.Combinatorics.SimpleGraph.CycleGraph
 public import Mathlib.Combinatorics.SimpleGraph.Dart
+public import Mathlib.Combinatorics.SimpleGraph.Degree
 public import Mathlib.Combinatorics.SimpleGraph.DegreeSum
 public import Mathlib.Combinatorics.SimpleGraph.DeleteEdges
 public import Mathlib.Combinatorics.SimpleGraph.Density
diff --git a/Mathlib/Combinatorics/SimpleGraph/Degree.lean b/Mathlib/Combinatorics/SimpleGraph/Degree.lean
new file mode 100644
index 00000000000000..7fcf4abbf62f76
--- /dev/null
+++ b/Mathlib/Combinatorics/SimpleGraph/Degree.lean
@@ -0,0 +1,390 @@
+/-
+Copyright (c) 2026 Snir Broshi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Snir Broshi
+-/
+module
+
+public import Mathlib.Combinatorics.SimpleGraph.Copy
+public import Mathlib.Data.ENat.Lattice
+
+/-!
+# Degrees
+
+## Main definitions
+
+* `G.edegree v`: The extended degree of `v` in `G`: the number of vertices adjacent to `v`,
+  or `⊤` if there are infinitely many.
+* `G.maxEDegree`: The maximum extended degree of all vertices, or `0` if there are no vertices.
+* `G.minEDegree`: The minimum extended degree of all vertices, or `⊤` if there are no vertices.
+-/
+
+public section
+
+namespace SimpleGraph
+
+variable {V W : Type*} (G G' : SimpleGraph V) (H : SimpleGraph W) (u v : V)
+
+/-- `G.edegree v` is the extended degree of `v` in `G`: the number of vertices adjacent to `v`,
+or `⊤` if there are infinitely many. -/
+noncomputable def edegree : ℕ∞ :=
+  G.neighborSet v |>.encard
+
+@[simp]
+theorem encard_neighborSet : (G.neighborSet v).encard = G.edegree v := by
+  rfl
+
+variable {G v} in
+@[simp]
+theorem edegree_eq_zero_iff_isIsolated : G.edegree v = 0 ↔ G.IsIsolated v := by
+  simp [← encard_neighborSet]
+
+@[simp]
+alias ⟨_, IsIsolated.edegree_eq⟩ := edegree_eq_zero_iff_isIsolated
+
+variable {G u v} in
+theorem Adj.edegree_ne_zero_left (h : G.Adj u v) : G.edegree u ≠ 0 :=
+  edegree_eq_zero_iff_isIsolated.not.mpr h.not_isIsolated_left
+
+variable {G u v} in
+theorem Adj.edegree_ne_zero_right (h : G.Adj u v) : G.edegree v ≠ 0 :=
+  h.symm.edegree_ne_zero_left
+
+variable {G v} in
+theorem nontrivial_of_edegree_ne_zero (h : G.edegree v ≠ 0) : Nontrivial V :=
+  nontrivial_of_not_isIsolated <| edegree_eq_zero_iff_isIsolated.not.mp h
+
+theorem edegree_eq_zero_of_subsingleton [Subsingleton V] (G : SimpleGraph V) (v : V) :
+    G.edegree v = 0 := by
+  simp
+
+variable {G v} in
+theorem edegree_eq_one_iff_existsUnique_adj : G.edegree v = 1 ↔ ∃! u, G.Adj v u := by
+  simp [← encard_neighborSet, Set.encard_eq_one, Set.singleton_iff_unique_mem]
+
+variable {G v} in
+theorem edegree_ne_top_iff_finite_neighborSet : G.edegree v ≠ ⊤ ↔ (G.neighborSet v).Finite :=
+  Set.encard_ne_top_iff
+
+theorem edegree_ne_top_of_finite [Finite V] (G : SimpleGraph V) (v : V) : G.edegree v ≠ ⊤ :=
+  edegree_ne_top_iff_finite_neighborSet.mpr <| Set.toFinite _
+
+theorem coe_degree_eq_edegree [Fintype <| G.neighborSet v] : G.degree v = G.edegree v := by
+  simp [encard_neighborSet, ← ncard_neighborSet]
+
+variable {G v} in
+theorem edegree_eq_coe_iff [Fintype <| G.neighborSet v] {n : ℕ} :
+    G.edegree v = n ↔ G.degree v = n := by
+  simp [← coe_degree_eq_edegree]
+
+@[simp]
+theorem toNat_edegree [Fintype <| G.neighborSet v] : (G.edegree v).toNat = G.degree v := by
+  simp [← coe_degree_eq_edegree]
+
+theorem coe_toNat_edegree_eq_self :
+    (G.edegree v).toNat = G.edegree v ↔ (G.neighborSet v).Finite := by
+  simp [edegree_ne_top_iff_finite_neighborSet]
+
+theorem edegree_le_card : G.edegree v ≤ ENat.card V := by
+  grw [← encard_neighborSet, Set.encard_le_card]
+
+variable {v} in
+theorem edegree_lt_card_of_ne_top (h : G.edegree v ≠ ⊤) : G.edegree v < ENat.card V :=
+  edegree_ne_top_iff_finite_neighborSet.mp h |>.encard_lt_card <| G.neighborSet_ne_univ v
+
+@[simp]
+theorem encard_incidenceSet : (G.incidenceSet v).encard = G.edegree v := by
+  classical
+  simp [Set.encard_congr <| G.incidenceSetEquivNeighborSet v]
+
+theorem edegree_le_encard_edgeSet : G.edegree v ≤ G.edgeSet.encard := by
+  grw [← encard_incidenceSet, incidenceSet_subset]
+
+variable {G H} in
+theorem Copy.edegree_le (f : Copy G H) (v : V) : G.edegree v ≤ H.edegree (f v) :=
+  f.mapNeighborSet v |>.encard_le
+
+variable {G H} in
+@[simp]
+theorem Iso.edegree_eq (f : G ≃g H) (v : V) : H.edegree (f v) = G.edegree v :=
+  (Set.encard_congr <| f.mapNeighborSet v).symm
+
+variable {G G'} in
+@[gcongr]
+theorem edegree_mono (hle : G ≤ G') (v : V) : G.edegree v ≤ G'.edegree v :=
+  Copy.ofLE G G' hle |>.edegree_le v
+
+@[simp]
+theorem edegree_top : edegree ⊤ v = ENat.card V - 1 := by
+  rw [← encard_neighborSet, neighborSet_top, ← Set.encard_ne_add_one v, ← Set.compl_singleton_eq]
+  cases Set.encard {v}ᶜ <;> norm_cast
+
+theorem edegree_bot : edegree ⊥ v = 0 := by
+  simp
+
+variable {G} in
+theorem IsRegularOfDegree.edegree_eq [G.LocallyFinite] {d : ℕ} (h : G.IsRegularOfDegree d) (v : V) :
+    G.edegree v = d :=
+  edegree_eq_coe_iff.mpr <| h.degree_eq v
+
+/-- The maximum extended degree of all vertices, or `0` if there are no vertices -/
+noncomputable def maxEDegree : ℕ∞ :=
+  ⨆ v, G.edegree v
+
+/-- The minimum extended degree of all vertices, or `⊤` if there are no vertices -/
+noncomputable def minEDegree : ℕ∞ :=
+  ⨅ v, G.edegree v
+
+theorem maxEDegree_eq_iSup : G.maxEDegree = ⨆ v, G.edegree v := by
+  rfl
+
+theorem minEDegree_eq_iInf : G.minEDegree = ⨅ v, G.edegree v := by
+  rfl
+
+variable {G} in
+@[simp]
+theorem maxEDegree_eq_zero_iff_eq_bot : G.maxEDegree = 0 ↔ G = ⊥ := by
+  simp [maxEDegree_eq_iSup, eq_bot_iff_isIsolated]
+
+variable {G} in
+theorem minEDegree_eq_zero_iff_isIsolated : G.minEDegree = 0 ↔ ∃ v, G.IsIsolated v := by
+  simp [minEDegree_eq_iInf]
+
+variable {G} in
+theorem minEDegree_eq_zero_iff_support_ne : G.minEDegree = 0 ↔ G.support ≠ .univ := by
+  simp [minEDegree_eq_iInf, Set.ne_univ_iff_exists_notMem, notMem_support_iff_isIsolated]
+
+variable {G} in
+theorem maxEDegree_eq_top_iff_lt : G.maxEDegree = ⊤ ↔ ∀ n : ℕ, ∃ v, n < G.edegree v :=
+  WithTop.iSup_eq_top_iff_lt
+
+variable {G} in
+theorem maxEDegree_eq_top_iff_le : G.maxEDegree = ⊤ ↔ ∀ n : ℕ, ∃ v, n ≤ G.edegree v :=
+  WithTop.iSup_eq_top_iff_le
+
+variable {G} in
+theorem minEDegree_eq_top_iff : G.minEDegree = ⊤ ↔ ∀ v, G.edegree v = ⊤ :=
+  iInf_eq_top
+
+theorem exists_edegree_eq_maxEDegree [Nonempty V] (G : SimpleGraph V) (h : G.maxEDegree ≠ ⊤) :
+    ∃ v, G.edegree v = G.maxEDegree :=
+  Set.range_nonempty G.edegree |>.csSup_mem <| ENat.finite_of_sSup_lt_top h.lt_top
+
+theorem exists_edegree_eq_minEDegree [Nonempty V] (G : SimpleGraph V) :
+    ∃ v, G.edegree v = G.minEDegree :=
+  ciInf_mem G.edegree
+
+theorem edegree_le_maxEDegree : G.edegree v ≤ G.maxEDegree :=
+  le_iSup G.edegree v
+
+theorem minEDegree_le_edegree : G.minEDegree ≤ G.edegree v :=
+  iInf_le G.edegree v
+
+variable {G v} in
+theorem maxEDegree_eq_top_of_edegree_eq_top (h : G.edegree v = ⊤) : G.maxEDegree = ⊤ :=
+  eq_top_iff.mpr <| G.edegree_le_maxEDegree v |>.trans_eq' h
+
+variable {G v} in
+theorem minEDegree_eq_zero_of_edegree_eq_zero (h : G.edegree v = 0) : G.minEDegree = 0 :=
+  nonpos_iff_eq_zero.mp <| G.minEDegree_le_edegree v |>.trans_eq h
+
+variable {G} in
+theorem maxEDegree_le_of_forall_edegree_le {n : ℕ∞} (h : ∀ v, G.edegree v ≤ n) : G.maxEDegree ≤ n :=
+  iSup_le h
+
+variable {G} in
+theorem le_minEDegree_of_forall_le_edegree {n : ℕ∞} (h : ∀ v, n ≤ G.edegree v) : n ≤ G.minEDegree :=
+  le_iInf h
+
+@[simp]
+theorem maxEDegree_of_subsingleton [Subsingleton V] (G : SimpleGraph V) : G.maxEDegree = 0 := by
+  simp [maxEDegree_eq_iSup]
+
+@[simp]
+theorem minEDegree_of_isEmpty [IsEmpty V] (G : SimpleGraph V) : G.minEDegree = ⊤ :=
+  iInf_of_empty G.edegree
+
+@[simp]
+theorem minEDegree_of_subsingleton_of_nonempty [Subsingleton V] [Nonempty V] (G : SimpleGraph V) :
+    G.minEDegree = 0 := by
+  simp [minEDegree_eq_iInf]
+
+theorem maxEDegree_ne_top_of_finite [Finite V] (G : SimpleGraph V) : G.maxEDegree ≠ ⊤ :=
+  iSup_ne_top G.edegree_ne_top_of_finite
+
+theorem minEDegree_ne_top_of_finite [Nonempty V] [Finite V] (G : SimpleGraph V) :
+    G.minEDegree ≠ ⊤ := by
+  rw [minEDegree_eq_iInf, ne_eq, iInf_eq_top, not_forall]
+  have ⟨v⟩ := ‹Nonempty V›
+  exact ⟨v, G.edegree_ne_top_of_finite v⟩
+
+theorem coe_maxDegree_eq_maxEDegree [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] :
+    G.maxDegree = G.maxEDegree := by
+  cases isEmpty_or_nonempty V
+  · simp
+  rw [maxEDegree_eq_iSup, maxDegree, ← Finset.coe_max' <| by simp, Finset.max'_eq_sup',
+    Finset.sup'_image, Finset.sup'_univ_eq_ciSup]
+  simpa [← coe_degree_eq_edegree] using ENat.coe_iSup <| Set.finite_range _ |>.bddAbove
+
+theorem coe_minDegree_eq_minEDegree [Nonempty V] [Fintype V] (G : SimpleGraph V)
+    [DecidableRel G.Adj] : G.minDegree = G.minEDegree := by
+  rw [minEDegree_eq_iInf, minDegree, ← Finset.coe_min' <| by simp, Finset.min'_eq_inf',
+    Finset.inf'_image, Finset.inf'_univ_eq_ciInf]
+  simpa [← coe_degree_eq_edegree] using! ENat.coe_iInf
+
+variable {G} in
+theorem maxEDegree_eq_coe_iff [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {n : ℕ} :
+    G.maxEDegree = n ↔ G.maxDegree = n := by
+  simp [← coe_maxDegree_eq_maxEDegree]
+
+variable {G} in
+theorem minEDegree_eq_coe_iff [Nonempty V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj]
+    {n : ℕ} : G.minEDegree = n ↔ G.minDegree = n := by
+  simp [← coe_minDegree_eq_minEDegree]
+
+variable {G} in
+theorem minEDegree_eq_coe_iff_of_neZero [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {n : ℕ}
+    [NeZero n] : G.minEDegree = n ↔ G.minDegree = n := by
+  cases isEmpty_or_nonempty V
+  · simpa using NeZero.ne' n
+  simp [← coe_minDegree_eq_minEDegree]
+
+@[simp]
+theorem toNat_maxEDegree [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] :
+    G.maxEDegree.toNat = G.maxDegree := by
+  simp [← coe_maxDegree_eq_maxEDegree]
+
+@[simp]
+theorem toNat_minEDegree [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] :
+    G.minEDegree.toNat = G.minDegree := by
+  cases isEmpty_or_nonempty V
+  · simp
+  simp [← coe_minDegree_eq_minEDegree]
+
+variable {G H} in
+theorem IsContained.maxEDegree_le (h : G ⊑ H) : G.maxEDegree ≤ H.maxEDegree := by
+  refine G.maxEDegree_le_of_forall_edegree_le fun v ↦ ?_
+  grw [h.some.edegree_le, edegree_le_maxEDegree]
+
+variable {G H} in
+theorem Copy.minEDegree_le {f : Copy G H} (hf : Function.Surjective f) :
+    G.minEDegree ≤ H.minEDegree := by
+  refine H.le_minEDegree_of_forall_le_edegree fun w ↦ ?_
+  obtain ⟨v, rfl⟩ := hf w
+  grw [← f.edegree_le, ← minEDegree_le_edegree]
+
+variable {G H} in
+theorem Hom.minEDegree_le {f : G →g H} (hf : Function.Bijective f) : G.minEDegree ≤ H.minEDegree :=
+  Copy.minEDegree_le (f := ⟨f, hf.injective⟩) hf.surjective
+
+variable {G H} in
+theorem Iso.maxEDegree_eq (f : G ≃g H) : G.maxEDegree = H.maxEDegree :=
+  f.toEquiv.iSup_congr f.edegree_eq
+
+variable {G H} in
+theorem Iso.minEDegree_eq (f : G ≃g H) : G.minEDegree = H.minEDegree :=
+  f.toEquiv.iInf_congr f.edegree_eq
+
+variable {G G'} in
+@[gcongr]
+theorem maxEDegree_mono (hle : G ≤ G') : G.maxEDegree ≤ G'.maxEDegree :=
+  IsContained.of_le hle |>.maxEDegree_le
+
+variable {G G'} in
+@[gcongr]
+theorem minEDegree_mono (hle : G ≤ G') : G.minEDegree ≤ G'.minEDegree :=
+  Hom.ofLE hle |>.minEDegree_le Function.bijective_id
+
+theorem maxEDegree_le_card : G.maxEDegree ≤ ENat.card V :=
+  G.maxEDegree_le_of_forall_edegree_le G.edegree_le_card
+
+theorem minEDegree_le_card [Nonempty V] (G : SimpleGraph V) : G.minEDegree ≤ ENat.card V := by
+  have ⟨v⟩ := ‹Nonempty V›
+  grw [G.minEDegree_le_edegree v, edegree_le_card]
+
+variable {G} in
+theorem maxEDegree_lt_card_of_ne_top [Nonempty V] (G : SimpleGraph V) (h : G.maxEDegree ≠ ⊤) :
+    G.maxEDegree < ENat.card V := by
+  have ⟨v, hv⟩ := G.exists_edegree_eq_maxEDegree h
+  rw [← hv] at h ⊢
+  exact G.edegree_lt_card_of_ne_top h
+
+variable {G} in
+theorem minEDegree_lt_card_of_ne_top (h : G.minEDegree ≠ ⊤) : G.minEDegree < ENat.card V := by
+  cases isEmpty_or_nonempty V
+  · simp at h
+  have ⟨v, hv⟩ := G.exists_edegree_eq_minEDegree
+  rw [← hv] at h ⊢
+  exact G.edegree_lt_card_of_ne_top h
+
+theorem minEDegree_le_encard_edgeSet [Nonempty V] (G : SimpleGraph V) :
+    G.minEDegree ≤ G.edgeSet.encard := by
+  have ⟨v, hv⟩ := G.exists_edegree_eq_minEDegree
+  exact hv ▸ G.edegree_le_encard_edgeSet v
+
+theorem maxEDegree_le_encard_edgeSet : G.maxEDegree ≤ G.edgeSet.encard :=
+  maxEDegree_le_of_forall_edegree_le G.edegree_le_encard_edgeSet
+
+theorem minEDegree_le_maxEDegree [Nonempty V] (G : SimpleGraph V) :
+    G.minEDegree ≤ G.maxEDegree := by
+  have ⟨v⟩ := ‹Nonempty V›
+  grw [G.minEDegree_le_edegree v, edegree_le_maxEDegree]
+
+@[simp]
+theorem maxEDegree_top : (completeGraph V).maxEDegree = ENat.card V - 1 := by
+  cases isEmpty_or_nonempty V
+  · simp [ENat.card_eq_zero_iff_empty V |>.mpr ‹_›]
+  simp [maxEDegree_eq_iSup]
+
+@[simp]
+theorem minEDegree_top [Nonempty V] : (completeGraph V).minEDegree = ENat.card V - 1 := by
+  simp [minEDegree_eq_iInf]
+
+@[simp]
+theorem maxEDegree_bot : (emptyGraph V).maxEDegree = 0 := by
+  simp [maxEDegree_eq_iSup]
+
+@[simp]
+theorem minEDegree_bot [Nonempty V] : (emptyGraph V).minEDegree = 0 := by
+  simp [minEDegree_eq_iInf]
+
+variable {G} in
+theorem IsRegularOfDegree.maxEDegree_eq [Nonempty V] [G.LocallyFinite] {d : ℕ}
+    (h : G.IsRegularOfDegree d) : G.maxEDegree = d := by
+  simp [maxEDegree_eq_iSup, h.edegree_eq]
+
+variable {G} in
+theorem IsRegularOfDegree.minEDegree_eq [Nonempty V] [G.LocallyFinite] {d : ℕ}
+    (h : G.IsRegularOfDegree d) : G.minEDegree = d := by
+  simp [minEDegree_eq_iInf, h.edegree_eq]
+
+section Induce
+
+variable {s : Set V}
+
+variable {G} in
+theorem edegree_induce_of_neighborSet_subset {v : s} (h : G.neighborSet v ⊆ s) :
+    (G.induce s).edegree v = G.edegree v := by
+  rw [← encard_neighborSet, ← encard_neighborSet, neighborSet_induce,
+    Set.encard_preimage_of_injective_subset_range Subtype.val_injective <| by simpa]
+
+variable {G} in
+theorem maxEDegree_induce_of_support_subset (h : G.support ⊆ s) :
+    (G.induce s).maxEDegree = G.maxEDegree := by
+  apply le_antisymm <| Embedding.induce s |>.isContained.maxEDegree_le
+  refine G.maxEDegree_le_of_forall_edegree_le fun v ↦ ?_
+  by_cases hv : G.IsIsolated v
+  · simp [hv]
+  grw [← edegree_le_maxEDegree _ ⟨v, h <| G.mem_support_iff_not_isIsolated.mpr hv⟩,
+    edegree_induce_of_neighborSet_subset <| G.neighborSet_subset_support v |>.trans h]
+
+variable {G} in
+theorem le_minEDegree_induce_of_support_subset (h : G.support ⊆ s) :
+    G.minEDegree ≤ (G.induce s).minEDegree := by
+  refine le_minEDegree_of_forall_le_edegree fun v ↦ ?_
+  grw [G.minEDegree_le_edegree v, edegree_induce_of_neighborSet_subset]
+  grw [neighborSet_subset_support, h]
+
+end Induce
+
+end SimpleGraph
diff --git a/Mathlib/Combinatorics/SimpleGraph/Finite.lean b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
index e8b42995533a41..ad441e596f6dce 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Finite.lean
+++ b/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,11 @@ 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
 
+-- #40624
+@[simp]
+theorem ncard_neighborSet : (G.neighborSet v).ncard = G.degree v := by
+  simp [Set.ncard_eq_toFinset_card', card_neighborSet_eq_degree, -Set.fintypeCard_eq_ncard]
+
 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 +256,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
@@ -485,7 +490,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_coe]
 
 @[simp]
 lemma minDegree_bot_eq_zero : (⊥ : SimpleGraph V).minDegree = 0 :=
@@ -545,7 +550,14 @@ 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]
+
+-- #40624
+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
diff --git a/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean b/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
index b95034f8a5fc9c..d92a15ea0e729b 100644
--- a/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
+++ b/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]
 
 theorem incMatrix_mul_transpose_diag [Fintype (Sym2 α)] [Fintype (neighborSet G a)] :
     (G.incMatrix R * (G.incMatrix R)ᵀ) a a = G.degree a := by
diff --git a/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean b/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
index bc9ccfecd07846..7caefefe14ed3c 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
+++ b/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
 
diff --git a/Mathlib/Order/SuccPred/CompleteLinearOrder.lean b/Mathlib/Order/SuccPred/CompleteLinearOrder.lean
index 10c2c2e1f76a4b..4b304e3d3fe4ca 100644
--- a/Mathlib/Order/SuccPred/CompleteLinearOrder.lean
+++ b/Mathlib/Order/SuccPred/CompleteLinearOrder.lean
@@ -165,4 +165,36 @@ lemma exists_eq_iInf_of_not_isPredPrelimit (hf : ¬ IsPredPrelimit (⨅ i, f i))
     ∃ i, f i = ⨅ i, f i :=
   sInf_mem_of_not_isPredPrelimit hf
 
+-- #38612
+theorem Order.IsSuccPrelimit.le_sSup_iff {l : α} (h : IsSuccPrelimit l) :
+    l ≤ sSup s ↔ IsCofinalFor (Iio l) s := by
+  simp_rw [le_sSup_iff_forall_lt, IsCofinalFor, mem_Iio]
+  grind [lt_iff_exists_lt]
+
 end CompleteLinearOrder
+
+namespace WithTop
+
+variable [ConditionallyCompleteLinearOrderBot α]
+
+-- #40620
+theorem sSup_eq_top_iff_lt {s : Set (WithTop α)} : sSup s = ⊤ ↔ ∀ a : α, ∃ b ∈ s, a < b := by
+  rw [sSup_eq_top]
+  exact forall_lt_top
+
+-- #40620
+theorem iSup_eq_top_iff_lt {f : ι → WithTop α} : iSup f = ⊤ ↔ ∀ a : α, ∃ i, a < f i :=
+  sSup_eq_top_iff_lt.trans <| forall_congr' fun _ ↦ exists_range_iff
+
+-- #40620
+theorem sSup_eq_top_iff_le [NoMaxOrder α] {s : Set (WithTop α)} :
+    sSup s = ⊤ ↔ ∀ a : α, ∃ b ∈ s, a ≤ b := by
+  rw [eq_top_iff, isSuccPrelimit_top.le_sSup_iff]
+  exact forall_lt_top
+
+-- #40620
+theorem iSup_eq_top_iff_le [NoMaxOrder α] {f : ι → WithTop α} :
+    iSup f = ⊤ ↔ ∀ a : α, ∃ i, a ≤ f i :=
+  sSup_eq_top_iff_le.trans <| forall_congr' fun _ ↦ exists_range_iff
+
+end WithTop
diff --git a/Mathlib/Order/WithBot.lean b/Mathlib/Order/WithBot.lean
index 330fe865bdd45f..44611e79aae008 100644
--- a/Mathlib/Order/WithBot.lean
+++ b/Mathlib/Order/WithBot.lean
@@ -508,6 +508,12 @@ lemma lt_unbotA_iff [Nonempty α] (hx : x ≠ ⊥) : a < x.unbotA ↔ a < x := l
 lemma unbotA_lt_iff [Nonempty α] (hx : x ≠ ⊥) : x.unbotA < a ↔ x < a := by
   lift x to α using hx; simp
 
+-- #40620
+@[to_dual forall_lt_top]
+theorem forall_bot_lt {p : WithBot α → Prop} : (∀ a, ⊥ < a → p a) ↔ (∀ a : α, p a) := by
+  simp_rw [WithBot.bot_lt_iff_ne_bot]
+  exact forall_ne_bot
+
 end LT
 
 @[to_dual]