Bump mathlib

Author: YaelDillies

LeanCamCombi.lean

@@ -42,7 +42,6 @@ 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.SuccPred.Relation
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 import LeanCamCombi.MetricBetween
 import LeanCamCombi.MinkowskiCaratheodory

LeanCamCombi/GrowthInGroups/Lecture1.lean

@@ -3,32 +3,37 @@ import Mathlib.Combinatorics.Additive.DoublingConst
 import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
 import Mathlib.Tactic.Positivity.Finset
 import LeanCamCombi.Mathlib.GroupTheory.Nilpotent
-import LeanCamCombi.Mathlib.Order.SuccPred.Relation
 
 open Finset Fintype Group Matrix MulOpposite Real
 open scoped Combinatorics.Additive MatrixGroups Pointwise
 
 namespace GrowthInGroups.Lecture1
 variable {G : Type*} [Group G] [DecidableEq G] {A X : Finset G} {n : ℕ} {K : ℝ}
 
+lemma card_pow_lt_card_pow_succ_of_pow_ne_closure (hX : X.Nonempty)
+    (hXclosure : (X ^ n : Set G) ≠ Subgroup.closure (X : Set G)) : #(X ^ n) < #(X ^ (n + 1)) := by
+  refine (hX.card_pow_mono <| Order.le_succ _).lt_of_ne fun h ↦ hXclosure ?_
+  dsimp at h
+  sorry
+
 lemma card_pow_strictMonoOn (hX : X.Nonempty) :
     StrictMonoOn (fun n ↦ #(X ^ n))
       {n | (X ^ (n - 1) : Set G) ≠ Subgroup.closure (X : Set G)} := by
-  refine Order.strictMonoOn_of_lt_succ ⟨fun _ _ m hm n ⟨_, hmn⟩ hn ↦ sorry⟩ fun n hn hn' ↦ ?_
-  refine (hX.card_pow_mono <| Order.le_succ _).lt_of_ne fun h ↦ hn' ?_
-  dsimp at h
-  dsimp
+  refine strictMonoOn_of_lt_add_one ⟨fun _ _ m hm n ⟨_, hmn⟩ hn ↦ hm ?_⟩ fun n _ hn hn' ↦
+    card_pow_lt_card_pow_succ_of_pow_ne_closure hX hn'
   sorry
 
-lemma card_pow_strictMono (hX : X.Nonempty)
-    (hXclosure : (Subgroup.closure (X : Set G) : Set G).Infinite) :
+lemma card_pow_strictMono (hXclosure : (Subgroup.closure (X : Set G) : Set G).Infinite) :
     StrictMono fun n ↦ #(X ^ n) := by
-  have h n : (X ^ (n - 1) : Set G) ≠ Subgroup.closure (X : Set G) := sorry
+  obtain rfl | hX := X.eq_empty_or_nonempty
+  · simp at hXclosure
+  have h n : (X ^ (n - 1) : Set G) ≠ Subgroup.closure (X : Set G) :=
+    fun h ↦ by simp [← h, ← coe_pow] at hXclosure
   simpa [h] using card_pow_strictMonoOn hX
 
-/-- The growth of a symmetric generating set in an infinite group is at least linear. -/
-lemma fact_3_1_1 [Infinite G] (hXsymm : X⁻¹ = X) (hXgen : Subgroup.closure (X : Set G) = ⊤) :
-    n ≤ #(X ^ n) := sorry
+/-- The growth of a generating set in an infinite group is at least linear. -/
+lemma fact_3_1_1 [Infinite G] (hXgen : Subgroup.closure (X : Set G) = ⊤) : n ≤ #(X ^ n) :=
+  (card_pow_strictMono (by simp [hXgen, Set.infinite_univ])).le_apply
 
 /-- The growth of a set is at most exponential. -/
 lemma fact_3_1_2 : #(X ^ n) ≤ #X ^ n := card_pow_le

LeanCamCombi/Mathlib/Order/SuccPred/Relation.lean

@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3",
+   "rev": "9ac12945862fa39eab7795c2f79bb9aa0c8e332c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3fc88df14c066088e5e4414114cd3d69a4de8bb2",
+   "rev": "5b9d3428db8ad17a2529d98bfc183fbe432e9798",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,