@[simp] fixes and min degree = 0 iff corrections

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -926,6 +926,7 @@ lemma mem_support_iff_not_isIsolated : v ∈ G.support ↔ ¬ G.IsIsolated v :=
   simp [mem_support, IsIsolated]
 
 -- #38747
+@[simp]
 theorem notMem_support_iff_isIsolated : v ∉ G.support ↔ G.IsIsolated v := by
   simp [mem_support_iff_not_isIsolated]
 

Mathlib/Combinatorics/SimpleGraph/Degree.lean

@@ -39,6 +39,7 @@ variable {G v} in
 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
@@ -53,10 +54,9 @@ 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
 
-@[simp]
 theorem edegree_eq_zero_of_subsingleton [Subsingleton V] (G : SimpleGraph V) (v : V) :
-    G.edegree v = 0 :=
-  edegree_eq_zero_iff_isIsolated.mpr <| .of_subsingleton G 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
@@ -119,9 +119,8 @@ 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
 
-@[simp]
 theorem edegree_bot : edegree ⊥ v = 0 := by
-  simp [← encard_neighborSet]
+  simp
 
 variable {G} in
 theorem IsRegularOfDegree.edegree_eq [G.LocallyFinite] {d : ℕ} (h : G.IsRegularOfDegree d) (v : V) :
@@ -147,6 +146,10 @@ variable {G} in
 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]

Mathlib/Combinatorics/SimpleGraph/Finite.lean

@@ -500,10 +500,15 @@ lemma minDegree_bot_eq_zero : (⊥ : SimpleGraph V).minDegree = 0 :=
 
 variable {G} in
 theorem minDegree_eq_zero_iff [DecidableRel G.Adj] [Nonempty V] :
-    G.minDegree = 0 ↔ ∃ v, G.degree v = 0 := by
+    G.minDegree = 0 ↔ ∃ v, G.IsIsolated v := by
   refine ⟨fun h ↦ ?_, fun ⟨v, hv⟩ ↦ ?_⟩
-  · grind [G.exists_minimal_degree_vertex]
-  · grind [G.minDegree_le_degree v]
+  · grind [G.exists_minimal_degree_vertex, degree_eq_zero]
+  · grind [G.minDegree_le_degree v, degree_eq_zero]
+
+variable {G} in
+theorem minDegree_eq_zero_iff_support_ne [DecidableRel G.Adj] [Nonempty V] :
+    G.minDegree = 0 ↔ G.support ≠ .univ := by
+  simp [Set.ne_univ_iff_exists_notMem, minDegree_eq_zero_iff]
 
 @[simp]
 lemma minDegree_top [DecidableEq V] : (⊤ : SimpleGraph V).minDegree = Fintype.card V - 1 := by