bump to nightly-2023-05-09-22

mathlib commit leanprover-community/mathlib@d4437c6

Mathbin/MeasureTheory/Constructions/BorelSpace.lean

@@ -1148,7 +1148,7 @@ theorem AEMeasurable.isLUB {ι} {μ : Measure δ} [Countable ι] {f : ι → δ
     AEMeasurable g μ := by
   by_cases hμ : μ = 0
   · rw [hμ]
-    exact aEMeasurable_zero_measure
+    exact aemeasurable_zero_measure
   have : μ.ae.ne_bot := by simpa [ne_bot_iff]
   by_cases hι : Nonempty ι
   · exact ae_measurable.is_lub_of_nonempty hι hf hg
@@ -1182,7 +1182,7 @@ theorem AEMeasurable.isGLB {ι} {μ : Measure δ} [Countable ι] {f : ι → δ
   haveI hα : Nonempty α := inferInstance
   cases' isEmpty_or_nonempty ι with hι hι
   · simp only [IsEmpty.exists_iff, set_of_false, isGLB_empty_iff] at hg
-    exact aEMeasurable_const' (hg.mono fun a ha => hg.mono fun b hb => (hb _).antisymm (ha _))
+    exact aemeasurable_const' (hg.mono fun a ha => hg.mono fun b hb => (hb _).antisymm (ha _))
   let p : δ → (ι → α) → Prop := fun x f' => IsGLB { a | ∃ i, f' i = a } (g x)
   let g_seq := (aeSeqSet hf p).piecewise g fun _ => hα.some
   have hg_seq : ∀ b, IsGLB { a | ∃ i, aeSeq hf p i b = a } (g_seq b) :=
@@ -1213,7 +1213,7 @@ theorem aEMeasurable_restrict_of_monotoneOn [LinearOrder β] [OrderClosedTopolog
     {s : Set β} (hs : MeasurableSet s) {f : β → α} (hf : MonotoneOn f s) :
     AEMeasurable f (μ.restrict s) :=
   have this : Monotone (f ∘ coe : s → α) := fun ⟨x, hx⟩ ⟨y, hy⟩ (hxy : x ≤ y) => hf hx hy hxy
-  aEMeasurable_restrict_of_measurable_subtype hs this.Measurable
+  aemeasurable_restrict_of_measurable_subtype hs this.Measurable
 #align ae_measurable_restrict_of_monotone_on aEMeasurable_restrict_of_monotoneOn
 
 protected theorem Antitone.measurable [LinearOrder β] [OrderClosedTopology β] {f : β → α}
@@ -2301,7 +2301,7 @@ theorem aEMeasurable_of_unif_approx {β} [MeasurableSpace β] [PseudoMetricSpace
 theorem measurable_of_tendsto_metrizable_ae {μ : Measure α} [μ.IsComplete] {f : ℕ → α → β}
     {g : α → β} (hf : ∀ n, Measurable (f n))
     (h_ae_tendsto : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))) : Measurable g :=
-  aEMeasurable_iff_measurable.mp
+  aemeasurable_iff_measurable.mp
     (aEMeasurable_of_tendsto_metrizable_ae' (fun i => (hf i).AEMeasurable) h_ae_tendsto)
 #align measurable_of_tendsto_metrizable_ae measurable_of_tendsto_metrizable_ae
 
@@ -2427,7 +2427,7 @@ theorem measurable_smul_const {f : α → 𝕜} {c : E} (hc : c ≠ 0) :
 
 theorem aEMeasurable_smul_const {f : α → 𝕜} {μ : Measure α} {c : E} (hc : c ≠ 0) :
     AEMeasurable (fun x => f x • c) μ ↔ AEMeasurable f μ :=
-  (closedEmbedding_smul_left hc).MeasurableEmbedding.aEMeasurable_comp_iff
+  (closedEmbedding_smul_left hc).MeasurableEmbedding.aemeasurable_comp_iff
 #align ae_measurable_smul_const aEMeasurable_smul_const
 
 end NormedSpace

Mathbin/MeasureTheory/Group/Arithmetic.lean

@@ -893,7 +893,7 @@ theorem List.measurable_prod' (l : List (α → M)) (hl : ∀ f ∈ l, Measurabl
 @[measurability, to_additive]
 theorem List.aEMeasurable_prod' (l : List (α → M)) (hl : ∀ f ∈ l, AEMeasurable f μ) :
     AEMeasurable l.Prod μ := by
-  induction' l with f l ihl; · exact aEMeasurable_one
+  induction' l with f l ihl; · exact aemeasurable_one
   rw [List.forall_mem_cons] at hl
   rw [List.prod_cons]
   exact hl.1.mul (ihl hl.2)

Mathbin/MeasureTheory/Integral/Layercake.lean

@@ -188,7 +188,7 @@ theorem lintegral_comp_eq_lintegral_meas_le_mul (μ : Measure α) [SigmaFinite 
   have ex_G : ∃ G : ℝ → ℝ, Measurable G ∧ 0 ≤ G ∧ g =ᵐ[volume.restrict (Ioi 0)] G :=
     by
     refine' AEMeasurable.exists_measurable_nonneg _ g_nn
-    exact aEMeasurable_Ioi_of_forall_Ioc fun t ht => (g_intble t ht).1.1.AEMeasurable
+    exact aemeasurable_Ioi_of_forall_Ioc fun t ht => (g_intble t ht).1.1.AEMeasurable
   rcases ex_G with ⟨G, G_mble, G_nn, g_eq_G⟩
   have g_eq_G_on : ∀ t, g =ᵐ[volume.restrict (Ioc 0 t)] G := fun t =>
     ae_mono (measure.restrict_mono Ioc_subset_Ioi_self le_rfl) g_eq_G

Mathbin/Probability/IdentDistrib.lean

@@ -109,8 +109,8 @@ protected theorem comp_of_aEMeasurable {u : γ → δ} (h : IdentDistrib f g μ
       exact hu.comp_ae_measurable h.ae_measurable_snd
     map_eq :=
       by
-      rw [← AEMeasurable.map_map_of_aEMeasurable hu h.ae_measurable_fst, ←
-        AEMeasurable.map_map_of_aEMeasurable _ h.ae_measurable_snd, h.map_eq]
+      rw [← AEMeasurable.map_map_of_aemeasurable hu h.ae_measurable_fst, ←
+        AEMeasurable.map_map_of_aemeasurable _ h.ae_measurable_snd, h.map_eq]
       rwa [← h.map_eq] }
 #align probability_theory.ident_distrib.comp_of_ae_measurable ProbabilityTheory.IdentDistrib.comp_of_aEMeasurable
 

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "fb6510c3defb411fe47f1944b61e1ad7d70668a0",
+    "rev": "cf332e598e668a48505829e9415431b92d3a0317",
     "name": "lean3port",
-    "inputRev?": "fb6510c3defb411fe47f1944b61e1ad7d70668a0"}},
+    "inputRev?": "cf332e598e668a48505829e9415431b92d3a0317"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "68b21e12e6d612e77f34febea2e00a9358ce2f76",
+    "rev": "9042f7bc3d4671b6fbf898fb2ce2dbe8c66301f1",
     "name": "mathlib",
-    "inputRev?": "68b21e12e6d612e77f34febea2e00a9358ce2f76"}},
+    "inputRev?": "9042f7bc3d4671b6fbf898fb2ce2dbe8c66301f1"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

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-05-09-20"
+def tag : String := "nightly-2023-05-09-22"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"fb6510c3defb411fe47f1944b61e1ad7d70668a0"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"cf332e598e668a48505829e9415431b92d3a0317"
 
 @[default_target]
 lean_lib Mathbin where