Bump mathlib

Author: YaelDillies

LeanCamCombi.lean

@@ -43,7 +43,6 @@ import LeanCamCombi.Mathlib.Analysis.Convex.Extreme
 import LeanCamCombi.Mathlib.Analysis.Convex.Independence
 import LeanCamCombi.Mathlib.Analysis.Convex.SimplicialComplex.Basic
 import LeanCamCombi.Mathlib.Combinatorics.Additive.RuzsaCovering
-import LeanCamCombi.Mathlib.Combinatorics.Additive.SmallTripling
 import LeanCamCombi.Mathlib.Combinatorics.Schnirelmann
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Containment
@@ -59,7 +58,6 @@ import LeanCamCombi.Mathlib.Data.List.DropRight
 import LeanCamCombi.Mathlib.Data.Multiset.Basic
 import LeanCamCombi.Mathlib.Data.Prod.Lex
 import LeanCamCombi.Mathlib.Data.Set.Image
-import LeanCamCombi.Mathlib.Data.Set.Lattice
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.Finite
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.Interval
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul

LeanCamCombi/GrowthInGroups/ApproximateSubgroup.lean

@@ -1,8 +1,9 @@
+import Mathlib.Algebra.Group.Subgroup.Defs
 import Mathlib.Algebra.Order.BigOperators.Ring.Finset
+import Mathlib.Combinatorics.Additive.SmallTripling
 import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Basic
 import LeanCamCombi.Mathlib.Combinatorics.Additive.RuzsaCovering
-import LeanCamCombi.Mathlib.Combinatorics.Additive.SmallTripling
 import LeanCamCombi.Mathlib.Data.Finset.Basic
 
 open scoped Finset Pointwise

LeanCamCombi/GrowthInGroups/Lecture1.lean

@@ -6,7 +6,6 @@ import Mathlib.Tactic.Positivity.Finset
 import LeanCamCombi.GrowthInGroups.VerySmallDoubling
 import LeanCamCombi.Mathlib.Algebra.Group.Subgroup.Pointwise
 import LeanCamCombi.Mathlib.Data.Finset.Basic
-import LeanCamCombi.Mathlib.Data.Set.Lattice
 
 open Finset Fintype Group Matrix MulOpposite Real
 open scoped Combinatorics.Additive MatrixGroups Pointwise

LeanCamCombi/Mathlib/Algebra/Group/Subgroup/Pointwise.lean

@@ -1,5 +1,4 @@
 import Mathlib.Algebra.Group.Subgroup.Pointwise
-import LeanCamCombi.Mathlib.Data.Set.Lattice
 
 open Subgroup
 open scoped Pointwise

LeanCamCombi/Mathlib/Combinatorics/Additive/SmallTripling.lean

@@ -1,9 +0,0 @@
-import Mathlib.Data.Finset.Basic
-
-namespace Finset
-
-nonrec lemma Nontrivial.nonempty {α} {X : Finset α} (hX : X.Nontrivial) : X.Nonempty := hX.nonempty
-
-attribute [simp] subset_empty
-
-end Finset

LeanCamCombi/Mathlib/Data/Finset/Basic.lean

@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fd92bc36215a9632f15c6482fb0132d24e6c49ab",
+   "rev": "2c03193f60cd7865fd4823ebaa5e600acd97404d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b41bc9cec7f433d6e1d74ff3b59edaaf58ad2915",
+   "rev": "2905ab4ec3961d1fd68ddae0ab4083497e579014",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -125,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3a296bbf01538edd592ca5bbdec389768d6abed4",
+   "rev": "7b6a56e8e4fcf54d3834b225b9814a7c9e4d4bda",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",