bump to nightly-2024-01-29-06

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/CategoryTheory/Bicategory/Basic.lean

@@ -234,11 +234,11 @@ attribute [instance] hom_category
 
 variable {B : Type u} [Bicategory.{w, v} B] {a b c d e : B}
 
-#print CategoryTheory.Bicategory.hom_inv_whiskerLeft /-
+#print CategoryTheory.Bicategory.whiskerLeft_hom_inv /-
 @[simp, reassoc]
-theorem hom_inv_whiskerLeft (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) :
+theorem whiskerLeft_hom_inv (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) :
     f ◁ η.Hom ≫ f ◁ η.inv = 𝟙 (f ≫ g) := by rw [← whisker_left_comp, hom_inv_id, whisker_left_id]
-#align category_theory.bicategory.hom_inv_whisker_left CategoryTheory.Bicategory.hom_inv_whiskerLeft
+#align category_theory.bicategory.hom_inv_whisker_left CategoryTheory.Bicategory.whiskerLeft_hom_inv
 -/
 
 #print CategoryTheory.Bicategory.hom_inv_whiskerRight /-
@@ -248,11 +248,11 @@ theorem hom_inv_whiskerRight {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) :
 #align category_theory.bicategory.hom_inv_whisker_right CategoryTheory.Bicategory.hom_inv_whiskerRight
 -/
 
-#print CategoryTheory.Bicategory.inv_hom_whiskerLeft /-
+#print CategoryTheory.Bicategory.whiskerLeft_inv_hom /-
 @[simp, reassoc]
-theorem inv_hom_whiskerLeft (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) :
+theorem whiskerLeft_inv_hom (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) :
     f ◁ η.inv ≫ f ◁ η.Hom = 𝟙 (f ≫ h) := by rw [← whisker_left_comp, inv_hom_id, whisker_left_id]
-#align category_theory.bicategory.inv_hom_whisker_left CategoryTheory.Bicategory.inv_hom_whiskerLeft
+#align category_theory.bicategory.inv_hom_whisker_left CategoryTheory.Bicategory.whiskerLeft_inv_hom
 -/
 
 #print CategoryTheory.Bicategory.inv_hom_whiskerRight /-

Mathbin/GroupTheory/Coset.lean

