tag notMem_support_iff_isIsolated as simp

SnirBroshi · web-flow · commit ed013006ffdf · 2026-05-01T02:46:28.000+03:00
diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean
@@ -939,6 +939,7 @@ attribute [simp] IsIsolated.neighborSet_eq_empty
 lemma mem_support_iff_not_isIsolated : v ∈ G.support ↔ ¬ G.IsIsolated v := by
   simp [mem_support, IsIsolated]
 
+@[simp]
 theorem notMem_support_iff_isIsolated : v ∉ G.support ↔ G.IsIsolated v := by
   simp [mem_support_iff_not_isIsolated]
 
