chore(SimpleGraph/Finite): drop some DecidableEq assumptions (#10441)

- don't assume `DecidableEq` in `card_edgeFinset_le_card_choose_two`;
- make `edgeFinset_deleteEdges` work with any `Fintype G.edgeSet`
  and `Fintype (G.deleteEdges s).edgeSet` instances;
- don't assume `DecidbaleEq` in theorems about `DeleteFar`.

Author: urkud

Mathlib/Combinatorics/SimpleGraph/Finite.lean

@@ -114,28 +114,28 @@ theorem edgeSet_univ_card : (univ : Finset G.edgeSet).card = G.edgeFinset.card :
   Fintype.card_of_subtype G.edgeFinset fun _ => mem_edgeFinset
 #align simple_graph.edge_set_univ_card SimpleGraph.edgeSet_univ_card
 
-variable [Fintype V] [DecidableEq V]
+variable [Fintype V]
 
 @[simp]
-theorem edgeFinset_top : (⊤ : SimpleGraph V).edgeFinset = univ.filter fun e => ¬e.IsDiag := by
+theorem edgeFinset_top [DecidableEq V] :
+    (⊤ : SimpleGraph V).edgeFinset = univ.filter fun e => ¬e.IsDiag := by
   rw [← coe_inj]; simp
 
 /-- The complete graph on `n` vertices has `n.choose 2` edges. -/
-theorem card_edgeFinset_top_eq_card_choose_two :
+theorem card_edgeFinset_top_eq_card_choose_two [DecidableEq V] :
     (⊤ : SimpleGraph V).edgeFinset.card = (Fintype.card V).choose 2 := by
   simp_rw [Set.toFinset_card, edgeSet_top, Set.coe_setOf, ← Sym2.card_subtype_not_diag]
 
 /-- Any graph on `n` vertices has at most `n.choose 2` edges. -/
 theorem card_edgeFinset_le_card_choose_two : G.edgeFinset.card ≤ (Fintype.card V).choose 2 := by
+  classical
   rw [← card_edgeFinset_top_eq_card_choose_two]
   exact card_le_card (edgeFinset_mono le_top)
 
 end EdgeFinset
 
--- porting note: added `Fintype (Sym2 V)` argument rather than have it be inferred.
--- As a consequence, deleted the `Fintype V` argument.
-theorem edgeFinset_deleteEdges [Fintype (Sym2 V)] [DecidableEq V] [DecidableRel G.Adj]
-    (s : Finset (Sym2 V)) [DecidableRel (G.deleteEdges s).Adj] :
+theorem edgeFinset_deleteEdges [DecidableEq V] [Fintype G.edgeSet] (s : Finset (Sym2 V))
+    [Fintype (G.deleteEdges s).edgeSet] :
     (G.deleteEdges s).edgeFinset = G.edgeFinset \ s := by
   ext e
   simp [edgeSet_deleteEdges]
@@ -144,8 +144,8 @@ theorem edgeFinset_deleteEdges [Fintype (Sym2 V)] [DecidableEq V] [DecidableRel
 section DeleteFar
 
 -- porting note: added `Fintype (Sym2 V)` argument.
-variable {𝕜 : Type*} [OrderedRing 𝕜] [Fintype V] [Fintype (Sym2 V)] [DecidableEq V]
-  [DecidableRel G.Adj] {p : SimpleGraph V → Prop} {r r₁ r₂ : 𝕜}
+variable {𝕜 : Type*} [OrderedRing 𝕜] [Fintype V] [Fintype (Sym2 V)]
+  [Fintype G.edgeSet] {p : SimpleGraph V → Prop} {r r₁ r₂ : 𝕜}
 
 /-- A graph is `r`-*delete-far* from a property `p` if we must delete at least `r` edges from it to
 get a graph with the property `p`. -/
@@ -158,6 +158,7 @@ variable {G}
 theorem deleteFar_iff :
     G.DeleteFar p r ↔ ∀ ⦃H : SimpleGraph _⦄ [DecidableRel H.Adj],
       H ≤ G → p H → r ≤ G.edgeFinset.card - H.edgeFinset.card := by
+  classical
   refine ⟨fun h H _ hHG hH ↦ ?_, fun h s hs hG ↦ ?_⟩
   · have := h (sdiff_subset G.edgeFinset H.edgeFinset)
     simp only [deleteEdges_sdiff_eq_of_le _ hHG, edgeFinset_mono hHG, card_sdiff,