Merge remote-tracking branch 'origin/master' into bump/v4.22.0

Author: mathlib4-bot

.github/workflows/PR_summary.yml

@@ -110,23 +110,32 @@ jobs:
       run: |
         cd pr-branch
         touch moved_without_deprecation.txt
+        touch extraneous_deprecated_module.txt
         git checkout ${{ github.base_ref }}
         while IFS= read -r file
         do
           if grep ^deprecated_module "${file}" ; then
-            printf 'info: removed file %s contains a deprecation\n' "${file}"
+            # shellcheck disable=SC2016
+            printf '\n⚠️ **warning**: removed file `%s` contains a module deprecation: please add this in a follow-up PR instead\n' "${file}" |
+              tee -a extraneous_deprecated_module.txt
           else
             # shellcheck disable=SC2016
-            printf '\n⚠️ **warning**: file `%s` was removed without a module deprecation\n' "${file}" |
+            printf '\nnote: file `%s` was removed.\nPlease create a follow-up pull request adding a module deprecation. Thanks!\n' "${file}" |
               tee -a moved_without_deprecation.txt
           fi
         done < removed_files.txt
         IFS=$'\n'
         while IFS= read -r file
         do
-          # shellcheck disable=SC2016
-          printf '\n⚠️ **warning**: file %s without a module deprecation\n' "${file}" |
-            tee -a moved_without_deprecation.txt
+          if grep ^deprecated_module "${file}" ; then
+            # shellcheck disable=SC2016
+            printf '\n⚠️ **warning**: renamed file `%s` contains a module deprecation: please add this in a follow-up PR instead\n' "${file}" |
+              tee -a extraneous_deprecated_module.txt
+          else
+            # shellcheck disable=SC2016
+            printf '\nnote: file `%s` without a module deprecation\nPlease create a follow-up pull request adding one. Thanks!\n' "${file}" |
+              tee -a moved_without_deprecation.txt
+          fi
         done < renamed_files.txt
 
         # we return to the PR branch, since the next step wants it!
@@ -209,12 +218,18 @@ jobs:
         # store in a file, to avoid "long arguments" error.
         printf '%s [%s](%s)%s\n\n%s\n\n---\n\n%s\n\n---\n\n%s\n' "${title}" "$(git rev-parse --short HEAD)" "${hashURL}" "${high_percentages}" "${importCount}" "${declDiff}" "${techDebtVar}" > please_merge_master.md
 
-        echo "Include any errors about removed or renamed files without deprecation."
+        echo "Include any errors about removed or renamed files without deprecation,"
+        echo "as well as errors about extraneous deprecated_module additions."
         if [ -s moved_without_deprecation.txt ]
         then
           printf '\n\n---\n\n' >> please_merge_master.md
           cat moved_without_deprecation.txt >> please_merge_master.md
         fi
+        if [ -s extraneous_deprecated_module.txt ]
+        then
+          printf '\n\n---\n\n' >> please_merge_master.md
+          cat extraneous_deprecated_module.txt >> please_merge_master.md
+        fi
 
         cat please_merge_master.md
         ../master-branch/scripts/update_PR_comment.sh please_merge_master.md "${title}" "${PR}"

Archive/Imo/Imo1982Q1.lean

@@ -72,15 +72,15 @@ lemma superadditive {m n : ℕ+} : f m + f n ≤ f (m + n) := by
   have h := hf.rel m n
   rcases h with ( hl | hr )
   · rw [hl]
