chore(SimpleGraph/Regularity): Don't use Classical (#12575)

The classical decidability instances were found in theorem statements, making them harder to use.

Author: YaelDillies

Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean

@@ -38,13 +38,13 @@ Once ported to mathlib4, this file will be a great golfing ground for Heather's
 
 
 open Finpartition Finset Fintype Rel Nat
-
-open scoped BigOperators Classical SzemerediRegularity.Positivity
+open scoped BigOperators SzemerediRegularity.Positivity
 
 namespace SzemerediRegularity
 
-variable {α : Type*} [Fintype α] {P : Finpartition (univ : Finset α)} (hP : P.IsEquipartition)
-  (G : SimpleGraph α) (ε : ℝ) {U : Finset α} (hU : U ∈ P.parts) (V : Finset α)
+variable {α : Type*} [Fintype α] [DecidableEq α] {P : Finpartition (univ : Finset α)}
+  (hP : P.IsEquipartition) (G : SimpleGraph α) [DecidableRel G.Adj] (ε : ℝ) {U : Finset α}
+  (hU : U ∈ P.parts) (V : Finset α)
 
 local notation3 "m" => (card α / stepBound P.parts.card : ℕ)
 

Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean

@@ -38,10 +38,10 @@ Once ported to mathlib4, this file will be a great golfing ground for Heather's
 
 open Finset Fintype SimpleGraph SzemerediRegularity
 
-open scoped BigOperators Classical SzemerediRegularity.Positivity
+open scoped BigOperators SzemerediRegularity.Positivity
 
-variable {α : Type*} [Fintype α] {P : Finpartition (univ : Finset α)} (hP : P.IsEquipartition)
-  (G : SimpleGraph α) (ε : ℝ)
+variable {α : Type*} [Fintype α] [DecidableEq α] {P : Finpartition (univ : Finset α)}
+  (hP : P.IsEquipartition) (G : SimpleGraph α) [DecidableRel G.Adj] (ε : ℝ)
 
 local notation3 "m" => (card α / stepBound P.parts.card : ℕ)
 
