Bump mathlib

Author: YaelDillies

LeanCamCombi.lean

@@ -41,7 +41,6 @@ import LeanCamCombi.Mathlib.Algebra.Group.Subgroup.Pointwise
 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.Degree.Operations
 import LeanCamCombi.Mathlib.Algebra.Polynomial.Div
 import LeanCamCombi.Mathlib.Algebra.Polynomial.Eval.Degree
 import LeanCamCombi.Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
@@ -64,7 +63,6 @@ import LeanCamCombi.Mathlib.Data.Finset.PosDiffs
 import LeanCamCombi.Mathlib.Data.List.DropRight
 import LeanCamCombi.Mathlib.Data.Multiset.Basic
 import LeanCamCombi.Mathlib.Data.Prod.Lex
-import LeanCamCombi.Mathlib.Data.Set.Basic
 import LeanCamCombi.Mathlib.Data.Set.Card
 import LeanCamCombi.Mathlib.Data.Set.Image
 import LeanCamCombi.Mathlib.Data.Set.Lattice

LeanCamCombi/Archive/CauchyDavenportFromKneser.lean

@@ -20,7 +20,7 @@ This file proves the Cauchy-Davenport theorem as a corollary of Kneser's lemma.
 additive combinatorics, number theory, sumset, cauchy-davenport
 -/
 
-open Finset
+open AddAction Finset
 open scoped Pointwise
 
 /-- The **Cauchy-Davenport Theorem**. -/
