upgrade lean 4.32 rc1

Graphon/Approximation.lean

@@ -208,17 +208,17 @@ noncomputable def MeasurablePartition.splitPart (P : MeasurablePartition α μ)
       · exact (P.measurableSet_part hS).diff hS₁_meas
     pairwiseDisjoint := fun T₁ hT₁ T₂ hT₂ hne => by
       simp only [Finset.coe_union, Finset.coe_erase, Finset.coe_insert,
-          Finset.coe_singleton, Set.mem_union, Set.mem_diff, Set.mem_singleton_iff,
+          Finset.coe_singleton, Set.mem_union, Set.mem_sdiff, Set.mem_singleton_iff,
           Set.mem_insert_iff] at hT₁ hT₂
       rcases hT₁ with ⟨hT₁_in, hT₁_ne⟩ | (hT₁_eq | hT₁_eq)
       <;> rcases hT₂ with ⟨hT₂_in, hT₂_ne⟩ | (hT₂_eq | hT₂_eq)
       · exact P.pairwiseDisjoint hT₁_in hT₂_in hne
       · subst hT₂_eq; exact (P.pairwiseDisjoint hT₁_in hS hT₁_ne).mono_right hS₁_sub
-      · subst hT₂_eq; exact (P.pairwiseDisjoint hT₁_in hS hT₁_ne).mono_right diff_subset
+      · subst hT₂_eq; exact (P.pairwiseDisjoint hT₁_in hS hT₁_ne).mono_right sdiff_subset
       · subst hT₁_eq; exact ((P.pairwiseDisjoint hT₂_in hS hT₂_ne).mono_right hS₁_sub).symm
       · subst hT₁_eq; subst hT₂_eq; exact absurd rfl hne
       · subst hT₁_eq; subst hT₂_eq; exact Set.disjoint_sdiff_right
-      · subst hT₁_eq; exact ((P.pairwiseDisjoint hT₂_in hS hT₂_ne).mono_right diff_subset).symm
+      · subst hT₁_eq; exact ((P.pairwiseDisjoint hT₂_in hS hT₂_ne).mono_right sdiff_subset).symm
       · subst hT₁_eq; subst hT₂_eq; exact Set.disjoint_sdiff_right.symm
       · subst hT₁_eq; subst hT₂_eq; exact absurd rfl hne
     ae_covers := by
@@ -243,7 +243,7 @@ theorem MeasurablePartition.splitPart_refines (P : MeasurablePartition α μ)
   rcases hT with ⟨_, hT_in⟩ | (rfl | rfl)
   · exact ⟨T, hT_in, Subset.refl T⟩
   · exact ⟨S, hS, hS₁_sub⟩
-  · exact ⟨S, hS, diff_subset⟩
+  · exact ⟨S, hS, sdiff_subset⟩
 
 /-- Splitting adds at most one part. -/
 theorem MeasurablePartition.splitPart_card (P : MeasurablePartition α μ)
