chore(SimpleGraph): fix DecidableEq/Fintype assumptions (#16079)

Found by a linter in #10235
Mostly repeats @grunweg's  #15306 accidentally reverted by @semorrison's #15726

Author: urkud

Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean

@@ -58,8 +58,6 @@ theorem set_walk_length_succ_eq (u v : V) (n : ℕ) :
     · rintro ⟨w, huw, pwv, rfl, rfl, rfl⟩
       rfl
 
-variable [DecidableEq V]
-
 /-- Walks of length two from `u` to `v` correspond bijectively to common neighbours of `u` and `v`.
 Note that `u` and `v` may be the same. -/
 @[simps]
@@ -73,7 +71,7 @@ def walkLengthTwoEquivCommonNeighbors (u v : V) :
 
 section LocallyFinite
 
-variable [LocallyFinite G]
+variable [DecidableEq V] [LocallyFinite G]
 
 /-- The `Finset` of length-`n` walks from `u` to `v`.
 This is used to give `{p : G.walk u v | p.length = n}` a `Fintype` instance, and it
@@ -143,7 +141,7 @@ end LocallyFinite
 
 section Finite
 
-variable [Fintype V] [DecidableRel G.Adj]
+variable [DecidableEq V] [Fintype V] [DecidableRel G.Adj]
 
 theorem reachable_iff_exists_finsetWalkLength_nonempty (u v : V) :
     G.Reachable u v ↔ ∃ n : Fin (Fintype.card V), (G.finsetWalkLength n u v).Nonempty := by
@@ -172,8 +170,12 @@ instance instDecidableMemSupp (c : G.ConnectedComponent) (v : V) : Decidable (v
   c.recOn (fun w ↦ decidable_of_iff (G.Reachable v w) <| by simp)
     (fun _ _ _ _ ↦ Subsingleton.elim _ _)
 
-lemma odd_card_iff_odd_components : Odd (Nat.card V) ↔
+end Finite
+
+lemma odd_card_iff_odd_components [Finite V] : Odd (Nat.card V) ↔
     Odd (Nat.card ({(c : ConnectedComponent G) | Odd (Nat.card c.supp)})) := by
+  classical
+  cases nonempty_fintype V
   rw [Nat.card_eq_fintype_card]
   simp only [← (set_fintype_card_eq_univ_iff _).mpr G.iUnion_connectedComponentSupp,
     ConnectedComponent.mem_supp_iff, Fintype.card_subtype_compl,
@@ -184,8 +186,6 @@ lemma odd_card_iff_odd_components : Odd (Nat.card V) ↔
   rw [Nat.card_eq_fintype_card, Fintype.card_ofFinset]
   exact (Finset.odd_sum_iff_odd_card_odd (fun x : G.ConnectedComponent ↦ Nat.card x.supp))
 
-end Finite
-
 end WalkCounting
 
 end SimpleGraph

Mathlib/Combinatorics/SimpleGraph/Turan.lean

@@ -124,7 +124,7 @@ end Defs
 
 namespace IsTuranMaximal
 
-variable {s t u : V} [DecidableEq V]
+variable {s t u : V}
 
 /-- In a Turán-maximal graph, non-adjacent vertices have the same degree. -/
 lemma degree_eq_of_not_adj (h : G.IsTuranMaximal r) (hn : ¬G.Adj s t) :
@@ -186,15 +186,15 @@ instance : DecidableRel h.setoid.r :=
 /-- The finpartition derived from `h.setoid`. -/
 def finpartition [DecidableEq V] : Finpartition (univ : Finset V) := Finpartition.ofSetoid h.setoid
 
-lemma not_adj_iff_part_eq :
+lemma not_adj_iff_part_eq [DecidableEq V] :
     ¬G.Adj s t ↔ h.finpartition.part s = h.finpartition.part t := by
   change h.setoid.r s t ↔ _
   rw [← Finpartition.mem_part_ofSetoid_iff_rel]
   let fp := h.finpartition
   change t ∈ fp.part s ↔ fp.part s = fp.part t
   rw [fp.mem_part_iff_part_eq_part (mem_univ t) (mem_univ s), eq_comm]
 
-lemma degree_eq_card_sub_part_card :
+lemma degree_eq_card_sub_part_card [DecidableEq V] :
     G.degree s = Fintype.card V - (h.finpartition.part s).card :=
   calc
     _ = (univ.filter (G.Adj s)).card := by
@@ -207,7 +207,7 @@ lemma degree_eq_card_sub_part_card :
       simp [setoid]
 
 /-- The parts of a Turán-maximal graph form an equipartition. -/
-theorem isEquipartition : h.finpartition.IsEquipartition := by
+theorem isEquipartition [DecidableEq V] : h.finpartition.IsEquipartition := by
   set fp := h.finpartition
   by_contra hn
   rw [Finpartition.not_isEquipartition] at hn
@@ -227,7 +227,7 @@ theorem isEquipartition : h.finpartition.IsEquipartition := by
   have : large.card ≤ Fintype.card V := by simpa using card_le_card large.subset_univ
   omega
 
-lemma card_parts_le : h.finpartition.parts.card ≤ r := by
+lemma card_parts_le [DecidableEq V] : h.finpartition.parts.card ≤ r := by
   by_contra! l
   obtain ⟨z, -, hz⟩ := h.finpartition.exists_subset_part_bijOn
   have ncf : ¬G.CliqueFree z.card := by
@@ -240,7 +240,7 @@ lemma card_parts_le : h.finpartition.parts.card ≤ r := by
 /-- There are `min n r` parts in a graph on `n` vertices satisfying `G.IsTuranMaximal r`.
 `min` handles the `n < r` case, when `G` is complete but still `r + 1`-cliquefree
 for having insufficiently many vertices. -/
-theorem card_parts : h.finpartition.parts.card = min (Fintype.card V) r := by
+theorem card_parts [DecidableEq V] : h.finpartition.parts.card = min (Fintype.card V) r := by
   set fp := h.finpartition
   apply le_antisymm (le_min fp.card_parts_le_card h.card_parts_le)
   by_contra! l
@@ -280,8 +280,6 @@ theorem nonempty_iso_turanGraph :
 
 end IsTuranMaximal
 
-variable [DecidableEq V]
-
 /-- **Turán's theorem**, reverse direction.
 
 Any graph isomorphic to `turanGraph n r` is itself Turán-maximal if `0 < r`. -/
@@ -293,7 +291,7 @@ theorem isTuranMaximal_of_iso (f : G ≃g turanGraph n r) (hr : 0 < r) : G.IsTur
     fun H _ cf ↦ (f.symm.comp g).card_edgeFinset_eq ▸ j.2 H cf
 
 /-- Turán-maximality with `0 < r` transfers across graph isomorphisms. -/
-theorem IsTuranMaximal.iso {W : Type*} [DecidableEq W] [Fintype W] {H : SimpleGraph W}
+theorem IsTuranMaximal.iso {W : Type*} [Fintype W] {H : SimpleGraph W}
     [DecidableRel H.Adj] (h : G.IsTuranMaximal r) (f : G ≃g H) (hr : 0 < r) : H.IsTuranMaximal r :=
   isTuranMaximal_of_iso (h.nonempty_iso_turanGraph.some.comp f.symm) hr