Bump mathlib

LeanCamCombi.lean

@@ -37,15 +37,13 @@ import LeanCamCombi.Kneser.KneserRuzsa
 import LeanCamCombi.Kneser.MulStab
 import LeanCamCombi.LittlewoodOfford
 import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
-import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Basic
 import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.BigOperators
 import LeanCamCombi.Mathlib.Algebra.Group.Subgroup.Lattice
 import LeanCamCombi.Mathlib.Algebra.Group.Subgroup.Pointwise
 import LeanCamCombi.Mathlib.Algebra.Group.Submonoid.Basic
 import LeanCamCombi.Mathlib.Algebra.Group.Submonoid.Pointwise
 import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Equiv
 import LeanCamCombi.Mathlib.Algebra.Order.GroupWithZero.Unbundled
-import LeanCamCombi.Mathlib.Algebra.Pointwise.Stabilizer
 import LeanCamCombi.Mathlib.Algebra.Polynomial.Degree.Lemmas
 import LeanCamCombi.Mathlib.Algebra.Polynomial.Div
 import LeanCamCombi.Mathlib.Algebra.Polynomial.Eval.Degree
@@ -56,7 +54,6 @@ import LeanCamCombi.Mathlib.Analysis.Convex.Extreme
 import LeanCamCombi.Mathlib.Analysis.Convex.Independence
 import LeanCamCombi.Mathlib.Analysis.Convex.SimplicialComplex.Basic
 import LeanCamCombi.Mathlib.Analysis.Normed.Group.Basic
-import LeanCamCombi.Mathlib.Combinatorics.Additive.RuzsaCovering
 import LeanCamCombi.Mathlib.Combinatorics.Schnirelmann
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Containment
@@ -88,10 +85,7 @@ import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 import LeanCamCombi.Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
 import LeanCamCombi.Mathlib.MeasureTheory.Measure.OpenPos
-import LeanCamCombi.Mathlib.NumberTheory.Fermat
-import LeanCamCombi.Mathlib.Order.Chain
 import LeanCamCombi.Mathlib.Order.Flag
-import LeanCamCombi.Mathlib.Order.Monotone.Monovary
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
 import LeanCamCombi.Mathlib.Order.RelIso.Group
 import LeanCamCombi.Mathlib.Order.SupClosed
@@ -101,7 +95,6 @@ import LeanCamCombi.Mathlib.RingTheory.FinitePresentation
 import LeanCamCombi.Mathlib.RingTheory.Ideal.Span
 import LeanCamCombi.Mathlib.RingTheory.LocalRing.ResidueField.Ideal
 import LeanCamCombi.Mathlib.RingTheory.Localization.Integral
-import LeanCamCombi.Mathlib.Topology.MetricSpace.Pseudo.Defs
 import LeanCamCombi.MetricBetween
 import LeanCamCombi.MinkowskiCaratheodory
 import LeanCamCombi.MonovaryOrder

LeanCamCombi/DiscreteDeriv.lean

@@ -1,7 +1,7 @@
 import Mathlib.Algebra.Polynomial.AlgebraMap
 import Mathlib.Algebra.Polynomial.BigOperators
-import Mathlib.Algebra.Polynomial.Degree.Lemmas
-import Mathlib
+import Mathlib.Algebra.Polynomial.Eval.SMul
+import Mathlib.Data.Finsupp.Notation
 
 open Finset
 open scoped BigOperators

LeanCamCombi/GroupMarking.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Analysis.Normed.Group.Basic
-import Mathlib.GroupTheory.FreeGroup.Basic
+import Mathlib.GroupTheory.FreeGroup.Reduce
 
 /-!
 # Marked groups

LeanCamCombi/GrowthInGroups/ApproximateSubgroup.lean

@@ -1,8 +1,8 @@
 import Mathlib.Algebra.Order.BigOperators.Ring.Finset
+import Mathlib.Combinatorics.Additive.RuzsaCovering
 import Mathlib.Combinatorics.Additive.SmallTripling
 import Mathlib.Tactic.Bound
