Bump mathlib

LeanCamCombi.lean

@@ -14,7 +14,6 @@ import LeanCamCombi.GraphTheory.ExampleSheet2
 import LeanCamCombi.GroupMarking
 import LeanCamCombi.GrowthInGroups.ApproximateSubgroup
 import LeanCamCombi.GrowthInGroups.BooleanSubalgebra
-import LeanCamCombi.GrowthInGroups.CardPowGeneratingSet
 import LeanCamCombi.GrowthInGroups.CardQuotient
 import LeanCamCombi.GrowthInGroups.Chevalley
 import LeanCamCombi.GrowthInGroups.ChevalleyComplex
@@ -26,9 +25,9 @@ import LeanCamCombi.GrowthInGroups.Lecture1
 import LeanCamCombi.GrowthInGroups.Lecture2
 import LeanCamCombi.GrowthInGroups.Lecture3
 import LeanCamCombi.GrowthInGroups.Lecture4
+import LeanCamCombi.GrowthInGroups.LinearLowerBound
 import LeanCamCombi.GrowthInGroups.NoDoubling
 import LeanCamCombi.GrowthInGroups.PrimeSpectrumPolynomial
-import LeanCamCombi.GrowthInGroups.SMulCover
 import LeanCamCombi.GrowthInGroups.SpanRangeUpdate
 import LeanCamCombi.GrowthInGroups.VerySmallDoubling
 import LeanCamCombi.GrowthInGroups.WithBotSucc
@@ -39,7 +38,6 @@ import LeanCamCombi.Kneser.KneserRuzsa
 import LeanCamCombi.Kneser.MulStab
 import LeanCamCombi.LittlewoodOfford
 import LeanCamCombi.Mathlib.Algebra.Algebra.Operations
-import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.BigOperators
 import LeanCamCombi.Mathlib.Algebra.Module.Submodule.Defs
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Basic
@@ -82,9 +80,9 @@ import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 import LeanCamCombi.Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
 import LeanCamCombi.Mathlib.MeasureTheory.Measure.OpenPos
 import LeanCamCombi.Mathlib.Order.Flag
+import LeanCamCombi.Mathlib.Order.Monotone.Basic
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
 import LeanCamCombi.Mathlib.Order.RelIso.Group
-import LeanCamCombi.Mathlib.Order.SupClosed
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 import LeanCamCombi.Mathlib.RingTheory.FinitePresentation
 import LeanCamCombi.Mathlib.RingTheory.Ideal.Span

LeanCamCombi/GrowthInGroups/ApproximateSubgroup.lean

@@ -1,11 +1,10 @@
+import Mathlib.Algebra.Group.Subgroup.Pointwise
 import Mathlib.Algebra.Order.BigOperators.Ring.Finset
+import Mathlib.Combinatorics.Additive.CovBySMul
 import Mathlib.Combinatorics.Additive.RuzsaCovering
 import Mathlib.Combinatorics.Additive.SmallTripling
 import Mathlib.Tactic.Bound
-import Mathlib.Algebra.Group.Subgroup.Pointwise
 import LeanCamCombi.Mathlib.Data.Set.Lattice
-import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
-import LeanCamCombi.GrowthInGroups.SMulCover
 
 -- TODO: Unsimp in mathlib
 attribute [-simp] Set.image_subset_iff

LeanCamCombi/GrowthInGroups/BooleanSubalgebra.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Order.Sublattice
-import LeanCamCombi.Mathlib.Order.SupClosed
 
 /-!
 # Boolean subalgebras

LeanCamCombi/GrowthInGroups/Lecture1.lean

@@ -2,7 +2,7 @@ import Mathlib.Analysis.SpecialFunctions.Log.Basic
 import Mathlib.Combinatorics.Additive.DoublingConst
 import Mathlib.GroupTheory.Nilpotent
 import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
-import LeanCamCombi.GrowthInGroups.CardPowGeneratingSet
+import LeanCamCombi.GrowthInGroups.LinearLowerBound
 import LeanCamCombi.GrowthInGroups.NoDoubling
 import LeanCamCombi.GrowthInGroups.VerySmallDoubling
 
