fix StronglyRegular.lean

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -953,7 +953,7 @@ theorem exists_adj_iff_not_isIsolated : (∃ u, G.Adj v u) ↔ ¬G.IsIsolated v
 @[simp]
 theorem IsIsolated.of_subsingleton [Subsingleton V] (G : SimpleGraph V) (v : V) :
     G.IsIsolated v :=
-  fun _ hadj ↦ not_nontrivial V <| hadj.nontrivial
+  fun _ hadj ↦ not_nontrivial V hadj.nontrivial
 
 variable {G} in
 theorem nontrivial_of_not_isIsolated (h : ¬G.IsIsolated v) : Nontrivial V :=

Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean

@@ -64,7 +64,7 @@ theorem bot_strongly_regular : (⊥ : SimpleGraph V).IsSRGWith (Fintype.card V)
   of_not_adj v w _ := by
     simp only [card_eq_zero, Fintype.card_ofFinset, forall_true_left, not_false_iff, bot_adj]
     ext
-    simp [mem_commonNeighbors]
+    simp
 
 theorem IsSRGWith.ediam_eq_two [Nontrivial V] (h : G.IsSRGWith n k ℓ μ) (ht : G ≠ ⊤) (hm : μ ≠ 0) :
     G.ediam = 2 := by