Bump mathlib

Author: YaelDillies

LeanCamCombi.lean

@@ -12,7 +12,6 @@ import LeanCamCombi.GraphTheory.ExampleSheet1
 import LeanCamCombi.GraphTheory.ExampleSheet2
 import LeanCamCombi.GrowthInGroups.ApproximateSubgroup
 import LeanCamCombi.GrowthInGroups.BooleanSubalgebra
-import LeanCamCombi.GrowthInGroups.CharPolyBaseChange
 import LeanCamCombi.GrowthInGroups.Chevalley
 import LeanCamCombi.GrowthInGroups.ChevalleyComplex
 import LeanCamCombi.GrowthInGroups.Constructible
@@ -65,7 +64,6 @@ import LeanCamCombi.Mathlib.Data.Set.Pointwise.Interval
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
-import LeanCamCombi.Mathlib.Order.Interval.Finset.Defs
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
 import LeanCamCombi.Mathlib.Order.RelClasses
 import LeanCamCombi.Mathlib.Order.SupClosed
@@ -74,8 +72,6 @@ import LeanCamCombi.Mathlib.RingTheory.FinitePresentation
 import LeanCamCombi.Mathlib.RingTheory.Ideal.Span
 import LeanCamCombi.Mathlib.RingTheory.LocalRing.ResidueField.Ideal
 import LeanCamCombi.Mathlib.RingTheory.Polynomial.Basic
-import LeanCamCombi.Mathlib.Topology.Defs.Induced
-import LeanCamCombi.Mathlib.Topology.Spectral.Hom
 import LeanCamCombi.MetricBetween
 import LeanCamCombi.MinkowskiCaratheodory
 import LeanCamCombi.OrderShatter

LeanCamCombi/GrowthInGroups/BooleanSubalgebra.lean

@@ -81,10 +81,10 @@ instance instBotCoe : Bot L where bot := ⟨⊥, bot_mem⟩
 instance instTopCoe : Top L where top := ⟨⊤, top_mem⟩
 
 /-- A boolean subalgebra of a lattice inherits a supremum. -/
-instance instSupCoe : Sup L where sup a b := ⟨a ⊔ b, L.supClosed a.2 b.2⟩
+instance instSupCoe : Max L where max a b := ⟨a ⊔ b, L.supClosed a.2 b.2⟩
 
 /-- A boolean subalgebra of a lattice inherits an infimum. -/
-instance instInfCoe : Inf L where inf a b := ⟨a ⊓ b, L.infClosed a.2 b.2⟩
+instance instInfCoe : Min L where min a b := ⟨a ⊓ b, L.infClosed a.2 b.2⟩
 
 /-- A boolean subalgebra of a lattice inherits a complement. -/
 instance instHasComplCoe : HasCompl L where compl a := ⟨aᶜ, compl_mem a.2⟩
@@ -166,8 +166,8 @@ instance instBot : Bot (BooleanSubalgebra α) where
   bot.infClosed' _ := by aesop
 
 /-- The inf of two boolean subalgebras is their intersection. -/
