Bump mathlib

Author: YaelDillies

LeanCamCombi/GrowthInGroups/Lecture4.lean

@@ -1,4 +1,4 @@
-import Mathlib.Analysis.Matrix
+import Mathlib.Analysis.Matrix.Normed
 import Mathlib.GroupTheory.Nilpotent
 import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
 import LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup
@@ -21,7 +21,7 @@ lemma fact_4_1 (S T : GL n ℂ) :
 open scoped Classical in
 lemma lemma_4_2 (hC₀ : Fintype.card n < C₀) (K : ℝ) :
     ∃ δ : ℝ,
-      ∀ (A : Finset (GL n ℂ)) (hA : IsApproximateSubgroup K A.toSet) (hC₀ : ∀ a ∈ A, ‖a.val‖ ≤ C₀),
+      ∀ A : Finset (GL n ℂ), IsApproximateSubgroup K (A : Set (GL n ℂ)) → (∀ a ∈ A, ‖a.val‖ ≤ C₀) →
         ∃ γ ∈ A ^ 2, δ * #A ≤ #{x ∈ A ^ 4 | Commute γ x} := sorry
 
 lemma corollary_4_3 (K C₀ : ℝ) :

LeanCamCombi/Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean

@@ -39,7 +39,7 @@ lemma exists_isApproximateSubgroup_of_small_doubling [DecidableEq G] {A : Finset
   have hS₁ : 1 ∈ S := by simp [S, hA₀.ne_empty]; bound
   have hS₀ : S.Nonempty := ⟨1, hS₁⟩
   have hSA : S ⊆ A⁻¹ * A := filter_subset ..
-  have hSsymm : S⁻¹ = S := by ext; simp [S]; simp [← mem_inv']; sorry
+  have hSsymm : S⁻¹ = S := by ext; simp [S]; sorry
   have hScard := calc
     (#S : ℝ) ≤ #(A⁻¹ * A) := by gcongr
     _ ≤ K ^ 2 * #A := sorry

LeanCamCombi/PlainCombi/LittlewoodOfford.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Analysis.NormedSpace.HahnBanach.Extension
+import Mathlib.Analysis.Normed.Module.HahnBanach
 import Mathlib.Combinatorics.Enumerative.DoubleCounting
 import Mathlib.Order.Partition.Finpartition
 

LeanCamCombi/PlainCombi/ProbLYM.lean

@@ -11,8 +11,6 @@ import LeanCamCombi.PlainCombi.KatonaCircle
 
 This file proves the LYM inequality using (very elementary) probability theory.
 
-
-
 ## References
 
 This proof formalizes Section 1.2 of Prof. Yufei Zhao's lecture notes for MIT 18.226:
@@ -35,7 +33,7 @@ open Finset Fintype Numbering
 variable {α : Type*} [Fintype α] {𝒜 : Finset (Finset α)}
 
 /-- The **Lubell-Yamamoto-Meshalkin inequality**, proved using the Katona circle method. -/
-theorem LYM_inequality (h𝒜 : IsAntichain (· ⊆ ·) 𝒜.toSet) :
+theorem LYM_inequality (h𝒜 : IsAntichain (· ⊆ ·) (𝒜 : Set (Finset α))) :
     ∑ s ∈ 𝒜, ((card α).choose #s : ℚ≥0)⁻¹ ≤ 1 := by
   classical
   calc

lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f897ebcf72cd16f89ab4577d0c826cd14afaafc7",
+   "rev": "029db123ddaa7f8fd0d18cea3b1b33bf84dacd1e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.24.0",
+   "inputRev": "v4.25.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dfd06ebfe8d0e8fa7faba9cb5e5a2e74e7bd2805",
+   "rev": "2503bfb5e2d4d8202165f5bd2cc39e44a3be31c3",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
+   "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d768126816be17600904726ca7976b185786e6b9",
+   "rev": "009064c21bad4d7f421f2901c5e817c8bf3468cb",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "556caed0eadb7901e068131d1be208dd907d07a2",
+   "rev": "fb8ed0a85a96e3176f6e94b20d413ea72d92576d",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.74",
+   "inputRev": "v0.0.77",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50",
+   "rev": "26e4c7c0e63eb3e6cce3cf7faba27b8526ea8349",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dea6a3361fa36d5a13f87333dc506ada582e025c",
+   "rev": "2781d8ad404303b2fe03710ac7db946ddfe3539f",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
+   "rev": "39260e31b7b3f7f05643da95242463b462dc05f1",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da",
+   "rev": "1dae8b12f8ba27576ffe5ddee78bebf6458157b0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.25.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "LeanCamCombi",

lakefile.toml

@@ -39,7 +39,7 @@ linter.style.setOption = true
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.24.0"
+rev = "v4.25.0"
 
 [[lean_lib]]
 name = "LeanCamCombi"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.25.0