Bump mathlib

Author: YaelDillies

LeanCamCombi.lean

@@ -12,21 +12,17 @@ import LeanCamCombi.ExampleSheets.Graph.ES1
 import LeanCamCombi.ExampleSheets.Graph.ES2
 import LeanCamCombi.GrowthInGroups.Lecture1
 import LeanCamCombi.GrowthInGroups.Lecture2
-import LeanCamCombi.GrowthInGroups.NormCommutator
 import LeanCamCombi.GrowthInGroups.SmallTripling
 import LeanCamCombi.Impact
 import LeanCamCombi.Incidence
 import LeanCamCombi.Kneser.Kneser
 import LeanCamCombi.Kneser.KneserRuzsa
 import LeanCamCombi.Kneser.MulStab
 import LeanCamCombi.LittlewoodOfford
-import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
-import LeanCamCombi.Mathlib.Algebra.Group.Subgroup.Pointwise
 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.Normed.Field.Basic
 import LeanCamCombi.Mathlib.Combinatorics.Additive.PluenneckeRuzsa
 import LeanCamCombi.Mathlib.Combinatorics.Schnirelmann
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic
@@ -41,10 +37,8 @@ import LeanCamCombi.Mathlib.Data.List.DropRight
 import LeanCamCombi.Mathlib.Data.Multiset.Basic
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.Finite
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
-import LeanCamCombi.Mathlib.GroupTheory.Coset.Card
 import LeanCamCombi.Mathlib.GroupTheory.Nilpotent
 import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement
-import LeanCamCombi.Mathlib.GroupTheory.QuotientGroup.Finite
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 import LeanCamCombi.Mathlib.Order.Interval.Finset.Defs
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition

LeanCamCombi/Archive/CauchyDavenportFromKneser.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.GroupTheory.SpecificGroups.Cyclic
-import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import LeanCamCombi.Kneser.Kneser
 
 /-!
@@ -30,7 +29,7 @@ lemma ZMod.cauchy_davenport' {p : ℕ} (hp : p.Prime) {s t : Finset (ZMod p)} (h
   haveI : Fact p.Prime := ⟨hp⟩
   obtain h | h := eq_bot_or_eq_top (AddAction.stabilizer (ZMod p) (s + t))
   · refine min_le_of_right_le ?_
-    rw [← AddSubgroup.coe_set_eq_zero, ← coe_addStab (hs.add ht), coe_eq_zero] at h
+    rw [← coe_set_eq_zero, ← coe_addStab (hs.add ht), coe_eq_zero] at h
     simpa [*] using add_kneser s t
   · rw [← AddSubgroup.coe_eq_univ, ← coe_addStab (hs.add ht), coe_eq_univ] at h
     refine card_addStab_le_card.trans' ?_

LeanCamCombi/GrowthInGroups/Lecture1.lean

@@ -2,7 +2,6 @@ import Mathlib.Analysis.SpecialFunctions.Log.Basic
 import Mathlib.Combinatorics.Additive.DoublingConst
 import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
 import Mathlib.Tactic.Positivity.Finset
-import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import LeanCamCombi.Mathlib.GroupTheory.Nilpotent
 import LeanCamCombi.Mathlib.Order.SuccPred.Relation
 

LeanCamCombi/GrowthInGroups/Lecture2.lean

@@ -1,14 +1,11 @@
-
-import Mathlib.Combinatorics.Additive.DoublingConst
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Fin.VecNotation
 import Mathlib.Tactic.FinCases
 import Mathlib.Tactic.NormNum
-import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import LeanCamCombi.GrowthInGroups.SmallTripling
 
 open Fin Finset List
-open scoped Combinatorics.Additive Pointwise
+open scoped Pointwise
 
 namespace GrowthInGroups.Lecture2
 variable {G : Type*} [DecidableEq G] [CommGroup G] {A : Finset G} {k K : ℝ} {m : ℕ}

LeanCamCombi/GrowthInGroups/NormCommutator.lean