@@ -77,8 +77,9 @@ theorem card_increment (hPα : P.parts.card * 16 ^ P.parts.card ≤ card α) (hP
   rw [filter_card_add_filter_neg_card_eq_card, card_attach]
 #align szemeredi_regularity.card_increment SzemerediRegularity.card_increment
 
-theorem increment_isEquipartition (hP : P.IsEquipartition) (G : SimpleGraph α) (ε : ℝ) :
-    (increment hP G ε).IsEquipartition := by
+variable (hP G ε)
+
+theorem increment_isEquipartition : (increment hP G ε).IsEquipartition := by
   simp_rw [IsEquipartition, Set.equitableOn_iff_exists_eq_eq_add_one]
   refine' ⟨m, fun A hA => _⟩
   rw [mem_coe, increment, mem_bind] at hA
@@ -87,12 +88,14 @@ theorem increment_isEquipartition (hP : P.IsEquipartition) (G : SimpleGraph α)
 #align szemeredi_regularity.increment_is_equipartition SzemerediRegularity.increment_isEquipartition
 
 /-- The contribution to `Finpartition.energy` of a pair of distinct parts of a `Finpartition`. -/
-private noncomputable def distinctPairs (G : SimpleGraph α) (ε : ℝ) (hP : P.IsEquipartition)
-    (x : {x // x ∈ P.parts.offDiag}) : Finset (Finset α × Finset α) :=
+private noncomputable def distinctPairs (x : {x // x ∈ P.parts.offDiag}) :
+    Finset (Finset α × Finset α) :=
   (chunk hP G ε (mem_offDiag.1 x.2).1).parts ×ˢ (chunk hP G ε (mem_offDiag.1 x.2).2.1).parts
 
+variable {hP G ε}
+
 private theorem distinctPairs_increment :
-    P.parts.offDiag.attach.biUnion (distinctPairs G ε hP) ⊆ (increment hP G ε).parts.offDiag := by
+    P.parts.offDiag.attach.biUnion (distinctPairs hP G ε) ⊆ (increment hP G ε).parts.offDiag := by
   rintro ⟨Ui, Vj⟩
   simp only [distinctPairs, increment, mem_offDiag, bind_parts, mem_biUnion, Prod.exists,
     exists_and_left, exists_prop, mem_product, mem_attach, true_and_iff, Subtype.exists, and_imp,
@@ -105,7 +108,7 @@ private theorem distinctPairs_increment :
 
 private lemma pairwiseDisjoint_distinctPairs :
     (P.parts.offDiag.attach : Set {x // x ∈ P.parts.offDiag}).PairwiseDisjoint
-      (distinctPairs G ε hP) := by
+      (distinctPairs hP G ε) := by
   simp (config := { unfoldPartialApp := true }) only [distinctPairs, Set.PairwiseDisjoint,
     Function.onFun, disjoint_left, inf_eq_inter, mem_inter, mem_product]
   rintro ⟨⟨s₁, s₂⟩, hs⟩ _ ⟨⟨t₁, t₂⟩, ht⟩ _ hst ⟨u, v⟩ huv₁ huv₂
@@ -124,7 +127,7 @@ lemma le_sum_distinctPairs_edgeDensity_sq (x : {i // i ∈ P.parts.offDiag}) (h
     (hPα : P.parts.card * 16 ^ P.parts.card ≤ card α) (hPε : ↑100 ≤ ↑4 ^ P.parts.card * ε ^ 5) :
     (G.edgeDensity x.1.1 x.1.2 : ℝ) ^ 2 +
       ((if G.IsUniform ε x.1.1 x.1.2 then 0 else ε ^ 4 / 3) - ε ^ 5 / 25) ≤
-    (∑ i in distinctPairs G ε hP x, G.edgeDensity i.1 i.2 ^ 2 : ℝ) / 16 ^ P.parts.card := by
+    (∑ i in distinctPairs hP G ε x, G.edgeDensity i.1 i.2 ^ 2 : ℝ) / 16 ^ P.parts.card := by
   rw [distinctPairs, ← add_sub_assoc, add_sub_right_comm]
   split_ifs with h
   · rw [add_zero]
@@ -144,9 +147,9 @@ theorem energy_increment (hP : P.IsEquipartition) (hP₇ : 7 ≤ P.parts.card)
     _ = (∑ x in P.parts.offDiag, (G.edgeDensity x.1 x.2 : ℝ) ^ 2 +
           P.parts.card ^ 2 * (ε ^ 5 / 4) : ℝ) / P.parts.card ^ 2 := by
         rw [coe_energy, add_div, mul_div_cancel_left₀]; positivity
-    _ ≤ (∑ x in P.parts.offDiag.attach, (∑ i in distinctPairs G ε hP x,
+    _ ≤ (∑ x in P.parts.offDiag.attach, (∑ i in distinctPairs hP G ε x,
           G.edgeDensity i.1 i.2 ^ 2 : ℝ) / 16 ^ P.parts.card) / P.parts.card ^ 2 := ?_
-    _ = (∑ x in P.parts.offDiag.attach, ∑ i in distinctPairs G ε hP x,
+    _ = (∑ x in P.parts.offDiag.attach, ∑ i in distinctPairs hP G ε x,
           G.edgeDensity i.1 i.2 ^ 2 : ℝ) / (increment hP G ε).parts.card ^ 2 := by
         rw [card_increment hPα hPG, coe_stepBound, mul_pow, pow_right_comm,
           div_mul_eq_div_div_swap, ← sum_div]; norm_num

Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean

@@ -66,9 +66,8 @@ We currently only prove the equipartition version of SRL.
 
 open Finpartition Finset Fintype Function SzemerediRegularity
 
-open scoped Classical
-
-variable {α : Type*} [Fintype α] (G : SimpleGraph α) {ε : ℝ} {l : ℕ}
+variable {α : Type*} [DecidableEq α] [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : ℝ}
+  {l : ℕ}
 
 /-- Effective **Szemerédi Regularity Lemma**: For any sufficiently large graph, there is an
 `ε`-uniform equipartition of bounded size (where the bound does not depend on the graph). -/