@@ -297,17 +297,17 @@ noncomputable def MeasurablePartition.splitAllParts (P : MeasurablePartition α
       · by_cases h : S₁ = S₂
         · subst h; exact disjoint_inf_sdiff
         · exact (P.pairwiseDisjoint hS₁_mem hS₂_mem h).mono
-            Set.inter_subset_left Set.diff_subset
+            Set.inter_subset_left Set.sdiff_subset
       -- (S₁ \ A, S₂ ∩ A)
       · by_cases h : S₁ = S₂
         · subst h; exact disjoint_inf_sdiff.symm
         · exact (P.pairwiseDisjoint hS₁_mem hS₂_mem h).mono
-            Set.diff_subset Set.inter_subset_left
+            Set.sdiff_subset Set.inter_subset_left
       -- (S₁ \ A, S₂ \ A)
       · by_cases h : S₁ = S₂
         · subst h; exact absurd rfl hne
         · exact (P.pairwiseDisjoint hS₁_mem hS₂_mem h).mono
-            Set.diff_subset Set.diff_subset
+            Set.sdiff_subset Set.sdiff_subset
     ae_covers := by
       filter_upwards [P.ae_covers] with x ⟨S, hS_mem, hx⟩
       by_cases hxA : x ∈ A
@@ -328,7 +328,7 @@ theorem MeasurablePartition.splitAllParts_refines (P : MeasurablePartition α μ
       Finset.mem_singleton] at hT
   obtain ⟨S, hS_mem, rfl | rfl⟩ := hT
   · exact ⟨S, hS_mem, Set.inter_subset_left⟩
-  · exact ⟨S, hS_mem, Set.diff_subset⟩
+  · exact ⟨S, hS_mem, Set.sdiff_subset⟩
 
 omit [IsProbabilityMeasure μ] in
 /-- splitAllParts has at most 2 * P.parts.card parts. -/

Graphon/Basic.lean

@@ -214,7 +214,7 @@ variable [IsProbabilityMeasure μ]
 
 For a sequence of empty graphs `Gₙ` (graphs with no edges), the edge density
 between any two sets converges to 0, giving the graphon `W(x,y) = 0` for all `x,y`. -/
-def zero : Graphon α μ where
+noncomputable def zero : Graphon α μ where
   toAEEqFun := AEEqFun.const (α × α) 0
   symm' := by
     have h1 : ∀ᵐ p ∂(μ.prod μ), (AEEqFun.const (α × α) (0 : ℝ) : (α × α) →ₘ[μ.prod μ] ℝ) p = 0 :=
@@ -232,7 +232,7 @@ def zero : Graphon α μ where
 
 For a sequence of complete graphs `Kₙ`, the edge density between any two sets
 converges to 1, giving the graphon `W(x,y) = 1` for all `x,y`. -/
-def one : Graphon α μ where
+noncomputable def one : Graphon α μ where
   toAEEqFun := AEEqFun.const (α × α) 1
   symm' := by
     have h1 : ∀ᵐ p ∂(μ.prod μ), (AEEqFun.const (α × α) (1 : ℝ) : (α × α) →ₘ[μ.prod μ] ℝ) p = 1 :=
@@ -268,7 +268,7 @@ Key properties:
 If `W` is the graphon limit of graphs `Gₙ`, then `compl W` is the limit of the
 complement graphs `Ḡₙ`. The edge probability `W(x,y)` becomes the non-edge
 probability `1 - W(x,y)`. -/
-def compl (W : Graphon α μ) : Graphon α μ where
+noncomputable def compl (W : Graphon α μ) : Graphon α μ where
   toAEEqFun := AEEqFun.const (α × α) 1 - W.toAEEqFun
   symm' := by
     have hsub_ae : ∀ᵐ p ∂(μ.prod μ),
@@ -382,7 +382,7 @@ If `W₁(x,y) ∈ [0,1]` and `W₂(x,y) ∈ [0,1]` a.e., then
 
 This operation is fundamental for defining the cut distance:
 `δ□(U, W) = inf_φ ‖U - W^φ‖_□` where `W^φ` is a pullback of `W`. -/
-def sub (W₁ W₂ : Graphon α μ) : SignedGraphon α μ where
+noncomputable def sub (W₁ W₂ : Graphon α μ) : SignedGraphon α μ where
   toAEEqFun := W₁.toAEEqFun - W₂.toAEEqFun
   symm' := by
     have hsub_ae := AEEqFun.coeFn_sub W₁.toAEEqFun W₂.toAEEqFun

Graphon/Compactness.lean

@@ -561,7 +561,7 @@ theorem totallyBounded (ε : ℝ) (hε : ε > 0) :
       apply Filter.mem_of_superset (compl_mem_ae_iff.mpr h_null)
       intro x hx hxS
       by_contra h_ne
-      exact hx (Set.mem_diff_of_mem hxS h_ne)
+      exact hx (Set.mem_sdiff_of_mem hxS h_ne)
     have h_e_fst : ∀ᵐ p ∂(μ.prod μ),
         ∀ (S : Set α) (hS : S ∈ P₀.parts), p.1 ∈ S → e p.1 ∈ σ S hS :=
       Measure.QuasiMeasurePreserving.ae Measure.quasiMeasurePreserving_fst h_align_ae
@@ -792,7 +792,7 @@ private theorem exists_cutNormDiff_cauchy_realignment
         summable_geometric_of_lt_one (by positivity) (by norm_num)
       have h2 := h.mul_left 2
       simp only [one_div] at h2
-      convert h2 using 1; ext k; rw [inv_pow]; ring
+      exact h2.congr (fun k => by rw [inv_pow]; ring)
   refine ⟨f, hf, δ, hδ_sum, hδ_pos, fun k => ?_⟩
   -- Key calc: f (k+1) = f k . trans (σ k), so ⇑(f (k+1)) = σ_k ∘ f_k
   -- pb(V(k+1), f_{k+1}) = pb(V(k+1), σ_k ∘ f_k) = pb(pb(V(k+1), σ_k), f_k)
@@ -948,7 +948,7 @@ private lemma rectIntegralDiff_le_tail_tsum
             ≤ |rectIntegralDiff (A n) (A m) S T| +
               |rectIntegralDiff (A m) (A (m + 1)) S T| := h_tri
           _ ≤ ∑ j ∈ Finset.range (m - n), δ (n + j) + δ m := add_le_add (ih h) h_step
-      · push_neg at h
+      · push Not at h
         have heq : n = m + 1 := by omega
         subst heq
         simp only [Nat.sub_self, Finset.range_zero, Finset.sum_empty, rectIntegralDiff, sub_self,
@@ -1171,7 +1171,6 @@ private theorem exists_limit_measure_of_summable
     (by simp [hc_empty])
     (by
       intro f hf h_disj
-      simp only []
       rw [hc_additive hf h_disj]
       exact ENNReal.ofReal_tsum_of_nonneg (fun i => hc_nn (f i) (hf i))
         (Summable.of_nonneg_of_le (fun i => hc_nn (f i) (hf i))

Graphon/CutDistance.lean

@@ -323,7 +323,7 @@ private lemma layer_cake_Icc (a : ℝ) (ha : a ∈ Set.Icc 0 1) :
   rw [h_inter, min_eq_left ha.2]
   by_cases ha0 : a ≤ 0
   · rw [le_antisymm ha0 ha.1, Set.Ioc_self]; simp
-  · push_neg at ha0
+  · push Not at ha0
     rw [setIntegral_const, smul_eq_mul, mul_one]
     unfold Measure.real
     rw [Real.volume_Ioc, sub_zero, ENNReal.toReal_ofReal ha0.le]
@@ -426,7 +426,7 @@ private lemma layer_cake_simple_eq (U W : Graphon α μ) (S : Set α) (hS : Meas
   rw [h_lhs_eq]
   have h_lhs : ∫ p, ∑ i : Fin n, c i * (S ×ˢ T i).indicator K p ∂(μ.prod μ) =
       ∑ i : Fin n, c i * rectIntegralDiff U W S (T i) := by
-    rw [integral_finset_sum]
+    rw [integral_finsetSum]
     · congr 1; ext i
       rw [integral_const_mul, integral_indicator (hS.prod (hT_meas i))]
       rfl
@@ -445,7 +445,7 @@ private lemma layer_cake_simple_eq (U W : Graphon α μ) (S : Set α) (hS : Meas
     · intro hty
       -- g y ≥ t > 0, so g y > 0, so y must be in some T j, and c j ≥ t
       by_contra h_none
-      push_neg at h_none
+      push Not at h_none
       -- h_none : ∀ i, t ≤ c i → y ∉ T i
       -- We'll show g y = 0, contradicting t ≤ g y with t > 0
       have hgy0 : g y = 0 := by
@@ -491,7 +491,7 @@ private lemma layer_cake_simple_eq (U W : Graphon α μ) (S : Set α) (hS : Meas
     rw [h_level t ht.1, h_rect_union t ht.1]
   rw [h_rhs_eq]
   -- Step 4: Swap integral and finite sum
-  rw [integral_finset_sum]
+  rw [integral_finsetSum]
   · -- Step 5: Compute each inner integral
     congr 1; ext i
     -- ∫ t in Ioc 0 1, (if t ≤ c i then R_i else 0) dt = c_i * R_i
@@ -508,7 +508,7 @@ private lemma layer_cake_simple_eq (U W : Graphon α μ) (S : Set α) (hS : Meas
     rw [Set.Ioc_inter_Iic, min_eq_right (hc_bound i).2]
     by_cases hci0 : c i ≤ 0
     · rw [le_antisymm hci0 (hc_bound i).1, Set.Ioc_self, setIntegral_empty, zero_mul]
-    · push_neg at hci0
+    · push Not at hci0
       rw [setIntegral_const, smul_eq_mul]
       congr 1
       unfold Measure.real
@@ -671,7 +671,7 @@ private lemma abs_weighted_integral_diff_indicator_general_le (U W : Graphon α
         by_cases h : t ≤ g p.2
         · simp [Set.indicator_of_mem (show p.2 ∈ {y : α | t ≤ g y} from h),
                 Set.indicator_of_mem (Set.mem_Iic.mpr h)]
-        · push_neg at h
+        · push Not at h
           simp [Set.indicator_of_notMem (show p.2 ∉ {y : α | t ≤ g y} from not_le.mpr h),
                 Set.indicator_of_notMem (show t ∉ Set.Iic (g p.2) from not_le.mpr h)]
       rw [h_ind_eq]
@@ -883,7 +883,7 @@ theorem abs_weighted_integral_diff_le (U W : Graphon α μ) (f g : α → ℝ)
         by_cases h : s ≤ f p.1
         · simp [Set.indicator_of_mem (show p.1 ∈ {x : α | s ≤ f x} from h),
                 Set.indicator_of_mem (Set.mem_Iic.mpr h)]
-        · push_neg at h
+        · push Not at h
           simp [Set.indicator_of_notMem (show p.1 ∉ {x : α | s ≤ f x} from not_le.mpr h),
                 Set.indicator_of_notMem (show s ∉ Set.Iic (f p.1) from not_le.mpr h)]
       rw [h_ind_eq]
@@ -1244,7 +1244,7 @@ theorem cutDistance_triangle [StandardBorelSpace α] (U V W : Graphon α μ) :
   -- Suffices to show: for all ε > 0, d(U,W) ≤ d(U,V) + d(V,W) + ε
   rw [← sub_nonneg]
   by_contra h_neg
-  push_neg at h_neg
+  push Not at h_neg
   -- h_neg : cutDistance U V + cutDistance V W - cutDistance U W < 0
   set δ := cutDistance U W - cutDistance U V - cutDistance V W with hδ_def
   have hδ_pos : δ > 0 := by linarith

Graphon/CycleKrylov.lean

@@ -6,7 +6,7 @@ Authors: Cameron Freer
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import Mathlib.Analysis.InnerProductSpace.ProdL2
 import Mathlib.Analysis.InnerProductSpace.Projection.Basic
-import Mathlib.Data.Real.Sqrt
+import Mathlib.Analysis.Real.Sqrt
 import Graphon.SimpleRank
 
 /-!
@@ -963,14 +963,12 @@ def k23Arms (a b c : ℕ) : SimpleGraph (Fin (4 + a + b + c + 1)) where
     (∃ l < 3, ∃ s ≤ armLen a b c l,
       ((u : ℕ) = armSeq a b c l s ∧ (v : ℕ) = armSeq a b c l (s + 1)) ∨
       ((v : ℕ) = armSeq a b c l s ∧ (u : ℕ) = armSeq a b c l (s + 1)))
-  symm := by
-    intro u v h
+  symm.symm := fun u v h => by
     rcases h with ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨l, hl, s, hs, h⟩
     · exact Or.inr (Or.inl ⟨h1, h2⟩)
     · exact Or.inl ⟨h1, h2⟩
     · exact Or.inr (Or.inr ⟨l, hl, s, hs, h.symm⟩)
-  loopless := by
-    intro u h
+  loopless.irrefl := fun u h => by
     rcases h with ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨l, hl, s, hs, h⟩
     · omega
     · omega
@@ -1133,12 +1131,10 @@ theorem k23Edge_injective (a b c : ℕ) :
 private theorem out_pair_eq {T' n : ℕ} (Bm : Fin T' → Fin T' → ℝ)
     (hB : ∀ i j, Bm i j = Bm j i) (τ : Fin n → Fin T') (x y : Fin n) :
     Bm (τ (Quot.out s(x, y)).1) (τ (Quot.out s(x, y)).2) = Bm (τ x) (τ y) := by
-  have hout := Quot.out_eq s(x, y)
-  rw [Sym2.mk_eq_mk_iff] at hout
-  rcases hout with h | h
-  · rw [congrArg Prod.fst h, congrArg Prod.snd h]
-  · simp only [Prod.swap] at h
-    rw [congrArg Prod.fst h, congrArg Prod.snd h, hB]
+  have hout : s((Quot.out s(x, y)).1, (Quot.out s(x, y)).2) = s(x, y) := Quot.out_eq _
+  rcases Sym2.eq_iff.mp hout with ⟨h1, h2⟩ | ⟨h1, h2⟩
+  · rw [h1, h2]
+  · rw [h1, h2, hB]
 
 /-- **Edge-product factorization** for `k23Arms`: the edge product splits into
 the three root-edge factors times the three independent arm-chain products. -/
@@ -1893,13 +1889,11 @@ def k2kArmsStructured (k : ℕ) (armLen : Fin k → ℕ) :
     (∃ l : Fin k, ∃ s ≤ armLen l,
       (u = K2kVertex.armNode k armLen l s ∧ v = K2kVertex.armNode k armLen l (s + 1)) ∨
       (v = K2kVertex.armNode k armLen l s ∧ u = K2kVertex.armNode k armLen l (s + 1)))
-  symm := by
-    intro u v h
+  symm.symm := fun u v h => by
     rcases h with ⟨l, h⟩ | ⟨l, s, hs, h⟩
     · exact Or.inl ⟨l, h.symm⟩
     · exact Or.inr ⟨l, s, hs, h.symm⟩
-  loopless := by
-    intro u h
+  loopless.irrefl := fun u h => by
     rcases h with ⟨l, h⟩ | ⟨l, s, hs, h⟩
     · obtain ⟨h1, h2⟩ | ⟨h1, h2⟩ := h <;> (rw [h1] at h2; simp at h2)
     · obtain ⟨h1, h2⟩ | ⟨h1, h2⟩ := h <;>
@@ -1977,12 +1971,10 @@ theorem k2kArmsStructured_edgeFinset (k : ℕ) (armLen : Fin k → ℕ) :
 theorem out_pair_eq' {T' : ℕ} {V : Type*} (Bm : Fin T' → Fin T' → ℝ)
     (hB : ∀ i j, Bm i j = Bm j i) (g : V → Fin T') (x y : V) :
     Bm (g (Quot.out s(x, y)).1) (g (Quot.out s(x, y)).2) = Bm (g x) (g y) := by
-  have hout := Quot.out_eq s(x, y)
-  rw [Sym2.mk_eq_mk_iff] at hout
-  rcases hout with h | h
-  · rw [congrArg Prod.fst h, congrArg Prod.snd h]
-  · simp only [Prod.swap] at h
-    rw [congrArg Prod.fst h, congrArg Prod.snd h, hB]
+  have hout : s((Quot.out s(x, y)).1, (Quot.out s(x, y)).2) = s(x, y) := Quot.out_eq _
+  rcases Sym2.eq_iff.mp hout with ⟨h1, h2⟩ | ⟨h1, h2⟩
+  · rw [h1, h2]
+  · rw [h1, h2, hB]
 
 /-- Arm index of a vertex (anchors/internals carry their arm; root/hub `none`).
 Used to recover `(l, s)` from a chain endpoint in `k2kEdge_injective`. -/
@@ -2612,7 +2604,7 @@ theorem decorateAtSum_edge_disjoint {n m : ℕ} (F : SimpleGraph (Fin (n + 1)))
         have hk : (hDecorEmb u) (Fin.succ k) = Sum.inr k := by simp [hDecorEmb]
         rw [hk] at hb'; rw [← hb] at hb'; exact absurd hb' (by simp)
     subst ha0 hb0
-    exact H.loopless 0 hadj'
+    exact H.irrefl hadj'
 
 /-- **Edge-product transport + split** (Commit 1 steps 1–2): the `rootedProfile`
 edge product over `decorateAt F H u` factors, through `decorVertexEquiv`, into the
@@ -2895,7 +2887,7 @@ theorem decorateAll_F_sup_disjoint {n m : ℕ} (F : SimpleGraph (Fin (n + 1)))
       · rfl
       · exact absurd (hb'.trans hb.symm) (by simp [embedHCopy])
     subst ha0 hb0
-    exact H.loopless 0 hadj'
+    exact H.irrefl hadj'
 
 /-- The `Finset.sup` of the `H`-copies has edge finset the disjoint union of the
 per-copy edge finsets. -/
@@ -3247,7 +3239,7 @@ theorem decorateAllFam_F_sup_disjoint {n : ℕ} {mfam : Fin n → ℕ}
       · rfl
       · exact absurd (hb'.trans hb.symm) (by simp [embedHCopyFam])
     subst ha0 hb0
-    exact (Hfam w).loopless 0 hadj'
+    exact (Hfam w).irrefl hadj'
 
 theorem decorateAllFamSum_sup_edgeFinset {n : ℕ} {mfam : Fin n → ℕ}
     (Hfam : (w : Fin n) → SimpleGraph (Fin (mfam w + 1))) [∀ w, DecidableRel (Hfam w).Adj] :
@@ -3820,8 +3812,8 @@ theorem commonNeighborGraph_edgeFinset :
     commonNeighborGraph.edgeFinset = {s((0 : Fin (1 + 2)), 2), s((1 : Fin (1 + 2)), 2)} := by
   ext e
   simp only [SimpleGraph.mem_edgeFinset, commonNeighborGraph, SimpleGraph.edgeSet_fromEdgeSet,
-    Finset.mem_insert, Finset.mem_singleton, Set.mem_diff, Set.mem_insert_iff,
-    Set.mem_singleton_iff, Sym2.mem_diagSet_iff_isDiag]
+    Finset.mem_insert, Finset.mem_singleton, Set.mem_sdiff, Set.mem_insert_iff,
+    Set.mem_singleton_iff, Sym2.mem_diagSet]
   refine ⟨fun ⟨he, _⟩ => he, fun he => ⟨he, ?_⟩⟩
   rcases he with he | he <;> rw [he, Sym2.mk_isDiag_iff] <;> decide
 

Graphon/HomDensity.lean

@@ -120,7 +120,8 @@ theorem homDensity_bot (W : Graphon α μ) :
 theorem edge_out_ne {F : SimpleGraph V} [DecidableRel F.Adj] {e : Sym2 V}
     (he : e ∈ F.edgeSet) : (Quot.out e).1 ≠ (Quot.out e).2 := by
   have h_not_diag := F.not_isDiag_of_mem_edgeSet he
-  have h_eq : e = Sym2.mk (Quot.out e) := (Quot.out_eq e).symm
+  have h_eq : e = s((Quot.out e).1, (Quot.out e).2) := by
+    simp [Sym2.mk, Quot.out_eq]
   rw [h_eq, Sym2.mk_isDiag_iff] at h_not_diag
   exact h_not_diag