@@ -29,8 +29,9 @@ 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 [← coe_set_eq_zero, ← coe_addStab (hs.add ht), coe_eq_zero] at h
+    rw [← coe_set_eq_zero, ← stabilizer_coe_finset, ← 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
+  · rw [← AddSubgroup.coe_eq_univ, ← stabilizer_coe_finset, ← coe_addStab (hs.add ht), coe_eq_univ]
+      at h
     refine card_addStab_le_card.trans' ?_
     simp [*, card_univ]

LeanCamCombi/GrowthInGroups/ApproximateSubgroup.lean

@@ -4,7 +4,6 @@ import Mathlib.Tactic.Bound
 import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Basic
 import LeanCamCombi.Mathlib.Algebra.Group.Subgroup.Pointwise
 import LeanCamCombi.Mathlib.Combinatorics.Additive.RuzsaCovering
-import LeanCamCombi.Mathlib.Data.Set.Basic
 import LeanCamCombi.Mathlib.Data.Set.Lattice
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.GrowthInGroups.SMulCover

LeanCamCombi/GrowthInGroups/CardQuotient.lean

@@ -1,7 +1,6 @@
 import Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import Mathlib.Combinatorics.Enumerative.DoubleCounting
 import Mathlib.GroupTheory.QuotientGroup.Defs
-import LeanCamCombi.Mathlib.GroupTheory.Coset.Defs
 
 open Finset Function
 open scoped Pointwise

LeanCamCombi/Kneser/Kneser.lean

@@ -298,12 +298,12 @@ theorem mul_kneser :
   -- We distinguish whether `s * t` has trivial stabilizer.
   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 (↑) :=
-      image_mul (QuotientGroup.mk' _ : α →* α ⧸ stabilizer α (s * t))
+      ((s * t).image (↑) : Finset (α ⧸ stabilizer α (s * t).toSet)) = s.image (↑) * t.image (↑) :=
+      image_mul (QuotientGroup.mk' _ : α →* α ⧸ stabilizer α (s * t).toSet)
     suffices hineq :
       #(s * t).mulStab *
-          (#(s.image (↑) : Finset (α ⧸ stabilizer α (s * t))) +
-              #(t.image (↑) : Finset (α ⧸ stabilizer α (s * t))) -  1) ≤
+          (#(s.image (↑) : Finset (α ⧸ stabilizer α (s * t).toSet)) +
+              #(t.image (↑) : Finset (α ⧸ stabilizer α (s * t).toSet)) -  1) ≤
         #(s * t) by
     -- now to prove that `#(s * (s * t).mulStab) = #(s * t).mulStab * #(s.image (↑))` and
     -- the analogous statement for `s` and `t` interchanged
@@ -313,9 +313,10 @@ theorem mul_kneser :
       convert hineq using 1
       exact add_comm _ _
     refine le_of_le_of_eq (mul_le_mul_left' ?_ _) (card_mul_card_eq_mulStab_card_mul_coe s t).symm
-    have := ih _ ?_ (s.image (↑) : Finset (α ⧸ stabilizer α (s * t))) (t.image (↑)) rfl
-    simpa only [← image_coe_mul, mulStab_image_coe_quotient (hs.mul ht), mul_one,
-      tsub_le_iff_right, card_one] using this
+    have := ih _ ?_ (s.image (↑) : Finset (α ⧸ stabilizer α (s * t).toSet)) (t.image (↑)) rfl
+    · classical
+      simpa only [← image_coe_mul, mulStab_image_coe_quotient (hs.mul ht), mul_one,
+        tsub_le_iff_right, card_one] using this
     rw [← image_coe_mul, card_mul_card_eq_mulStab_card_mul_coe]
     exact
       add_lt_add_of_lt_of_le

LeanCamCombi/Kneser/MulStab.lean

@@ -30,6 +30,10 @@ local notation s " +ˢ " N => Set.image ((↑) : α → α ⧸ N) s
 section Group
 variable [Group α] [DecidableEq α] {s t : Finset α} {a : α}
 
+@[to_additive]
+instance (s : Finset α) : DecidablePred (· ∈ stabilizer α s.toSet) :=
+  fun a ↦ decidable_of_iff (a ∈ stabilizer α s) (by simp)
+
 /-- The stabilizer of `s` as a finset. As an exception, this sends `∅` to `∅`.-/
 @[to_additive "The stabilizer of `s` as a finset. As an exception, this sends `∅` to `∅`."]
 def mulStab (s : Finset α) : Finset α := {a ∈ s / s | a • s = s}
@@ -51,20 +55,22 @@ lemma mulStab_subset_div_right (ha : a ∈ s) : s.mulStab ⊆ s / {a} := by
   exact smul_mem_smul_finset ha
 
 @[to_additive (attr := simp)]
-lemma coe_mulStab (hs : s.Nonempty) : (s.mulStab : Set α) = MulAction.stabilizer α s := by
+lemma coe_mulStab (hs : s.Nonempty) : (s.mulStab : Set α) = stabilizer α s.toSet := by
   ext; simp [mem_mulStab hs]
 
 @[to_additive]
 lemma mem_mulStab_iff_subset_smul_finset (hs : s.Nonempty) : a ∈ s.mulStab ↔ s ⊆ a • s := by
-  rw [← mem_coe, coe_mulStab hs, SetLike.mem_coe, mem_stabilizer_finset_iff_subset_smul_finset]
+  rw [← mem_coe, coe_mulStab hs, SetLike.mem_coe, stabilizer_coe_finset,
+    mem_stabilizer_finset_iff_subset_smul_finset]
 
 @[to_additive]
 lemma mem_mulStab_iff_smul_finset_subset (hs : s.Nonempty) : a ∈ s.mulStab ↔ a • s ⊆ s := by
-  rw [← mem_coe, coe_mulStab hs, SetLike.mem_coe, mem_stabilizer_finset_iff_smul_finset_subset]
+  rw [← mem_coe, coe_mulStab hs, SetLike.mem_coe, stabilizer_coe_finset,
+    mem_stabilizer_finset_iff_smul_finset_subset]
 
 @[to_additive]
 lemma mem_mulStab' (hs : s.Nonempty) : a ∈ s.mulStab ↔ ∀ ⦃b⦄, b ∈ s → a • b ∈ s := by
-  rw [← mem_coe, coe_mulStab hs, SetLike.mem_coe, mem_stabilizer_finset']
+  rw [← mem_coe, coe_mulStab hs, SetLike.mem_coe, stabilizer_coe_finset, mem_stabilizer_finset']
 
 @[to_additive (attr := simp)]
 lemma mulStab_empty : mulStab (∅ : Finset α) = ∅ := by simp [mulStab]
@@ -188,31 +194,30 @@ lemma mul_subset_left : t ⊆ s.mulStab → s * t ⊆ s := by rw [mul_comm]; exa
 lemma mulStab_idem (s : Finset α) : s.mulStab.mulStab = s.mulStab := by
   obtain rfl | hs := s.eq_empty_or_nonempty
   · simp
-  rw [← coe_inj, coe_mulStab hs, coe_mulStab hs.mulStab, ← stabilizer_coe_finset, coe_mulStab hs]
+  rw [← coe_inj, coe_mulStab hs, coe_mulStab hs.mulStab, coe_mulStab hs]
   simp
 
 @[to_additive (attr := simp)]
 lemma mulStab_smul (a : α) (s : Finset α) : (a • s).mulStab = s.mulStab := by
   obtain rfl | hs := s.eq_empty_or_nonempty
   · simp
-  · rw [← coe_inj, coe_mulStab hs, coe_mulStab hs.smul_finset, stabilizer_smul_eq_right]
-
-open scoped Classical
+  · rw [← coe_inj, coe_mulStab hs, coe_mulStab hs.smul_finset, stabilizer_coe_finset,
+    stabilizer_coe_finset, stabilizer_smul_eq_right]
 
 @[to_additive]
 lemma mulStab_image_coe_quotient (hs : s.Nonempty) :
-    (s.image (↑) : Finset (α ⧸ stabilizer α s)).mulStab = 1 := by
-  rw [← coe_inj, coe_mulStab (hs.image _), ← stabilizer_coe_finset, ← stabilizer_coe_finset,
-    coe_image, coe_one, stabilizer_image_coe_quotient, Subgroup.coe_bot, Set.singleton_one]
+    (s.image (↑) : Finset (α ⧸ stabilizer α s.toSet)).mulStab = 1 := by
+  simp_rw [← coe_inj, coe_mulStab (hs.image _), coe_image, coe_one]
+  rw [stabilizer_image_coe_quotient, Subgroup.coe_bot, Set.singleton_one]
 
 @[to_additive]
 lemma preimage_image_quotientMk_stabilizer_eq_mul_mulStab (ht : t.Nonempty) (s : Finset α) :
-    QuotientGroup.mk ⁻¹' (s +ˢ stabilizer α t) = s * t.mulStab := by
-  rw [QuotientGroup.preimage_image_mk_eq_mul, coe_mulStab ht]
+    QuotientGroup.mk ⁻¹' (s +ˢ stabilizer α t.toSet) = s * t.mulStab := by
+  rw [QuotientGroup.preimage_image_mk_eq_mul, coe_mulStab ht, stabilizer_coe_finset]
 
 @[to_additive]
 lemma preimage_image_quotientMk_mulStabilizer (s : Finset α) :
-    QuotientGroup.mk ⁻¹' (s +ˢ stabilizer α s) = s := by
+    QuotientGroup.mk ⁻¹' (s +ˢ stabilizer α s.toSet) = s := by
   obtain rfl | hs := s.eq_empty_or_nonempty
   · simp
   · rw [preimage_image_quotientMk_stabilizer_eq_mul_mulStab hs s, ← coe_mul, mul_mulStab]
@@ -280,12 +285,12 @@ lemma card_mulStab_dvd_card_mulStab (hs : s.Nonempty) (h : s.mulStab ⊆ t.mulSt
 
 /-- A version of Lagrange's theorem. -/
 @[to_additive "A version of Lagrange's theorem."]
-lemma card_mulStab_mul_card_image_coe' (s t : Finset α) :
-    #t.mulStab * #(s +ₛ stabilizer α t) = #(s * t.mulStab) := by
+lemma card_mulStab_mul_card_image_coe' (s t : Finset α) [DecidableEq (α ⧸ stabilizer α t.toSet)] :
+    #t.mulStab * #(s +ₛ stabilizer α t.toSet) = #(s * t.mulStab) := by
   obtain rfl | ht := t.eq_empty_or_nonempty
   · simp
-  have := QuotientGroup.preimageMkEquivSubgroupProdSet _ (s +ˢ stabilizer α t)
-  have that : ↥(stabilizer α t) = ↥t.mulStab := by
+  have := QuotientGroup.preimageMkEquivSubgroupProdSet _ (s +ˢ stabilizer α t.toSet)
+  have that : ↥(stabilizer α t.toSet) = ↥t.mulStab := by
     rw [← SetLike.coe_sort_coe, ← coe_mulStab ht, Finset.coe_sort_coe]
   have temp := this.trans ((Equiv.cast that).prodCongr (Equiv.refl _))
   rw [preimage_image_quotientMk_stabilizer_eq_mul_mulStab ht] at temp
@@ -295,13 +300,13 @@ lemma card_mulStab_mul_card_image_coe' (s t : Finset α) :
 
 @[to_additive]
 lemma card_mul_card_eq_mulStab_card_mul_coe (s t : Finset α) :
-    #(s * t) = #(s * t).mulStab * #((s * t) +ₛ stabilizer α (s * t)) := by
+    #(s * t) = #(s * t).mulStab * #((s * t) +ₛ stabilizer α (s * t).toSet) := by
   obtain rfl | hs := s.eq_empty_or_nonempty
   · simp
   obtain rfl | ht := t.eq_empty_or_nonempty
   · simp
-  have := QuotientGroup.preimageMkEquivSubgroupProdSet _ $ ↑(s * t) +ˢ stabilizer α (s * t)
-  have that : ↥(stabilizer α (s * t)) = ↥(s * t).mulStab := by
+  have := QuotientGroup.preimageMkEquivSubgroupProdSet _ $ ↑(s * t) +ˢ stabilizer α (s * t).toSet
+  have that : ↥(stabilizer α (s * t).toSet) = ↥(s * t).mulStab := by
     rw [← SetLike.coe_sort_coe, ← coe_mulStab (hs.mul ht), Finset.coe_sort_coe]
   have temp := this.trans $ (Equiv.cast that).prodCongr (Equiv.refl _)
   rw [preimage_image_quotientMk_mulStabilizer] at temp
@@ -310,40 +315,42 @@ lemma card_mul_card_eq_mulStab_card_mul_coe (s t : Finset α) :
 /-- A version of Lagrange's theorem. -/
 @[to_additive "A version of Lagrange's theorem."]
 lemma card_mulStab_mul_card_image_coe (s t : Finset α) :
-    #(s * t).mulStab * #((s +ₛ stabilizer α (s * t)) * (t +ₛ stabilizer α (s * t))) = #(s * t) := by
+    #(s * t).mulStab * #((s +ₛ stabilizer α (s * t).toSet) * (t +ₛ stabilizer α (s * t).toSet)) =
+      #(s * t) := by
   obtain rfl | hs := s.eq_empty_or_nonempty
   · simp
   obtain rfl | ht := t.eq_empty_or_nonempty
   · simp
-  let this := QuotientGroup.preimageMkEquivSubgroupProdSet (stabilizer α (s * t))
-    ((s +ˢ stabilizer α (s * t)) * (t +ˢ stabilizer α (s * t)))
+  let this := QuotientGroup.preimageMkEquivSubgroupProdSet (stabilizer α (s * t).toSet)
+    ((s +ˢ stabilizer α (s * t).toSet) * (t +ˢ stabilizer α (s * t).toSet))
   have image_coe_mul :
-    ((s * t) +ˢ stabilizer α (s * t)) = (s +ˢ stabilizer α (s * t)) * (t +ˢ stabilizer α (s * t)) :=
-    Set.image_mul (QuotientGroup.mk' (stabilizer α (s * t)) : α →* α ⧸ stabilizer α (s * t))
-  rw [← image_coe_mul, ← coe_mul, preimage_image_quotientMk_mulStabilizer, coe_mul, image_coe_mul]
-    at this
+    ((s * t).toSet +ˢ stabilizer α (s * t).toSet) =
+      (s +ˢ stabilizer α (s * t).toSet) * (t +ˢ stabilizer α (s * t).toSet) := by
+    simpa [coe_mul] using Set.image_mul (QuotientGroup.mk' (stabilizer α (s * t).toSet))
+  rw [← image_coe_mul, preimage_image_quotientMk_mulStabilizer, image_coe_mul] at this
   have that :
-    (stabilizer α (s * t) × ↥((s +ˢ stabilizer α (s * t)) * (t +ˢ stabilizer α (s * t)))) =
-      ((s * t).mulStab × ↥((s +ˢ stabilizer α (s * t)) * (t +ˢ stabilizer α (s * t)))) := by
+    (stabilizer α (s * t).toSet ×
+      ↥((s +ˢ stabilizer α (s * t).toSet) * (t +ˢ stabilizer α (s * t).toSet))) =
+      ((s * t).mulStab ×
+        ↥((s +ˢ stabilizer α (s * t).toSet) * (t +ˢ stabilizer α (s * t).toSet))) := by
     rw [← SetLike.coe_sort_coe, ← coe_mulStab (hs.mul ht), Finset.coe_sort_coe]
   let temp := this.trans (Equiv.cast that)
   replace temp := Fintype.card_congr temp
-  simp_rw [← Finset.coe_mul s t] at temp
   simp only [Fintype.card_prod, Fintype.card_coe] at temp
   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
+  have h2 : (s +ˢ stabilizer α (s * t).toSet) * (t +ˢ stabilizer α (s * t).toSet) =
+    ↑((s +ₛ stabilizer α (s * t).toSet) * (t +ₛ stabilizer α (s * t).toSet)) := by simp
   have h3 :
-    Fintype.card ((s +ˢ stabilizer α (s * t)) * (t +ˢ stabilizer α (s * t))) =
-      Fintype.card ((s +ₛ stabilizer α (s * t)) * (t +ₛ stabilizer α (s * t))) := by
+    Fintype.card ((s +ˢ stabilizer α (s * t).toSet) * (t +ˢ stabilizer α (s * t).toSet)) =
+      Fintype.card ((s +ₛ stabilizer α (s * t).toSet) * (t +ₛ stabilizer α (s * t).toSet)) := 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
+lemma subgroup_mul_card_eq_mul_of_mul_stab_subset (s : Subgroup α) [DecidablePred (· ∈ s)]
+    (t : Finset α) (hst : (s : Set α) ⊆ t.mulStab) : Nat.card s * #(t +ₛ s) = #t := by
   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) _)
@@ -353,7 +360,7 @@ lemma subgroup_mul_card_eq_mul_of_mul_stab_subset (s : Subgroup α) (t : Finset
   · rw [← coe_mul, mul_mulStab]
 
 @[to_additive]
-lemma mulStab_quotient_commute_subgroup (s : Subgroup α) (t : Finset α)
+lemma mulStab_quotient_commute_subgroup (s : Subgroup α) [DecidablePred (· ∈ s)] (t : Finset α)
     (hst : (s : Set α) ⊆ t.mulStab) : (t.mulStab +ₛ s) = (t +ₛ s).mulStab := by
   obtain rfl | ht := t.eq_empty_or_nonempty
   · simp

LeanCamCombi/Mathlib/Algebra/Polynomial/Degree/Operations.lean

@@ -1,5 +1,4 @@
 import Mathlib.Algebra.Polynomial.Eval.Degree
-import LeanCamCombi.Mathlib.Algebra.Polynomial.Degree.Operations
 
 variable {R S : Type*} [CommRing R] [CommRing S]
 
@@ -15,6 +14,6 @@ lemma degree_map_lt (hp : f p.leadingCoeff = 0) (hp₀ : p ≠ 0) : (p.map f).de
 -- TODO: There is a version of this where we assume `p` nonconstant instead of `map f p ≠ 0`
 lemma natDegree_map_lt (hp : f p.leadingCoeff = 0) (hp₀ : map f p ≠ 0) :
     (p.map f).natDegree < p.natDegree :=
-  natDegree_lt_natDegree' hp₀ <| degree_map_lt hp <| by rintro rfl; simp at hp₀
+  natDegree_lt_natDegree hp₀ <| degree_map_lt hp <| by rintro rfl; simp at hp₀
 
 end Polynomial

LeanCamCombi/Mathlib/Algebra/Polynomial/Eval/Degree.lean

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a822446d61ad7e7f5e843365c7041c326553050a",
+   "rev": "0dc51ac7947ff6aa2c16bcffb64c46c7149d1276",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "840e02ce2768e06de7ced0a624444746590e9d99",
+   "rev": "2abe270b9a11bad57afac01e29a40b4e92e1fcc5",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,