-import LeanCamCombi.Mathlib.Algebra.Group.Subgroup.Pointwise
-import LeanCamCombi.Mathlib.Combinatorics.Additive.RuzsaCovering
+import Mathlib.Algebra.Group.Subgroup.Pointwise
 import LeanCamCombi.Mathlib.Data.Set.Lattice
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.GrowthInGroups.SMulCover
@@ -117,7 +117,7 @@ lemma pow_inter_pow_covBySMul_sq_inter_sq
   obtain ⟨F₁, hF₁, hAF₁⟩ := hA.sq_covBySMul
   obtain ⟨F₂, hF₂, hBF₂⟩ := hB.sq_covBySMul
   have := hA.one_le
-  choose f hf using exists_smul_inter_smul_subset_smul_sq_inter_sq hA.inv_eq_self hB.inv_eq_self
+  choose f hf using exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul A B
   refine ⟨.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)), ?_, ?_⟩
   · calc
       (#(.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) : ℝ)
@@ -129,8 +129,10 @@ lemma pow_inter_pow_covBySMul_sq_inter_sq
         gcongr <;> apply pow_subset_pow_mul_of_sq_subset_mul <;> norm_cast <;> omega
       _ = ⋃ (a ∈ F₁ ^ (m - 1)) (b ∈ F₂ ^ (n - 1)), a • A ∩ b • B := by
         simp_rw [← smul_eq_mul, ← iUnion_smul_set, iUnion₂_inter_iUnion₂]; norm_cast
-      _ ⊆ ⋃ (a ∈ F₁ ^ (m - 1)) (b ∈ F₂ ^ (n - 1)), f a b • (A ^ 2 ∩ B ^ 2) := by gcongr; exact hf ..
+      _ ⊆ ⋃ (a ∈ F₁ ^ (m - 1)) (b ∈ F₂ ^ (n - 1)), f a b • (A⁻¹ * A ∩ (B⁻¹ * B)) := by
+        gcongr; exact hf ..
       _ = (Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) * (A ^ 2 ∩ B ^ 2) := by
+        simp_rw [hA.inv_eq_self, hB.inv_eq_self, ← sq]
         rw [Finset.coe_image₂, ← smul_eq_mul, ← iUnion_smul_set, biUnion_image2]
         simp_rw [Finset.mem_coe]
 

LeanCamCombi/GrowthInGroups/CardPowGeneratingSet.lean

@@ -68,7 +68,7 @@ lemma card_pow_strictMonoOn (hX₁ : 1 ∈ X) (hX : X.Nontrivial) :
     rw [eq_comm, coe_set_eq_one, closure_eq_bot_iff] at hm
     cases hX.not_subset_singleton hm
   calc (X : Set G) ^ (n - 1) = X ^ (n - m) * X ^ (m - 1) := by rw [← pow_add]; congr 1; omega
-  _ = closure (X : Set G) := by rw [hm, Set.mul_subgroupClosure_pow hX.nonempty.to_set]
+  _ = closure (X : Set G) := by rw [hm, Set.pow_mul_subgroupClosure hX.nonempty.to_set]
 
 @[to_additive]
 lemma card_pow_strictMono (hX₁ : 1 ∈ X) (hXclosure : (closure (X : Set G) : Set G).Infinite) :

LeanCamCombi/GrowthInGroups/CardQuotient.lean

@@ -57,7 +57,7 @@ lemma le_card_quotient_mul_sq_inter_subgroup (hAsymm : A⁻¹ = A) :
   calc
     #(bipartiteBelow (π · = ·) A (π a))
     _ ≤ #((bipartiteBelow (π · = ·) A (π a))⁻¹ * (bipartiteBelow (π · = ·) A (π a))) :=
-      card_le_card_mul_left _ ⟨a⁻¹, by simpa⟩
+      card_le_card_mul_left ⟨a⁻¹, by simpa⟩
     _ ≤ #{x ∈ A⁻¹ * A | x ∈ H} := by
       gcongr
       simp only [mul_subset_iff, mem_inv', mem_bipartiteBelow, map_inv, Finset.mem_filter, and_imp]

LeanCamCombi/GrowthInGroups/Lecture2.lean

@@ -7,8 +7,8 @@ open scoped Pointwise
 namespace GrowthInGroups.Lecture2
 variable {G : Type*} [DecidableEq G] [Group G] {A : Finset G} {k K : ℝ} {m : ℕ}
 
-lemma lemma_4_2 (U V W : Finset G) : #U * #(V⁻¹ * W) ≤ #(U * V) * #(U * W) := by
-  exact ruzsa_triangle_inequality_invMul_mul_mul ..
+lemma lemma_4_2 (U V W : Finset G) : #U * #(V⁻¹ * W) ≤ #(U * V) * #(U * W) :=
+  ruzsa_triangle_inequality_invMul_mul_mul ..
 
 lemma lemma_4_3_2 (hA : #(A ^ 2) ≤ K * #A) : #(A⁻¹ * A) ≤ K ^ 2 * #A := by
   obtain rfl | hA₀ := A.eq_empty_or_nonempty
@@ -61,6 +61,6 @@ lemma lemma_4_7 {A : Finset G} (hA₁ : 1 ∈ A) (hsymm : A⁻¹ = A) (hA : #(A
     IsApproximateSubgroup (K ^ 3) (A ^ 2 : Set G) := .of_small_tripling hA₁ hsymm hA
 
 lemma lemma_4_8 {A B : Finset G} (hB : B.Nonempty) (hK : #(A * B) ≤ K * #B) :
-    ∃ F ⊆ A, #F ≤ K ∧ A ⊆ F * B / B := ruzsa_covering_mul hB hK
+    ∃ F ⊆ A, #F ≤ K ∧ A ⊆ F * (B / B) := ruzsa_covering_mul hB hK
 
 end GrowthInGroups.Lecture2

LeanCamCombi/GrowthInGroups/Lecture3.lean

@@ -12,7 +12,7 @@ lemma lemma_5_1 [DecidableEq G] {A : Finset G} (hA₁ : 1 ∈ A) (hAsymm : A⁻
   .of_small_tripling hA₁ hAsymm hA
 
 lemma lemma_5_2 [DecidableEq G] {A B : Finset G} (hB : B.Nonempty) (hK : #(A * B) ≤ K * #B) :
-    ∃ F ⊆ A, #F ≤ K ∧ A ⊆ F * B / B := ruzsa_covering_mul hB hK
+    ∃ F ⊆ A, #F ≤ K ∧ A ⊆ F * (B / B) := ruzsa_covering_mul hB hK
 
 open scoped RightActions
 lemma proposition_5_3 [DecidableEq G] {A : Finset G} (hA₀ : A.Nonempty) (hA : #(A ^ 2) ≤ K * #A) :
@@ -34,8 +34,8 @@ lemma proposition_5_6_2 (hA : IsApproximateSubgroup K A) (hB : IsApproximateSubg
   hA.pow_inter_pow hB hm hn
 
 lemma lemma_5_7 (hA : A⁻¹ = A) (hB : B⁻¹ = B) (x y : G) :
-    ∃ z : G, x • A ∩ y • B ⊆ z • (A ^ 2 ∩ B ^ 2) :=
-  Set.exists_smul_inter_smul_subset_smul_sq_inter_sq hA hB x y
+    ∃ z : G, x • A ∩ y • B ⊆ z • (A ^ 2 ∩ B ^ 2) := by
+  simpa [hA, hB, sq] using Set.exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul A B x y
 
 open scoped Classical in
 lemma lemma_5_8_1 {H : Subgroup G} [H.Normal] {A : Finset G} :

LeanCamCombi/Kneser/Kneser.lean

@@ -469,8 +469,7 @@ theorem mul_kneser :
           (card_mulStab_dvd_card_mul_mulStab _ _).natCast) $
         (card_mulStab_dvd_card_mul_mulStab _ _).natCast).trans ?_
     rw [sub_sub]
-    exact sub_le_sub_left (add_le_add (Nat.cast_le.2 $ card_le_card_mul_right _ hH₁ne) $
-      Nat.cast_le.2 $ card_le_card_mul_right _ hH₁ne) _
+    gcongr _ - (Nat.cast ?_ + Nat.cast ?_) <;> exact card_le_card_mul_right hH₁ne
   have aux2₂ : (#s₂ : ℤ) + #t₂ + #H₂ ≤ #H := by
     rw [← le_sub_iff_add_le']
     refine (Int.le_of_dvd ((sub_nonneg_of_le $ Nat.cast_le.2 $ card_le_card $
@@ -479,16 +478,16 @@ theorem mul_kneser :
           (card_mulStab_dvd_card_mul_mulStab _ _).natCast) $
         (card_mulStab_dvd_card_mul_mulStab _ _).natCast).trans ?_
     rw [sub_sub]
-    exact sub_le_sub_left (add_le_add (Nat.cast_le.2 $ card_le_card_mul_right _ hH₂ne) $
-      Nat.cast_le.2 $ card_le_card_mul_right _ hH₂ne) _
+    exact sub_le_sub_left (add_le_add (Nat.cast_le.2 $ card_le_card_mul_right hH₂ne) $
+      Nat.cast_le.2 $ card_le_card_mul_right hH₂ne) _
   -- Now we deduce inequality (3) using the above lemma in addition to the facts that `s * t` is not
   -- convergent and then induction hypothesis applied to `sᵢ` and `tᵢ`
   have aux3₁ : (#S : ℤ) + #T + #s₁ + #t₁ - #H₁ < #H :=
     calc
       (#S : ℤ) + #T + #s₁ + #t₁ - #H₁
         < #S + #T + #(s ∪ t) + #(s ∩ t) - #(s * t) + #(s₁ * t₁) := by
         have ih₁ :=
-          (add_le_add (card_le_card_mul_right _ hH₁ne) $ card_le_card_mul_right _ hH₁ne).trans
+          (add_le_add (card_le_card_mul_right hH₁ne) $ card_le_card_mul_right hH₁ne).trans
             (ih _ _ hst₁)
         zify at ih₁
         linarith [hstconv, ih₁]
@@ -505,7 +504,7 @@ theorem mul_kneser :
       (#S : ℤ) + #T + #s₂ + #t₂ - #H₂
        < #S + #T + #(s ∪ t) + #(s ∩ t) - #(s * t) + #(s₂ * t₂) := by
         have ih₂ :=
-          (add_le_add (card_le_card_mul_right _ hH₂ne) $ card_le_card_mul_right _ hH₂ne).trans
+          (add_le_add (card_le_card_mul_right hH₂ne) $ card_le_card_mul_right hH₂ne).trans
             (ih _ _ hst₂)
         zify at hstconv ih₂
         linarith [ih₂]

LeanCamCombi/Kneser/KneserRuzsa.lean

@@ -220,7 +220,7 @@ lemma le_card_mul_add_card_mulStab_mul (hs : s.Nonempty) (ht : t.Nonempty) :
   rw [this]
   refine (le_inf' ht _ fun b hb ↦ ?_).trans (le_card_sup_add_card_mulStab_sup _)
   rw [← hstcard b hb]
-  refine add_le_add (card_le_card_mul_right _ ⟨_, hbt' _ hb⟩)
+  refine add_le_add (card_le_card_mul_right ⟨_, hbt' _ hb⟩)
     ((card_mono $ subset_mulStab_mul_left ⟨_, hbt' _ hb⟩).trans' ?_)
   rw [← card_smul_finset (b : α)⁻¹ (t' _)]
   refine card_mono ((mul_subset_left_iff $ hs.mono $ hs' _ hb).1 ?_)

LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

@@ -14,37 +14,4 @@ lemma smul_finset_subset_mul : a ∈ s → a • t ⊆ s * t := image_subset_ima
 attribute [gcongr] div_subset_div_left div_subset_div_right
 
 end Mul
-
-section Monoid
-variable [Monoid α] {s t : Finset α} {a : α} {n : ℕ}
-
-@[to_additive]
-lemma subset_pow (hs : 1 ∈ s) (hn : n ≠ 0) : s ⊆ s ^ n := by
-  simpa using pow_subset_pow_right hs <| Nat.one_le_iff_ne_zero.2 hn
-
-end Monoid
-
-section CancelMonoid
-variable [CancelMonoid α] {s t : Finset α} {a : α} {n : ℕ}
-
-@[to_additive]
-lemma Nontrivial.mul_right : s.Nontrivial → t.Nonempty → (s * t).Nontrivial := by
-  rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩
-  exact ⟨a * c, mul_mem_mul ha hc, b * c, mul_mem_mul hb hc, by simpa⟩
-
-@[to_additive]
-lemma Nontrivial.mul_left : t.Nontrivial → s.Nonempty → (s * t).Nontrivial := by
-  rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩
-  exact ⟨c * a, mul_mem_mul hc ha, c * b, mul_mem_mul hc hb, by simpa⟩
-
-@[to_additive]
-lemma Nontrivial.mul (hs : s.Nontrivial) (ht : t.Nontrivial) : (s * t).Nontrivial :=
-  hs.mul_right ht.nonempty
-
-@[to_additive]
-lemma Nontrivial.pow (hs : s.Nontrivial) : ∀ {n}, n ≠ 0 → (s ^ n).Nontrivial
-  | 1, _ => by simpa
-  | n + 2, _ => by simpa [pow_succ] using (hs.pow n.succ_ne_zero).mul hs
-
-end CancelMonoid
 end Finset

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

@@ -1,5 +1,4 @@
 import Mathlib.Algebra.Group.Subgroup.Pointwise
-import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Basic
 import LeanCamCombi.Mathlib.Algebra.Group.Subgroup.Lattice
 
 open Set Subgroup
@@ -24,29 +23,3 @@ lemma closure_pow (hs : 1 ∈ s) (hn : n ≠ 0) : closure (s ^ n) = closure s :=
   (closure_pow_le hn).antisymm <| by gcongr; exact subset_pow hs hn
 
 end Subgroup
-
-
-namespace Set
-variable {G : Type*} [Group G] {s : Set G}
-
-@[to_additive (attr := simp)]
-lemma mul_subgroupClosure (hs : s.Nonempty) : s * closure s = closure s := by
-  rw [← smul_eq_mul, ← Set.iUnion_smul_set]
-  have h a (ha : a ∈ s) : a • (closure s : Set G) = closure s :=
-    smul_coe_set <| subset_closure ha
-  simp (config := {contextual := true}) [h, hs]
-
-@[to_additive (attr := simp)]
-lemma mul_subgroupClosure_pow (hs : s.Nonempty) : ∀ n, s ^ n * closure s = closure s
-  | 0 => by simp
-  | n + 1 => by rw [pow_add, pow_one, mul_assoc, mul_subgroupClosure hs, mul_subgroupClosure_pow hs]
-
-end Set
-
-variable {G S : Type*} [Group G] [SetLike S G] [SubgroupClass S G] {s : Set G} {n : ℕ}
-
-set_option linter.unusedVariables false in
-@[to_additive (attr := simp)]
-lemma coe_set_pow : ∀ {n} (hn : n ≠ 0) (H : S), (H ^ n : Set G) = H
-  | 1, _, H => by simp
-  | n + 2, _, H => by rw [pow_succ, coe_set_pow n.succ_ne_zero, coe_mul_coe]

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

@@ -1,5 +1,4 @@
 import Mathlib.Algebra.Group.Submonoid.Pointwise
-import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Basic
 import LeanCamCombi.Mathlib.Algebra.Group.Submonoid.Basic
 
 open Set