@@ -68,7 +68,7 @@ lemma theorem_3_9 :
 open MulAction in
 open scoped RightActions in
 lemma fact_3_10 (hA : #(A * A) ≤ #A) :
-    ∃ H : Subgroup G, ∀ a ∈ A, a •> (H : Set G) = A ∧ (H : Set G) <• a = A := 
+    ∃ H : Subgroup G, ∀ a ∈ A, a •> (H : Set G) = A ∧ (H : Set G) <• a = A :=
   exists_subgroup_of_no_doubling hA
 
 open scoped Classical RightActions in

LeanCamCombi/GrowthInGroups/CardPowGeneratingSet.lean → LeanCamCombi/GrowthInGroups/LinearLowerBound.lean

@@ -3,9 +3,9 @@ Copyright (c) 2024 Yaël Dillies, Patrick Luo, Eric Rodriguez. All rights reserv
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Patrick Luo, Eric Rodriguez
 -/
+import Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import Mathlib.Algebra.Group.Subgroup.Pointwise
 import Mathlib.Data.Nat.SuccPred
-import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
 
 /-!
 # Linear lower bound on the growth of a generating set

LeanCamCombi/GrowthInGroups/NoDoubling.lean

@@ -3,8 +3,8 @@ Copyright (c) 2024 Yaël Dillies, Patrick Luo. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Patrick Luo
 -/
+import Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import Mathlib.GroupTheory.GroupAction.Defs
-import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
 
 /-!
 # Sets with no doubling

LeanCamCombi/GrowthInGroups/VerySmallDoubling.lean

@@ -4,13 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
 import Mathlib.Algebra.BigOperators.Ring
-import Mathlib.Algebra.Group.Subgroup.Pointwise
+import Mathlib.Algebra.Group.Pointwise.Finset.Basic
+import Mathlib.Algebra.Group.Subgroup.Defs
+import Mathlib.Algebra.Group.Submonoid.Pointwise
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
-import Mathlib.Data.Set.Card
+import Mathlib.SetTheory.Cardinal.Finite
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Qify
-import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
-import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 
 open Finset MulOpposite
 open scoped Pointwise

LeanCamCombi/Mathlib/Algebra/Ring/Hom/Defs.lean

@@ -1,9 +1,8 @@
-
 import Mathlib.Algebra.Ring.Hom.Defs
 
 namespace RingHom
 variable {R : Type*} [Semiring R]
 
-@[simp, norm_cast] lemma coe_id : ⇑(id R) = _root_.id := rfl
+attribute [norm_cast] coe_id
 
 end RingHom

LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean

@@ -3,7 +3,6 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Algebra.BigOperators.Group.Finset
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
 
 /-!
@@ -212,7 +211,7 @@ noncomputable def labelledCopyCount (G : SimpleGraph α) (H : SimpleGraph β) :
   exact { default := ⟨default, isEmptyElim⟩, uniq := fun _ ↦ Subsingleton.elim _ _ }
 
 @[simp] lemma labelledCopyCount_eq_zero : G.labelledCopyCount H = 0 ↔ ¬ G ⊑ H := by
-  simp [labelledCopyCount, IsContained, Fintype.card_eq_zero_iff]
+  simp [labelledCopyCount, IsContained, Fintype.card_eq_zero_iff, isEmpty_subtype]
 
 @[simp] lemma labelledCopyCount_pos : 0 < G.labelledCopyCount H ↔ G ⊑ H := by
   simp [labelledCopyCount, IsContained, Fintype.card_pos_iff]

LeanCamCombi/Mathlib/Data/Finset/Image.lean

@@ -1,14 +1,6 @@
 import Mathlib.Data.Finset.Image
 import LeanCamCombi.Mathlib.Data.Set.Function
 
-namespace Finset
-variable {α β : Type*} [DecidableEq β] {f : α → β} {s : Finset α} {p : β → Prop}
-
-lemma forall_mem_image : (∀ y ∈ s.image f, p y) ↔ ∀ ⦃x⦄, x ∈ s → p (f x) := by simp
-lemma exists_mem_image : (∃ y ∈ s.image f, p y) ↔ ∃ x ∈ s, p (f x) := by simp
-
-end Finset
-
 namespace Finset
 variable {α β : Type*} [DecidableEq α] [DecidableEq β] {s t : Finset α} {f : α → β}
 

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4e07f9201e4e4452cd24cf2bd217e93d28f68a69",
+   "rev": "589875a32a4f2e08e7259507f82ead240179c482",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a988e8b369e20ae90b4998923e4efcd732a1da62",
+   "rev": "d5bed454ee2c347b2d60a12fc609ed827c070617",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -125,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c016aa9938c4cedc9b7066099f99bcae1b1af625",
+   "rev": "9e583efcea920afa13ee2a53069821a2297a94c0",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",