Bump mathlib

Author: YaelDillies

LeanCamCombi.lean

@@ -17,7 +17,6 @@ import LeanCamCombi.GrowthInGroups.Constructible
 import LeanCamCombi.GrowthInGroups.Lecture1
 import LeanCamCombi.GrowthInGroups.Lecture2
 import LeanCamCombi.GrowthInGroups.Lecture3
-import LeanCamCombi.GrowthInGroups.SmallTripling
 import LeanCamCombi.GrowthInGroups.VerySmallDoubling
 import LeanCamCombi.Impact
 import LeanCamCombi.Incidence
@@ -32,7 +31,6 @@ 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.Combinatorics.Additive.PluenneckeRuzsa
 import LeanCamCombi.Mathlib.Combinatorics.Schnirelmann
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Containment

LeanCamCombi/BernoulliSeq.lean

@@ -138,8 +138,8 @@ protected lemma union (h : IndepFun X Y μ) :
   convert (hX.compl.inter hY.compl _).compl using 1
   · simp [compl_inter]
   · rw [mul_tsub, mul_one, tsub_tsub, tsub_tsub_cancel_of_le, tsub_mul, one_mul,
-      add_tsub_assoc_of_le (mul_le_of_le_one_left' $ hX.le_one)]
-    · exact (add_le_add_left (mul_le_of_le_one_right' $ hY.le_one) _).trans_eq
+      add_tsub_assoc_of_le (mul_le_of_le_one_left' hX.le_one)]
+    · exact (add_le_add_left (mul_le_of_le_one_right' hY.le_one) _).trans_eq
         (add_tsub_cancel_of_le hX.le_one)
   · rwa [IndepFun_iff, MeasurableSpace.comap_compl measurable_compl,
       MeasurableSpace.comap_compl measurable_compl, ← IndepFun_iff]

LeanCamCombi/ErdosRenyi/Basic.lean

@@ -18,12 +18,11 @@ open scoped Finset ENNReal NNReal
 variable {α Ω : Type*} [MeasurableSpace Ω]
 
 /-- A sequence iid. real valued Bernoulli random variables with parameter `p ≤ 1`. -/
-abbrev ErdosRenyi (G : Ω → SimpleGraph α) [∀ ω, DecidableRel (G ω).Adj] (p : ℝ≥0)
-    (μ : Measure Ω := by volume_tac) : Prop :=
+abbrev ErdosRenyi (G : Ω → SimpleGraph α) (p : ℝ≥0) (μ : Measure Ω := by volume_tac) : Prop :=
   IsBernoulliSeq (fun ω ↦ (G ω).edgeSet) p μ
 
-variable {G : Ω → SimpleGraph α} {H : SimpleGraph α} [∀ ω, DecidableRel (G ω).Adj] {p : ℝ≥0}
-  (μ : Measure Ω) (hG : ErdosRenyi G p μ)
+variable {G : Ω → SimpleGraph α} {H : SimpleGraph α} {p : ℝ≥0} (μ : Measure Ω)
+  (hG : ErdosRenyi G p μ)
 
 namespace ErdosRenyi
 include hG

LeanCamCombi/GrowthInGroups/Chevalley.lean

@@ -146,12 +146,6 @@ lemma LinearMap.charpoly_baseChange {R M} [CommRing R] [AddCommGroup M] [Module
   ext i j
   simp [Matrix.map_apply, LinearMap.toMatrix_apply, ← Algebra.algebraMap_eq_smul_one]
 
-lemma Algebra.baseChange_lmul {R B} [CommRing R] [CommRing B] [Algebra R B]
-    {A} [CommRing A] [Algebra R A] (f : B) :
-    (Algebra.lmul R B f).baseChange A = Algebra.lmul A (A ⊗[R] B) (1 ⊗ₜ f) := by
-  ext i
-  simp
-
 lemma isNilpotent_tensor_residueField_iff
     [Module.Free R A] [Module.Finite R A] (f : A) (I : Ideal R) [I.IsPrime] :
     IsNilpotent (algebraMap A (A ⊗[R] I.ResidueField) f) ↔

LeanCamCombi/GrowthInGroups/Lecture2.lean

@@ -1,6 +1,6 @@
+import Mathlib.Combinatorics.Additive.SmallTripling
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.Interval
 import LeanCamCombi.GrowthInGroups.ApproximateSubgroup
-import LeanCamCombi.GrowthInGroups.SmallTripling
 
 open Fin Finset List
 open scoped Pointwise

LeanCamCombi/GrowthInGroups/Lecture3.lean

@@ -1,6 +1,5 @@
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.Interval
 import LeanCamCombi.GrowthInGroups.ApproximateSubgroup
-import LeanCamCombi.GrowthInGroups.SmallTripling
 
 open Fin Finset List
 open scoped Pointwise

LeanCamCombi/GrowthInGroups/SmallTripling.lean

@@ -86,7 +86,7 @@ lemma modPartitions_parts_eq (s d : ℕ) (hd : d ≠ 0) (h : d ≤ s) :
     exact Nat.sub_pos_of_lt (hi.trans_le h)
   · rintro ⟨hj, rfl⟩
     refine ⟨j / d, ?_, Nat.mod_add_div _ _⟩
-    rwa [Nat.le_div_iff_mul_le' hd.bot_lt, Nat.le_sub_iff_add_le, Nat.le_sub_iff_add_le',
+    rwa [Nat.le_div_iff_mul_le hd.bot_lt, Nat.le_sub_iff_add_le, Nat.le_sub_iff_add_le',
       ← add_assoc, mul_comm, Nat.mod_add_div, Nat.add_one_le_iff]
     · exact hi.le.trans h
     rw [Nat.succ_le_iff]

LeanCamCombi/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean

@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "93bcfd774f89d3874903cab06abfbf69f327cbd9",
+   "rev": "5dfdc66e0d503631527ad90c1b5d7815c86a8662",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8aca2144b9fdaf45417cdb129c75699ddf4da4c8",
+   "rev": "ca888d9ee43cf9055ecce7fa541510cf68b425d6",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,