chore: bump Std (#8834)

leanprover-community · Dec 6, 2023 · a357dd5 · a357dd5
1 parent c6ea155
commit a357dd5
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean b/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
@@ -89,7 +89,7 @@ lemma map_prod_map {α' : Type*} [MeasurableSpace α'] {β' : Type*} [Measurable
     (μ.map f).prod (ν.map g) = (μ.prod ν).map (Prod.map f g) := by
   apply Subtype.ext
   simp only [val_eq_toMeasure, toMeasure_prod, toMeasure_map]
-  rw [Measure.map_prod_map _ _ f_mble g_mble] <;> infer_instance
+  rw [Measure.map_prod_map _ _ f_mble g_mble]
 
 lemma prod_swap : (μ.prod ν).map Prod.swap = ν.prod μ := by
   apply Subtype.ext
@@ -142,7 +142,7 @@ lemma map_prod_map {α' : Type*} [MeasurableSpace α'] {β' : Type*} [Measurable
       = (μ.prod ν).map (f_mble.prod_map g_mble).aemeasurable := by
   apply Subtype.ext
   simp only [val_eq_to_measure, toMeasure_prod, toMeasure_map]
-  rw [Measure.map_prod_map _ _ f_mble g_mble] <;> infer_instance
+  rw [Measure.map_prod_map _ _ f_mble g_mble]
 
 lemma prod_swap : (μ.prod ν).map measurable_swap.aemeasurable = ν.prod μ := by
   apply Subtype.ext

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "9e37a01f8590f81ace095b56710db694b5bf8ca0",
+   "rev": "baf6defee1fe881ae535519c0776f37f6ef08603",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",