-  · rw [hr]; nth_rewrite 1 [← add_zero (f n), ← add_assoc]; apply add_le_add_right (by norm_num)
+  · rw [hr]; nth_rewrite 1 [← add_zero (f n), ← add_assoc]; gcongr; norm_num
 
 lemma superhomogeneous {m n : ℕ+} : ↑n * f m ≤ f (n * m) := by
   induction n with
   | one => simp
   | succ n' ih =>
     calc
     ↑(n' + 1) * f m = ↑n' * f m + f m := by rw [PNat.add_coe, add_mul, PNat.val_ofNat, one_mul]
-    _ ≤ f (n' * m) + f m := add_le_add_right ih (f m)
+    _ ≤ f (n' * m) + f m := by gcongr
     _ ≤ f (n' * m + m) := hf.superadditive
     _ = f ((n' + 1) * m) := by congr; rw [add_mul, one_mul]
 

Archive/Wiedijk100Theorems/CubingACube.lean

@@ -269,7 +269,7 @@ theorem w_lt_w (hi : i ∈ bcubes cs c) : (cs i).w < c.w := by
   apply lt_of_le_of_ne _ (v.2.2 i hi.1)
   have j : Fin n := ⟨1, Nat.le_of_succ_le_succ h.three_le⟩
   rw [← add_le_add_iff_left ((cs i).b j.succ)]
-  apply le_trans (t_le_t hi j); rw [add_le_add_iff_right]; apply b_le_b hi
+  apply le_trans (t_le_t hi j); gcongr; apply b_le_b hi
 
 /-- There are at least two cubes in a valley -/
 theorem nontrivial_bcubes : (bcubes cs c).Nontrivial := by
@@ -292,8 +292,9 @@ theorem nontrivial_bcubes : (bcubes cs c).Nontrivial := by
   rintro rfl
   apply not_le_of_gt (hi'.2 ⟨1, Nat.le_of_succ_le_succ h.three_le⟩).2
   simp only [tail, Cube.tail, p]
-  rw [if_pos, add_le_add_iff_right]
-  · exact (hi.2 _).1
+  rw [if_pos]
+  · gcongr
+    exact (hi.2 _).1
   rfl
 
 /-- There is a cube in the valley -/
@@ -367,7 +368,7 @@ theorem smallest_onBoundary {j} (bi : OnBoundary (mi_mem_bcubes : mi h v ∈ _)
   · simp only [side, not_and_or, not_lt, not_le, mem_Ico]; left; exact hx
   intro i'' hi'' h2i'' h3i''; constructor; swap; · apply lt_trans hx h3i''.2
   rw [le_sub_iff_add_le]
-  refine le_trans ?_ (t_le_t hi'' j); rw [add_le_add_iff_left]; apply h3i' i'' ⟨hi'', _⟩
+  refine le_trans ?_ (t_le_t hi'' j); gcongr; apply h3i' i'' ⟨hi'', _⟩
   simp [i, mem_singleton, h2i'']
 
 variable (h v)

Mathlib.lean

@@ -753,6 +753,7 @@ import Mathlib.Algebra.Order.Antidiag.Nat
 import Mathlib.Algebra.Order.Antidiag.Pi
 import Mathlib.Algebra.Order.Antidiag.Prod
 import Mathlib.Algebra.Order.Archimedean.Basic
+import Mathlib.Algebra.Order.Archimedean.Class
 import Mathlib.Algebra.Order.Archimedean.Hom
 import Mathlib.Algebra.Order.Archimedean.IndicatorCard
 import Mathlib.Algebra.Order.Archimedean.Submonoid
@@ -827,6 +828,7 @@ import Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
 import Mathlib.Algebra.Order.GroupWithZero.Bounds
 import Mathlib.Algebra.Order.GroupWithZero.Canonical
 import Mathlib.Algebra.Order.GroupWithZero.Finset
+import Mathlib.Algebra.Order.GroupWithZero.Lex
 import Mathlib.Algebra.Order.GroupWithZero.Submonoid
 import Mathlib.Algebra.Order.GroupWithZero.Synonym
 import Mathlib.Algebra.Order.GroupWithZero.Unbundled
@@ -860,6 +862,7 @@ import Mathlib.Algebra.Order.Monoid.Basic
 import Mathlib.Algebra.Order.Monoid.Canonical.Basic
 import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Order.Monoid.Defs
+import Mathlib.Algebra.Order.Monoid.Lex
 import Mathlib.Algebra.Order.Monoid.NatCast
 import Mathlib.Algebra.Order.Monoid.OrderDual
 import Mathlib.Algebra.Order.Monoid.Prod
@@ -3802,6 +3805,7 @@ import Mathlib.GroupTheory.QuotientGroup.Basic
 import Mathlib.GroupTheory.QuotientGroup.Defs
 import Mathlib.GroupTheory.QuotientGroup.Finite
 import Mathlib.GroupTheory.Rank
+import Mathlib.GroupTheory.RegularWreathProduct
 import Mathlib.GroupTheory.Schreier
 import Mathlib.GroupTheory.SchurZassenhaus
 import Mathlib.GroupTheory.SemidirectProduct
@@ -4885,6 +4889,7 @@ import Mathlib.Order.Preorder.Chain
 import Mathlib.Order.Preorder.Finite
 import Mathlib.Order.PrimeIdeal
 import Mathlib.Order.PrimeSeparator
+import Mathlib.Order.Prod.Lex.Hom
 import Mathlib.Order.PropInstances
 import Mathlib.Order.Radical
 import Mathlib.Order.Rel.GaloisConnection
@@ -5027,11 +5032,13 @@ import Mathlib.RepresentationTheory.Character
 import Mathlib.RepresentationTheory.Coinduced
 import Mathlib.RepresentationTheory.Coinvariants
 import Mathlib.RepresentationTheory.FDRep
-import Mathlib.RepresentationTheory.GroupCohomology.Basic
-import Mathlib.RepresentationTheory.GroupCohomology.Functoriality
-import Mathlib.RepresentationTheory.GroupCohomology.Hilbert90
-import Mathlib.RepresentationTheory.GroupCohomology.LowDegree
-import Mathlib.RepresentationTheory.GroupCohomology.Resolution
+import Mathlib.RepresentationTheory.FiniteIndex
+import Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
+import Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
+import Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
+import Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
+import Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
+import Mathlib.RepresentationTheory.Homological.Resolution
 import Mathlib.RepresentationTheory.Induced
 import Mathlib.RepresentationTheory.Invariants
 import Mathlib.RepresentationTheory.Maschke

Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean

@@ -134,7 +134,7 @@ theorem tensorObj_comul (K L : CoalgCat R) :
   rfl
 
 theorem tensorHom_toLinearMap (f : M →ₗc[R] N) (g : P →ₗc[R] Q) :
-    (CoalgCat.ofHom f ⊗ CoalgCat.ofHom g).1.toLinearMap
+    (CoalgCat.ofHom f ⊗ₘ CoalgCat.ofHom g).1.toLinearMap
       = TensorProduct.map f.toLinearMap g.toLinearMap := rfl
 
 theorem associator_hom_toLinearMap :

Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

@@ -175,7 +175,7 @@ namespace MonoidalCategory
 
 @[simp]
 theorem tensorHom_tmul {K L M N : ModuleCat.{u} R} (f : K ⟶ L) (g : M ⟶ N) (k : K) (m : M) :
-    (f ⊗ g) (k ⊗ₜ m) = f k ⊗ₜ g m :=
+    (f ⊗ₘ g) (k ⊗ₜ m) = f k ⊗ₜ g m :=
   rfl
 
 @[simp]

Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean

@@ -28,7 +28,7 @@ namespace MonoidalCategory
 
 @[simp]
 theorem braiding_naturality {X₁ X₂ Y₁ Y₂ : ModuleCat.{u} R} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
-    (f ⊗ g) ≫ (Y₁.braiding Y₂).hom = (X₁.braiding X₂).hom ≫ (g ⊗ f) := by
+    (f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom = (X₁.braiding X₂).hom ≫ (g ⊗ₘ f) := by
   ext : 1
   apply TensorProduct.ext'
   intro x y

Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean

@@ -72,7 +72,7 @@ lemma tensorObj_map_tmul {X Y : Cᵒᵖ} (f : X ⟶ Y) (m₁ : M₁.obj X) (m₂
 /-- The tensor product of two morphisms of presheaves of modules. -/
 @[simps]
 noncomputable def tensorHom (f : M₁ ⟶ M₂) (g : M₃ ⟶ M₄) : tensorObj M₁ M₃ ⟶ tensorObj M₂ M₄ where
-  app X := f.app X ⊗ g.app X
+  app X := f.app X ⊗ₘ g.app X
   naturality {X Y} φ := ModuleCat.MonoidalCategory.tensor_ext (fun m₁ m₃ ↦ by
     dsimp
     rw [tensorObj_map_tmul]

Mathlib/Algebra/DirectSum/Internal.lean

@@ -468,7 +468,7 @@ variable [CanonicallyOrderedAdd ι]
 /-- The difference with `DirectSum.listProd_apply_eq_zero` is that the indices at which
 the terms of the list are zero is allowed to vary. -/
 theorem listProd_apply_eq_zero' {l : List ((⨁ i, A i) × ι)}
-    (hl : ∀ xn ∈ l, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄ (hn : n < (l.map Prod.snd).sum)  :
+    (hl : ∀ xn ∈ l, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄ (hn : n < (l.map Prod.snd).sum) :
     (l.map Prod.fst).prod n = 0 := by
   induction l generalizing n with
   | nil => simp [(zero_le n).not_gt] at hn
@@ -500,7 +500,7 @@ variable {A : ι → σ} [SetLike.GradedMonoid A]
 /-- The difference with `DirectSum.multisetProd_apply_eq_zero` is that the indices at which
 the terms of the multiset are zero is allowed to vary. -/
 theorem multisetProd_apply_eq_zero' {s : Multiset ((⨁ i, A i) × ι)}
-    (hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄ (hn : n < (s.map Prod.snd).sum)  :
+    (hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄ (hn : n < (s.map Prod.snd).sum) :
     (s.map Prod.fst).prod n = 0 := by
   have := listProd_apply_eq_zero' (l := s.toList) (by simpa using hs)
     (by simpa [← Multiset.sum_coe, ← Multiset.map_coe])
@@ -516,7 +516,7 @@ theorem multisetProd_apply_eq_zero {s : Multiset (⨁ i, A i)} {m : ι}
 /-- The difference with `DirectSum.finsetProd_apply_eq_zero` is that the indices at which
 the terms of the multiset are zero is allowed to vary. -/
 theorem finsetProd_apply_eq_zero' {s : Finset ((⨁ i, A i) × ι)}
-    (hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄ (hn : n < ∑ xn ∈ s, xn.2)  :
+    (hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄ (hn : n < ∑ xn ∈ s, xn.2) :
     (∏ xn ∈ s, xn.1) n = 0 := by
   simpa using listProd_apply_eq_zero' (l := s.toList) (by simpa using hs) (by simpa)
 

Mathlib/Algebra/Group/End.lean

@@ -179,6 +179,14 @@ theorem self_trans_inv (e : Perm α) : e.trans e⁻¹ = 1 :=
 theorem symm_mul (e : Perm α) : e.symm * e = 1 :=
   Equiv.self_trans_symm e
 
+/-- If `α` is equivalent to `β`, then `Perm α` is isomorphic to `Perm β`. -/
+def permCongrHom (e : α ≃ β) : Equiv.Perm α ≃* Equiv.Perm β where
+  toFun x := e.symm.trans (x.trans e)
+  invFun y := e.trans (y.trans e.symm)
+  left_inv _ := by ext; simp
+  right_inv _ := by ext; simp
+  map_mul' _ _ := by ext; simp
+
 /-! Lemmas about `Equiv.Perm.sumCongr` re-expressed via the group structure. -/