-instance instInf : Inf (BooleanSubalgebra α) where
-  inf L M :=  { carrier := L ∩ M
+instance instInf : Min (BooleanSubalgebra α) where
+  min L M :=  { carrier := L ∩ M
                 bot_mem' := ⟨bot_mem, bot_mem⟩
                 compl_mem' := fun ha ↦ ⟨compl_mem ha.1, compl_mem ha.2⟩
                 supClosed' := L.supClosed.inter M.supClosed

LeanCamCombi/GrowthInGroups/CharPolyBaseChange.lean

@@ -3,19 +3,15 @@ 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.Tactic.StacksAttribute
-import Mathlib.Topology.Compactness.Compact
-import Mathlib.Topology.Separation.Basic
 import Mathlib.Topology.Spectral.Hom
-import LeanCamCombi.Mathlib.Data.Set.Image
-import LeanCamCombi.Mathlib.Topology.Defs.Induced
 import LeanCamCombi.GrowthInGroups.BooleanSubalgebra
+import LeanCamCombi.Mathlib.Data.Set.Image
 
 /-!
 # Constructible sets
 -/
 
-open Set TopologicalSpace
+open Set TopologicalSpace Topology
 
 variable {ι : Sort*} {α β : Type*} [TopologicalSpace α] [TopologicalSpace β] {f : α → β}
   {s t U : Set α} {a : α}

LeanCamCombi/GrowthInGroups/Constructible.lean

@@ -1,11 +1,11 @@
 import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import Mathlib.LinearAlgebra.Dual
+import Mathlib.LinearAlgebra.Charpoly.BaseChange
 import Mathlib.LinearAlgebra.Eigenspace.Zero
 import Mathlib.LinearAlgebra.FreeModule.PID
 import Mathlib.Order.CompletePartialOrder
 import Mathlib.RingTheory.AdjoinRoot
 import Mathlib.RingTheory.SimpleRing.Basic
-import LeanCamCombi.GrowthInGroups.CharPolyBaseChange
 import LeanCamCombi.Mathlib.RingTheory.LocalRing.ResidueField.Ideal
 
 open Polynomial TensorProduct PrimeSpectrum
@@ -149,4 +149,3 @@ lemma isOpen_image_comap_of_monic (f g : R[X]) (hg : g.Monic) :
   exact (isClosed_zeroLocus (R := R) t).isOpen_compl
 
 end PrimeSpectrum
-#min_imports

LeanCamCombi/GrowthInGroups/PrimeSpectrumPolynomial.lean

@@ -127,8 +127,8 @@ def symmetricSubgroup (A : Finset G) (h : #(A * A) < (3 / 2 : ℚ) * #A) : Subgr
     rw [← coe_mul_comm_of_doubling (weaken_doubling h)]
     exact ⟨a * b * t, by simp [ht, mul_assoc], ((c * d)⁻¹ * t)⁻¹, by simp [ht, mul_assoc]⟩
 
-lemma coe_symmetricSubgroup (A : Finset G) (h) : (symmetricSubgroup A h : Set G) = A * A⁻¹ := by
-  rw [symmetricSubgroup_coe, eq_comm]
+lemma coe_symmetricSubgroup' (A : Finset G) (h) : (symmetricSubgroup A h : Set G) = A * A⁻¹ := by
+  rw [coe_symmetricSubgroup, eq_comm]
   norm_cast
   exact mul_comm_of_doubling (by qify at h ⊢; linarith)
 
@@ -180,7 +180,7 @@ lemma A_subset_aH (a : G) (ha : a ∈ A) : A ⊆ a • (A⁻¹ * A) := by
 lemma subgroup_strong_bound_left (h : #(A * A) < (3 / 2 : ℚ) * #A) (a : G) (ha : a ∈ A) :
     A * A ⊆ a • op a • (A⁻¹ * A) := by
   have h₁ : (A⁻¹ * A) * (A⁻¹ * A) = A⁻¹ * A := by
-    rw [← coe_inj, coe_mul, coe_mul, ← symmetricSubgroup_coe _ h, coe_mul_coe]
+    rw [← coe_inj, coe_mul, coe_mul, ← coe_symmetricSubgroup _ h, coe_mul_coe]
   have h₂ : a • op a • (A⁻¹ * A) = (a • (A⁻¹ * A)) * (op a • (A⁻¹ * A)) := by
     rw [mul_smul_comm, smul_mul_assoc, h₁, smul_comm]
   rw [h₂]
@@ -246,19 +246,19 @@ theorem very_small_doubling (h : #(A * A) < (3 / 2 : ℚ) * #A) :
   refine ⟨H, inferInstance, ?_, fun a ha ↦ ⟨?_, subset_antisymm ?_ ?_⟩⟩
   · simp [← Nat.card_eq_fintype_card, symmetricSubgroup, ← coe_mul, ← coe_inv, H]
     rwa [Nat.card_eq_finsetCard, subgroup_strong_bound h]
-  · rw [symmetricSubgroup_coe]
+  · rw [coe_symmetricSubgroup]
     exact_mod_cast A_subset_aH a ha
   · rw [Set.subset_set_smul_iff, ← op_inv]
     calc
       a •> (H : Set G) <• a⁻¹ ⊆ a •> (H : Set G) * A⁻¹ := Set.op_smul_set_subset_mul (by simpa)
       _ ⊆ A * (H : Set G) * A⁻¹ := by gcongr; exact Set.smul_set_subset_mul (by simpa)
       _ = H := by
-        rw [symmetricSubgroup_coe, ← mul_assoc, ← coe_symmetricSubgroup _ h, mul_assoc,
-          ← coe_symmetricSubgroup _ h, ← symmetricSubgroup_coe _ h, coe_mul_coe]
+        rw [coe_symmetricSubgroup, ← mul_assoc, ← coe_symmetricSubgroup' _ h, mul_assoc,
+          ← coe_symmetricSubgroup' _ h, ← coe_symmetricSubgroup _ h, coe_mul_coe]
   · rw [Set.subset_set_smul_iff]
     calc
       a⁻¹ •> ((H : Set G) <• a) ⊆ A⁻¹ * (H : Set G) <• a := Set.smul_set_subset_mul (by simpa)
       _ ⊆ A⁻¹ * ((H : Set G) * A) := by gcongr; exact Set.op_smul_set_subset_mul (by simpa)
       _ = H := by
-        rw [coe_symmetricSubgroup, mul_assoc, ← symmetricSubgroup_coe _ h, ← mul_assoc,
-          ← symmetricSubgroup_coe _ h, ← coe_symmetricSubgroup _ h, coe_mul_coe]
+        rw [coe_symmetricSubgroup', mul_assoc, ← coe_symmetricSubgroup _ h, ← mul_assoc,
+          ← coe_symmetricSubgroup _ h, ← coe_symmetricSubgroup' _ h, coe_mul_coe]