diff --git a/Mathlib/Combinatorics/SimpleGraph/Operations.lean b/Mathlib/Combinatorics/SimpleGraph/Operations.lean
index 229f12b14227d..51585ff75cd2f 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Operations.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Operations.lean
@@ -157,6 +157,7 @@ instance : Fintype (edge s t).edgeSet := by rw [edge]; infer_instance
 
 theorem edgeFinset_sup_edge [Fintype (edgeSet (G ⊔ edge s t))] (hn : ¬G.Adj s t) (h : s ≠ t) :
     (G ⊔ edge s t).edgeFinset = G.edgeFinset.cons s(s, t) (by simp_all) := by
+  letI := Classical.decEq V
   rw [edgeFinset_sup, cons_eq_insert, insert_eq, union_comm]
   simp_rw [edgeFinset, edge_edgeSet_of_ne h]; rfl
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean b/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
index 0d49e2b8b66c1..4d5eb29b4fb4a 100644
--- a/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
@@ -183,6 +183,7 @@ set_option linter.uppercaseLean3 false in
 `k * (k - ℓ - 1) = (n - k - 1) * μ`. -/
 theorem IsSRGWith.param_eq (h : G.IsSRGWith n k ℓ μ) (hn : 0 < n) :
     k * (k - ℓ - 1) = (n - k - 1) * μ := by
+  letI := Classical.decEq V
   rw [← h.card, Fintype.card_pos_iff] at hn
   obtain ⟨v⟩ := hn
   convert card_mul_eq_card_mul G.Adj (s := G.neighborFinset v) (t := Gᶜ.neighborFinset v) _ _