@@ -5,7 +5,6 @@ import Mathlib.Tactic.FinCases
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.Positivity.Finset
 import Mathlib.Tactic.Ring
-import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
 
 /-!
 # Small tripling implies small powers

LeanCamCombi/GrowthInGroups/SmallTripling.lean

@@ -3,8 +3,8 @@ 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.Group.Pointwise.Finset.Basic
 import Mathlib.Data.Nat.Lattice
-import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
 
 /-!
 # Impact function
@@ -34,7 +34,7 @@ variable [Group α] {n : ℕ}
 
 @[to_additive (attr := simp)]
 lemma mulImpact_singleton [Infinite α] (a : α) (n : ℕ) : ({a} : Finset α).mulImpact n = n := by
-  simp only [mulImpact, singleton_mul', card_smul_finset]
+  simp only [mulImpact, singleton_mul, card_smul_finset]
   haveI : Nonempty {t : Finset α // #t = n} := nonempty_subtype.2 (exists_card_eq _)
   exact Eq.trans (iInf_congr Subtype.prop) ciInf_const
 

LeanCamCombi/Impact.lean

@@ -62,9 +62,7 @@ lemma mulStab_mul_ssubset_mulStab (hs₁ : (s ∩ a • C.mulStab).Nonempty)
       rw [smul_mulStab hd, smul_mulStab hc, mem_mulStab hCne, ← smul_smul,
         (mem_mulStab hCne).mp hy, (mem_mulStab hCne).mp hx]
     apply subset_trans (div_subset_div_right this) _
-    have hsing : (x * y) • C.mulStab = {x * y} * C.mulStab := by rw [singleton_mul]; rfl
-    simp_rw [hsing, singleton_mul, div_singleton, image_image, div_eq_mul_inv, mul_comm, comp_def,
-      mul_inv_cancel_right, image_id', subset_refl]
+    simp [singleton_mul, div_eq_inv_mul, smul_smul, mul_assoc]
   have : (a * b) • C.mulStab = (a * c * (b * d)) • C.mulStab := by
     rw [smul_eq_iff_eq_inv_smul, ← smul_assoc, smul_eq_mul, mul_assoc, mul_comm c _, ← mul_assoc, ←
       mul_assoc, ← mul_assoc, mul_assoc _ a b, inv_mul_cancel (a * b), one_mul, ← smul_eq_mul,
@@ -302,7 +300,7 @@ theorem mul_kneser :
   obtain hstab | hstab := ne_or_eq (s * t).mulStab 1
   · have image_coe_mul :
       ((s * t).image (↑) : Finset (α ⧸ stabilizer α (s * t))) = s.image (↑) * t.image (↑) :=
-      sorry -- image_mul (QuotientGroup.mk' _ : α →* α ⧸ stabilizer α (s * t))
+      image_mul (QuotientGroup.mk' _ : α →* α ⧸ stabilizer α (s * t))
     suffices hineq :
       #(s * t).mulStab *
           (#(s.image (↑) : Finset (α ⧸ stabilizer α (s * t))) +
@@ -390,10 +388,10 @@ theorem mul_kneser :
   have hbt₁ : b ∈ t₁ := mem_inter.mpr ⟨hb, mem_smul_finset.2 ⟨1, one_mem_mulStab.2 hC, mul_one _⟩⟩
   have hs₁ne : s₁.Nonempty := ⟨_, has₁⟩
   have ht₁ne : t₁.Nonempty := ⟨_, hbt₁⟩
-  set C₁ := C ∪ s₁ * t₁ with hC₁
-  set C₂ := C ∪ s₂ * t₂ with hC₂
+  set C₁ := C ∪ s₁ * t₁
+  set C₂ := C ∪ s₂ * t₂
   set H₁ := (s₁ * t₁).mulStab with hH₁
-  set H₂ := (s₂ * t₂).mulStab with hH₂
+  set H₂ := (s₂ * t₂).mulStab
   have hC₁st : C₁ ⊆ s * t := union_subset hCst (mul_subset_mul hs₁s ht₁t)
   have hC₂st : C₂ ⊆ s * t := union_subset hCst (mul_subset_mul hs₂s ht₂t)
   have hstabH₁ : s₁ * t₁ ⊆ (a * b) • H := by

LeanCamCombi/Kneser/Kneser.lean

@@ -5,15 +5,13 @@ Authors: Mantas Bakšys, Yaël Dillies
 -/
 import Mathlib.Algebra.Pointwise.Stabilizer
 import Mathlib.GroupTheory.Coset.Card
+import Mathlib.GroupTheory.GroupAction.Blocks
 import Mathlib.GroupTheory.GroupAction.Quotient
-import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.Finite
-import LeanCamCombi.Mathlib.GroupTheory.QuotientGroup.Finite
 
 /-!
 # Stabilizer of a finset
 
-
 This file defines the stabilizer of a finset of a group as a finset.
 
 ## Main declarations
@@ -228,7 +226,7 @@ lemma pairwiseDisjoint_smul_finset_mulStab (s : Finset α) :
   rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩
   simp only [onFun, id_eq]
   simp_rw [← disjoint_coe, ← coe_injective.ne_iff, coe_smul_finset, coe_mulStab hs]
-  exact Subgroup.pairwiseDisjoint_smul _ (Set.mem_range_self _) (Set.mem_range_self _)
+  exact fun h ↦ isBlock_subgroup h
 
 @[to_additive]
 lemma disjoint_smul_finset_mulStab_mul_mulStab :
@@ -336,27 +334,24 @@ lemma card_mulStab_mul_card_image_coe (s t : Finset α) :
   have h1 : Fintype.card ((s * t : Finset α) : Set α) = Fintype.card (s * t) := by congr
   have h2 : (s +ˢ stabilizer α (s * t)) * (t +ˢ stabilizer α (s * t)) =
     ↑((s +ₛ stabilizer α (s * t)) * (t +ₛ stabilizer α (s * t))) := by simp
-  sorry
-  -- have h3 :
-  --   Fintype.card (((s : Set α).image coe : Set (α ⧸ stabilizer α (s * t))) * coe '' (t : Set α)) =
-  --     Fintype.card ((s.image coe : Finset (α ⧸ stabilizer α (s * t))) * image coe t) := by
-  --   simp_rw [h2]
-  --   congr
-  -- simp only [h1, h3, Fintype.card_coe] at temp
-  -- rw [temp]
+  have h3 :
+    Fintype.card ((s +ˢ stabilizer α (s * t)) * (t +ˢ stabilizer α (s * t))) =
+      Fintype.card ((s +ₛ stabilizer α (s * t)) * (t +ₛ stabilizer α (s * t))) := by
+    simp_rw [h2]
+    congr
+  simp only [h1, h3, Fintype.card_coe] at temp
+  rw [temp]
 
 @[to_additive]
 lemma subgroup_mul_card_eq_mul_of_mul_stab_subset (s : Subgroup α) (t : Finset α)
     (hst : (s : Set α) ⊆ t.mulStab) : Nat.card s * #(t +ₛ s) = #t := by
-  have h : (t : Set α) * s = t := by
-    apply Set.Subset.antisymm (Set.Subset.trans (Set.mul_subset_mul_left hst) _)
-    · intro x
-      rw [Set.mem_mul]
-      aesop
-    · rw [← coe_mul, mul_mulStab]
-  have := s.subgroup_mul_card_eq_mul t
-  rw [h] at this
-  simpa
+  suffices h : (t : Set α) * s = t by
+    simpa [h, eq_comm] using s.card_mul_eq_card_subgroup_mul_card_quotient  t
+  apply Set.Subset.antisymm (Set.Subset.trans (Set.mul_subset_mul_left hst) _)
+  · intro x
+    rw [Set.mem_mul]
+    aesop
+  · rw [← coe_mul, mul_mulStab]
 
 @[to_additive]
 lemma mulStab_quotient_commute_subgroup (s : Subgroup α) (t : Finset α)