Bump mathlib

LeanCamCombi.lean

@@ -35,7 +35,6 @@ import LeanCamCombi.Mathlib.Data.Multiset.Basic
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
-import LeanCamCombi.Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
 import LeanCamCombi.Mathlib.Order.Flag
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
 import LeanCamCombi.Mathlib.Order.RelIso.Group
@@ -45,7 +44,6 @@ import LeanCamCombi.MetricBetween
 import LeanCamCombi.MinkowskiCaratheodory
 import LeanCamCombi.Multipartite
 import LeanCamCombi.PhD.VCDim.AddVCDim
-import LeanCamCombi.PhD.VCDim.CondVar
 import LeanCamCombi.PhD.VCDim.HausslerPacking
 import LeanCamCombi.PhD.VCDim.HypercubeEdges
 import LeanCamCombi.PlainCombi.LittlewoodOfford

LeanCamCombi/GrowthInGroups/Lecture2.lean

@@ -33,10 +33,10 @@ lemma lemma_2_3_1 (hA : #(A ^ 2) ≤ K * #A) : #(A * A⁻¹) ≤ K ^ 2 * #A := b
 
 lemma lemma_2_4_1 (hm : 3 ≤ m) (hA : #(A ^ 3) ≤ K * #A) (ε : Fin m → ℤ) (hε : ∀ i, |ε i| = 1) :
     #((finRange m).map fun i ↦ A ^ ε i).prod ≤ K ^ (3 * (m - 2)) * #A :=
-  small_alternating_pow_of_small_tripling' hm hA ε hε
+  small_alternating_pow_of_small_tripling hm hA ε hε
 
 lemma lemma_2_4_2 (hm : 3 ≤ m) (hA : #(A ^ 3) ≤ K * #A) (hAsymm : A⁻¹ = A) :
-    #(A ^ m) ≤ K ^ (m - 2) * #A := small_pow_of_small_tripling' hm hA hAsymm
+    #(A ^ m) ≤ K ^ (m - 2) * #A := small_pow_of_small_tripling hm hA hAsymm
 
 def def_2_5 (S : Set G) (K : ℝ) : Prop := IsApproximateSubgroup K S
 

LeanCamCombi/Kneser/Kneser.lean

@@ -357,11 +357,11 @@ theorem mul_kneser :
       subset_mul_left _ $ one_mem_mulStab.2 $ hst.mul $ hs.mono subset_union_left) _).trans $
         ih (s ∩ t) (s ∪ t) ?_⟩
     exact add_lt_add_of_le_of_lt (card_le_card inter_mul_union_subset) (card_lt_card hsts)
-  let C := argminOn (fun C : Finset α => #C.mulStab) IsWellFounded.wf _ convergent_nonempty
+  let C := argminOn (fun C : Finset α => #C.mulStab) _ convergent_nonempty
   set H := C.mulStab with hH
-  obtain ⟨hCst, hCcard⟩ : C ∈ convergent := argminOn_mem _ _ _ _
-  have hCmin : ∀ D : Finset α, D.mulStab ⊂ H → ¬D ∈ convergent := fun D hDH hD =>
-    (card_lt_card hDH).not_le $ argminOn_le (fun D : Finset α => #D.mulStab) _ _ hD
+  obtain ⟨hCst, hCcard⟩ : C ∈ convergent := argminOn_mem _ _ _
+  have hCmin (D : Finset α) (hDH : D.mulStab ⊂ H) : D ∉ convergent := fun hD ↦
+    (card_lt_card hDH).not_le $ argminOn_le (fun D : Finset α => #D.mulStab) _ hD
   clear_value C
   clear convergent_nonempty
   obtain rfl | hC := C.eq_empty_or_nonempty

LeanCamCombi/Mathlib/Combinatorics/Schnirelmann.lean

@@ -182,7 +182,7 @@ theorem le_schnirelmannDensity_add (A B : Set ℕ) (hA : 0 ∈ A) (hB : 0 ∈ B)
         {c ∈ A + B | 0 < c - x ∧ (c : ℕ) ≤ next_elm A x n} = ∅ := by sorry
         -- by_contra! hin
         -- rw? at hin
-      -- have hcount : ∑ a in A, (1 + countelements B (next_elm A a n - a - 1)) ≤ countelements (⋃ a : A, {c ∈ A + B | 0 < c - a ∧ (c : ℕ) ≤ (next_elm A a n)}) n := by sorry
+      -- have hcount : ∑ a ∈ A, (1 + countelements B (next_elm A a n - a - 1)) ≤ countelements (⋃ a : A, {c ∈ A + B | 0 < c - a ∧ (c : ℕ) ≤ (next_elm A a n)}) n := by sorry
       sorry
     have ht : countelements A n + β * (n - countelements A n) ≤ countelements (A + B) n := by
       apply le_trans claim _

LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Finite.lean

@@ -26,7 +26,7 @@ lemma degOn_union (h : Disjoint s t) (a) : G.degOn (s ∪ t) a = G.degOn s a + G
   exact h.mono inter_subset_left inter_subset_left
 
 -- edges from t to s\t equals edges from s\t to t
-lemma sum_degOn_comm (s t : Finset α) : ∑ a in s, G.degOn t a = ∑ a in t, G.degOn s a := by
+lemma sum_degOn_comm (s t : Finset α) : ∑ a ∈ s, G.degOn t a = ∑ a ∈ t, G.degOn s a := by
   simp_rw [degOn, card_eq_sum_ones, ← sum_indicator_eq_sum_inter]
   rw [sum_comm]
   simp [Set.indicator_apply, adj_comm]

LeanCamCombi/PlainCombi/LittlewoodOfford.lean

@@ -20,7 +20,7 @@ variable {ι E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝒜 : Finse
 lemma exists_littlewood_offord_partition [DecidableEq ι] (hr : 0 < r) (hf : ∀ i ∈ s, r ≤ ‖f i‖) :
     ∃ P : Finpartition s.powerset,
       #P.parts = (#s).choose (#s / 2) ∧ (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s) ∧ ∀ 𝒜 ∈ P.parts,
-        (𝒜 : Set (Finset ι)).Pairwise fun u v ↦ r ≤ dist (∑ i in u, f i) (∑ i in v, f i) := by
+        (𝒜 : Set (Finset ι)).Pairwise fun u v ↦ r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i) := by
   classical
   induction' s using Finset.induction with i s hi ih
   · exact ⟨Finpartition.indiscrete $ singleton_ne_empty _, by simp⟩
@@ -29,12 +29,12 @@ lemma exists_littlewood_offord_partition [DecidableEq ι] (hr : 0 < r) (hf : ∀
   obtain ⟨g, hg, hgf⟩ :=
     exists_dual_vector ℝ (f i) (norm_pos_iff.1 $ hr.trans_le $ hf _ $ mem_insert_self _ _)
   choose! t ht using fun 𝒜 (h𝒜 : 𝒜 ∈ P.parts) ↦
-    Finset.exists_max_image _ (fun t ↦ g (∑ i in t, f i)) (P.nonempty_of_mem_parts h𝒜)
+    Finset.exists_max_image _ (fun t ↦ g (∑ i ∈ t, f i)) (P.nonempty_of_mem_parts h𝒜)
   sorry
 
 /-- **Kleitman's lemma** -/
 lemma card_le_of_forall_dist_sum_le (hr : 0 < r) (h𝒜 : ∀ t ∈ 𝒜, t ⊆ s) (hf : ∀ i ∈ s, r ≤ ‖f i‖)
-    (h𝒜r : ∀ u, u ∈ 𝒜 → ∀ v, v ∈ 𝒜 → dist (∑ i in u, f i) (∑ i in v, f i) < r) :
+    (h𝒜r : ∀ u, u ∈ 𝒜 → ∀ v, v ∈ 𝒜 → dist (∑ i ∈ u, f i) (∑ i ∈ v, f i) < r) :
     #𝒜 ≤ (#s).choose (#s / 2) := by
   classical
   obtain ⟨P, hP, _hs, hr⟩ := exists_littlewood_offord_partition hr hf

LeanCamCombi/SimplicialComplex/Simplex.lean

@@ -87,7 +87,7 @@ variable [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {s t : Finse
 
 lemma combiFrontier_eq :
     combiFrontier 𝕜 s = {x : E | ∃ (w : E → 𝕜)
-      (_hw₀ : ∀ y ∈ s, 0 ≤ w y) (_hw₁ : ∑ y in s, w y = 1) (_hw₂ : ∃ y ∈ s, w y = 0),
+      (_hw₀ : ∀ y ∈ s, 0 ≤ w y) (_hw₁ : ∑ y ∈ s, w y = 1) (_hw₂ : ∃ y ∈ s, w y = 0),
         s.centerMass w id = x} := by
   ext x
   simp_rw [combiFrontier, Set.mem_iUnion, Set.mem_setOf_eq]
@@ -135,7 +135,7 @@ lemma combiFrontier_eq :
 lemma combiInterior_subset_positive_weighings :
     combiInterior 𝕜 s ⊆
       {x : E | ∃ (w : E → 𝕜)
-        (_hw₀ : ∀ y ∈ s, 0 < w y) (_hw₁ : ∑ y in s, w y = 1), s.centerMass w id = x} := by
+        (_hw₀ : ∀ y ∈ s, 0 < w y) (_hw₁ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} := by
   rw [combiInterior, Finset.convexHull_eq, combiFrontier_eq]
   rintro x
   simp only [not_exists, and_imp, not_and, mem_setOf_eq, mem_diff, exists_imp]
@@ -145,7 +145,7 @@ lemma combiInterior_subset_positive_weighings :
 
 lemma combiInterior_eq (hs : AffineIndependent 𝕜 ((↑) : s → E)) :
     combiInterior 𝕜 s = {x : E | ∃ (w : E → 𝕜)
-      (_hw₀ : ∀ y ∈ s, 0 < w y) (_hw₁ : ∑ y in s, w y = 1), s.centerMass w id = x} := by
+      (_hw₀ : ∀ y ∈ s, 0 < w y) (_hw₁ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} := by
   refine combiInterior_subset_positive_weighings.antisymm fun x => ?_
   rw [combiInterior, Finset.convexHull_eq, combiFrontier_eq]
   simp only [not_exists, and_imp, not_and, mem_setOf_eq, mem_diff, exists_imp]

docbuild/lake-manifest.json

@@ -62,7 +62,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "319694c02ee0e84e316396bb7d4f11241eb07e81",
+   "rev": "313efebe306dd046fd00db765b813a3180106038",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -132,7 +132,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5b23a1297aba9683f231c4b1a7ab4076af4ad53d",
+   "rev": "f133cf255b5f087ee6b34486b7f588970506640f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "319694c02ee0e84e316396bb7d4f11241eb07e81",
+   "rev": "313efebe306dd046fd00db765b813a3180106038",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5b23a1297aba9683f231c4b1a7ab4076af4ad53d",
+   "rev": "f133cf255b5f087ee6b34486b7f588970506640f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",