Bump mathlib

Author: YaelDillies

LeanCamCombi.lean

@@ -1,5 +1,4 @@
 import LeanCamCombi.Archive.CauchyDavenportFromKneser
-import LeanCamCombi.CauchyFunctionalEquation
 import LeanCamCombi.ConvexityRefactor.Defs
 import LeanCamCombi.ConvexityRefactor.StdSimplex
 import LeanCamCombi.Corners.CombiDegen
@@ -22,20 +21,17 @@ import LeanCamCombi.GrowthInGroups.Lecture1
 import LeanCamCombi.GrowthInGroups.Lecture2
 import LeanCamCombi.GrowthInGroups.Lecture3
 import LeanCamCombi.GrowthInGroups.Lecture4
-import LeanCamCombi.GrowthInGroups.LinearLowerBound
 import LeanCamCombi.Impact
 import LeanCamCombi.Kneser.Kneser
 import LeanCamCombi.Kneser.KneserRuzsa
 import LeanCamCombi.Kneser.MulStab
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Basic
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Degrees
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Equiv
-import LeanCamCombi.Mathlib.Algebra.Ring.Hom.Defs
 import LeanCamCombi.Mathlib.Analysis.Convex.Exposed
 import LeanCamCombi.Mathlib.Analysis.Convex.Extreme
 import LeanCamCombi.Mathlib.Analysis.Convex.Independence
 import LeanCamCombi.Mathlib.Analysis.Convex.SimplicialComplex.Basic
-import LeanCamCombi.Mathlib.Analysis.RCLike.Basic
 import LeanCamCombi.Mathlib.Combinatorics.Schnirelmann
 import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shatter
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic
@@ -45,25 +41,16 @@ import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Maps
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
 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.Pointwise.SMul
 import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 import LeanCamCombi.Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
 import LeanCamCombi.Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
-import LeanCamCombi.Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
-import LeanCamCombi.Mathlib.MeasureTheory.Function.L1Space
-import LeanCamCombi.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import LeanCamCombi.Mathlib.MeasureTheory.Measure.Haar.NormedSpace
-import LeanCamCombi.Mathlib.MeasureTheory.Measure.Typeclasses
-import LeanCamCombi.Mathlib.Order.BooleanSubalgebra
 import LeanCamCombi.Mathlib.Order.Flag
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
 import LeanCamCombi.Mathlib.Order.RelIso.Group
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
-import LeanCamCombi.Mathlib.Probability.Variance
-import LeanCamCombi.Mathlib.RingTheory.FinitePresentation
 import LeanCamCombi.Mathlib.RingTheory.Spectrum.Prime.Topology
 import LeanCamCombi.Mathlib.Topology.MetricSpace.MetricSeparated
 import LeanCamCombi.MetricBetween

LeanCamCombi/CauchyFunctionalEquation.lean

@@ -1,8 +1,6 @@
 import Mathlib.Data.DFinsupp.WellFounded
 import Mathlib.RingTheory.Localization.Algebra
 import Mathlib.RingTheory.Spectrum.Prime.Polynomial
-import LeanCamCombi.Mathlib.Data.Prod.Lex
-import LeanCamCombi.Mathlib.RingTheory.FinitePresentation
 import LeanCamCombi.GrowthInGroups.ConstructiblePrimeSpectrum
 
 open Polynomial PrimeSpectrum TensorProduct Topology

LeanCamCombi/GrowthInGroups/Chevalley.lean

@@ -5,7 +5,6 @@ import Mathlib.RingTheory.Spectrum.Prime.Polynomial
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Basic
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Degrees
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Equiv
-import LeanCamCombi.Mathlib.Data.Prod.Lex
 import LeanCamCombi.Mathlib.Data.Set.Image
 import LeanCamCombi.Mathlib.RingTheory.Spectrum.Prime.Topology
 import LeanCamCombi.GrowthInGroups.ConstructibleSetData
@@ -149,7 +148,7 @@ lemma foo_induction (n : ℕ)
     -- We replace `R` by `R ⧸ Ideal.span {(e i).leadingCoeff}` where `(e i).degree` is lowered
     -- and `Away (e i).leadingCoeff` where `(e i).leadingCoeff` becomes invertible.
     apply hP _ _ i e rfl (by simpa using hi) (H_IH _ ?_ _ rfl) (H_IH _ ?_ _ rfl)
-    · rw [hv, Prod.Lex.lt_iff'']
+    · rw [hv, Prod.Lex.lt_iff']
       constructor
       · intro j
         simp only [coe_mapRingHom, InductionObj.ofLex_degree_fst, Pi.smul_apply,

LeanCamCombi/GrowthInGroups/ChevalleyComplex.lean

@@ -3,8 +3,8 @@ Copyright (c) 2024 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
+import Mathlib.Order.BooleanSubalgebra
 import Mathlib.Topology.Spectral.Hom
-import LeanCamCombi.Mathlib.Order.BooleanSubalgebra
 
 /-!
 # Constructible sets
@@ -342,7 +342,7 @@ lemma IsConstructible.induction_of_isTopologicalBasis {ι : Type*} [Nonempty ι]
         basis.isConstructible' compact_inter _))
     (union : ∀ s hs t ht, P s hs → P t ht → P (s ∪ t) (hs.union ht))
     (s : Set X) (hs : IsConstructible s) : P s hs := by
-  induction s, hs using BooleanSubalgebra.closure_sdiff_sup_induction' with
+  induction s, hs using BooleanSubalgebra.closure_sdiff_sup_induction with
   | isSublattice =>
     exact ⟨fun s hs t ht ↦ ⟨hs.1.union ht.1, hs.2.union ht.2⟩,
       fun s hs t ht ↦ ⟨hs.1.inter ht.1, hs.2.inter_isOpen ht.2 ht.1⟩⟩

LeanCamCombi/GrowthInGroups/Constructible.lean

@@ -1,9 +1,9 @@
 import Mathlib.Analysis.SpecialFunctions.Log.Basic
 import Mathlib.Combinatorics.Additive.DoublingConst
 import Mathlib.Combinatorics.Additive.VerySmallDoubling
+import Mathlib.Geometry.Group.Growth.LinearLowerBound
 import Mathlib.GroupTheory.Nilpotent
 import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
-import LeanCamCombi.GrowthInGroups.LinearLowerBound
 import LeanCamCombi.Util
 
 open Finset Fintype Group MulOpposite Real

LeanCamCombi/GrowthInGroups/Lecture1.lean

@@ -374,7 +374,7 @@ theorem mul_kneser :
   exfalso
   have : ¬s * t * H ⊆ s * t := by
     rw [mul_subset_left_iff (hs.mul ht), hstab, ← coe_subset, coe_one]
-    exact hCstab.not_subset_singleton
+    exact hCstab.coe.not_subset_singleton
   simp_rw [mul_subset_iff_left, Classical.not_forall, mem_mul] at this
   obtain ⟨_, ⟨a, ha, b, hb, rfl⟩, hab⟩ := this
   set s₁ := s ∩ a • H with hs₁