@@ -893,7 +893,7 @@ theorem card_eq_card_quotient_mul_card_subgroup [Fintype α] (s : Subgroup α) [
     [DecidablePred fun a => a ∈ s] : Fintype.card α = Fintype.card (α ⧸ s) * Fintype.card s := by
   rw [← Fintype.card_prod] <;> exact Fintype.card_congr Subgroup.groupEquivQuotientProdSubgroup
 #align subgroup.card_eq_card_quotient_mul_card_subgroup Subgroup.card_eq_card_quotient_mul_card_subgroup
-#align add_subgroup.card_eq_card_quotient_add_card_add_subgroup AddSubgroup.card_eq_card_quotient_add_card_addSubgroup
+#align add_subgroup.card_eq_card_quotient_add_card_add_subgroup AddSubgroup.card_eq_card_quotient_mul_card_addSubgroup
 -/
 
 #print Subgroup.card_subgroup_dvd_card /-

Mathbin/Probability/Kernel/CondCdf.lean

@@ -75,14 +75,14 @@ end Directed
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-#print prod_iInter /-
+#print Set.prod_iInter /-
 -- todo: move to data/set/lattice next to prod_Union or prod_sInter
-theorem prod_iInter {s : Set α} {t : ι → Set β} [hι : Nonempty ι] :
+theorem Set.prod_iInter {s : Set α} {t : ι → Set β} [hι : Nonempty ι] :
     (s ×ˢ ⋂ i, t i) = ⋂ i, s ×ˢ t i := by
   ext x
   simp only [mem_prod, mem_Inter]
   exact ⟨fun h i => ⟨h.1, h.2 i⟩, fun h => ⟨(h hι.some).1, fun i => (h i).2⟩⟩
-#align prod_Inter prod_iInter
+#align prod_Inter Set.prod_iInter
 -/
 
 #print Real.iUnion_Iic_rat /-
@@ -277,7 +277,7 @@ theorem iInf_IicSnd_gt (t : ℚ) {s : Set α} (hs : MeasurableSet s) [IsFiniteMe
   by
   simp_rw [ρ.Iic_snd_apply _ hs]
   rw [← measure_Inter_eq_infi]
-  · rw [← prod_iInter]
+  · rw [← Set.prod_iInter]
     congr with x : 1
     simp only [mem_Inter, mem_Iic, Subtype.forall, Subtype.coe_mk]
     refine' ⟨fun h => _, fun h a hta => h.trans _⟩
@@ -319,7 +319,7 @@ theorem tendsto_IicSnd_atBot [IsFiniteMeasure ρ] {s : Set α} (hs : MeasurableS
   by
   simp_rw [ρ.Iic_snd_apply _ hs]
   have h_empty : ρ (s ×ˢ ∅) = 0 := by simp only [prod_empty, measure_empty]
-  rw [← h_empty, ← Real.iInter_Iic_rat, prod_iInter]
+  rw [← h_empty, ← Real.iInter_Iic_rat, Set.prod_iInter]
   suffices h_neg :
     tendsto (fun r : ℚ => ρ (s ×ˢ Iic ↑(-r))) at_top (𝓝 (ρ (⋂ r : ℚ, s ×ˢ Iic ↑(-r))))
   · have h_inter_eq : (⋂ r : ℚ, s ×ˢ Iic ↑(-r)) = ⋂ r : ℚ, s ×ˢ Iic (r : ℝ) :=
@@ -619,7 +619,8 @@ theorem tendsto_preCDF_atBot_zero (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ
     rw [h_lintegral_eq]
     have h_zero_eq_measure_Inter : (0 : ℝ≥0∞) = ρ (⋂ r : ℚ, univ ×ˢ Iic (-r)) :=
       by
-      suffices (⋂ r : ℚ, Iic (-(r : ℝ))) = ∅ by rwa [← prod_iInter, this, prod_empty, measure_empty]
+      suffices (⋂ r : ℚ, Iic (-(r : ℝ))) = ∅ by
+        rwa [← Set.prod_iInter, this, prod_empty, measure_empty]
       ext1 x
       simp only [mem_Inter, mem_Iic, mem_empty_iff_false, iff_false_iff, Classical.not_forall,
         not_le]
@@ -1136,7 +1137,7 @@ theorem set_lintegral_condCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] (x
     exact_mod_cast hij
   simp_rw [h_coe, set_lintegral_cond_cdf_rat ρ _ hs]
   rw [← measure_Inter_eq_infi]
-  · rw [← prod_iInter]
+  · rw [← Set.prod_iInter]
     congr with y
     simp only [mem_Inter, mem_Iic, Subtype.forall, Subtype.coe_mk]
     exact ⟨le_of_forall_lt_rat_imp_le, fun hyx q hq => hyx.trans hq.le⟩

lake-manifest.json

@@ -58,19 +58,19 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "62acecee993214f545acf44c171ee0e2a2fe4051",
+   "rev": "d5277c9a3e68ca82db40387dd778b68d314c8cc0",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "62acecee993214f545acf44c171ee0e2a2fe4051",
+   "inputRev": "d5277c9a3e68ca82db40387dd778b68d314c8cc0",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean3port.git",
    "type": "git",
    "subDir": null,
-   "rev": "3b890e7719e32224564d4af64c69d2e725b421fb",
+   "rev": "6f3f9bf03a1daaaa34f24d7ecc526d53d8f7285d",
    "name": "lean3port",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "3b890e7719e32224564d4af64c69d2e725b421fb",
+   "inputRev": "6f3f9bf03a1daaaa34f24d7ecc526d53d8f7285d",
    "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-2024-01-28-06"
+def tag : String := "nightly-2024-01-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"@"3b890e7719e32224564d4af64c69d2e725b421fb"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"6f3f9bf03a1daaaa34f24d7ecc526d53d8f7285d"
 
 @[default_target]
 lean_lib Mathbin where