bump to nightly-2023-12-29-06

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Algebra/BigOperators/Basic.lean

@@ -613,12 +613,12 @@ theorem prod_bij' {s : Finset α} {t : Finset γ} {f : α → β} {g : γ → β
 #align finset.sum_bij' Finset.sum_bij'
 -/
 
-#print Finset.Equiv.prod_comp_finset /-
+#print Finset.prod_equiv /-
 /-- Reindexing a product over a finset along an equivalence.
 See `equiv.prod_comp` for the version where `s` and `s'` are `univ`. -/
 @[to_additive
       " Reindexing a sum over a finset along an equivalence.\nSee `equiv.sum_comp` for the version where `s` and `s'` are `univ`. "]
-theorem Equiv.prod_comp_finset {ι'} [DecidableEq ι] (e : ι ≃ ι') (f : ι' → β) {s' : Finset ι'}
+theorem Finset.prod_equiv {ι'} [DecidableEq ι] (e : ι ≃ ι') (f : ι' → β) {s' : Finset ι'}
     {s : Finset ι} (h : s = s'.image e.symm) : ∏ i' in s', f i' = ∏ i in s, f (e i) :=
   by
   rw [h]
@@ -628,8 +628,8 @@ theorem Equiv.prod_comp_finset {ι'} [DecidableEq ι] (e : ι ≃ ι') (f : ι'
       (fun a ha => e.apply_symm_apply a) fun a ha => e.symm_apply_apply a
   rcases finset.mem_image.mp ha with ⟨i', hi', rfl⟩
   rwa [e.apply_symm_apply]
-#align finset.equiv.prod_comp_finset Finset.Equiv.prod_comp_finset
-#align finset.equiv.sum_comp_finset Finset.Equiv.sum_comp_finset
+#align finset.equiv.prod_comp_finset Finset.prod_equiv
+#align finset.equiv.sum_comp_finset Finset.sum_equiv
 -/
 
 #print Finset.prod_finset_product /-

Mathbin/Data/Finset/Pointwise.lean

@@ -681,12 +681,12 @@ theorem div_def : s / t = (s ×ˢ t).image fun p : α × α => p.1 / p.2 :=
 -/
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-#print Finset.image_div_prod /-
+#print Finset.image_div_product /-
 @[to_additive add_image_prod]
-theorem image_div_prod : ((s ×ˢ t).image fun x : α × α => x.fst / x.snd) = s / t :=
+theorem image_div_product : ((s ×ˢ t).image fun x : α × α => x.fst / x.snd) = s / t :=
   rfl
-#align finset.image_div_prod Finset.image_div_prod
-#align finset.add_image_prod Finset.add_image_prod
+#align finset.image_div_prod Finset.image_div_product
+#align finset.add_image_prod Finset.image_sub_product
 -/
 
 #print Finset.mem_div /-

Mathbin/GroupTheory/Perm/Sign.lean

@@ -380,8 +380,8 @@ def signBijAux {n : ℕ} (f : Perm (Fin n)) (a : Σ a : Fin n, Fin n) : Σ a : F
 #align equiv.perm.sign_bij_aux Equiv.Perm.signBijAux
 -/
 
-#print Equiv.Perm.signBijAux_inj /-
-theorem signBijAux_inj {n : ℕ} {f : Perm (Fin n)} :
+#print Equiv.Perm.signBijAux_injOn /-
+theorem signBijAux_injOn {n : ℕ} {f : Perm (Fin n)} :
     ∀ a b : Σ a : Fin n, Fin n,
       a ∈ finPairsLT n → b ∈ finPairsLT n → signBijAux f a = signBijAux f b → a = b :=
   fun ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ha hb h => by
@@ -390,7 +390,7 @@ theorem signBijAux_inj {n : ℕ} {f : Perm (Fin n)} :
   have : ¬b₁ < b₂ := hb.le.not_lt
   split_ifs at h  <;>
     simp_all only [(Equiv.injective f).eq_iff, eq_self_iff_true, and_self_iff, heq_iff_eq]
-#align equiv.perm.sign_bij_aux_inj Equiv.Perm.signBijAux_inj
+#align equiv.perm.sign_bij_aux_inj Equiv.Perm.signBijAux_injOn
 -/
 
 #print Equiv.Perm.signBijAux_surj /-
@@ -437,7 +437,7 @@ theorem signAux_inv {n : ℕ} (f : Perm (Fin n)) : signAux f⁻¹ = signAux f :=
       else by
         rw [sign_bij_aux, if_pos (le_of_not_gt h), dif_neg h, apply_inv_self, apply_inv_self,
           if_pos (mem_fin_pairs_lt.1 hab).le])
-    signBijAux_inj signBijAux_surj
+    signBijAux_injOn signBijAux_surj
 #align equiv.perm.sign_aux_inv Equiv.Perm.signAux_inv
 -/
 

lake-manifest.json

@@ -49,19 +49,19 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "d2d0dcdfe131b20dbd6a80e7ac6c8da622614b63",
+   "rev": "8788d9a43952b75c0e9a0640f273629f73b3b2b4",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "d2d0dcdfe131b20dbd6a80e7ac6c8da622614b63",
+   "inputRev": "8788d9a43952b75c0e9a0640f273629f73b3b2b4",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean3port.git",
    "type": "git",
    "subDir": null,
-   "rev": "a9193ccdb0bfc992f332e532eef8f097bbfbdcd6",
+   "rev": "2938d8a2dc684fa15688f5dc5d408ec06f504315",
    "name": "lean3port",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "a9193ccdb0bfc992f332e532eef8f097bbfbdcd6",
+   "inputRev": "2938d8a2dc684fa15688f5dc5d408ec06f504315",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "mathlib3port",

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-12-28-06"
+def tag : String := "nightly-2023-12-29-06"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"a9193ccdb0bfc992f332e532eef8f097bbfbdcd6"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"2938d8a2dc684fa15688f5dc5d408ec06f504315"
 
 @[default_target]
 lean_lib Mathbin where