fix

Author: sgouezel

Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean

@@ -195,9 +195,10 @@ more often found in the literature, where `J` is the all-ones matrix. -/
 theorem IsSRGWith.matrix_eq {α : Type*} [Semiring α] (h : G.IsSRGWith n k ℓ μ) :
     G.adjMatrix α ^ 2 = k • (1 : Matrix V V α) + ℓ • G.adjMatrix α + μ • Gᶜ.adjMatrix α := by
   ext v w
-  simp only [adjMatrix_pow_apply_eq_card_walk, Set.coe_setOf, Matrix.add_apply, Matrix.smul_apply,
+  simp only [adjMatrix_pow_apply_eq_card_walk, Matrix.add_apply, Matrix.smul_apply,
     adjMatrix_apply, compl_adj]
-  erw [Fintype.card_congr (G.walkLengthTwoEquivCommonNeighbors v w)]
+  rw [@Fintype.card_congr _ _ (G.fintypeSetWalkLength v w 2) _
+    (G.walkLengthTwoEquivCommonNeighbors v w)]
   obtain rfl | hn := eq_or_ne v w
   · rw [← Set.toFinset_card]
     simp [commonNeighbors, ← neighborFinset_def, h.regular v]