Merge master into nightly-testing

leanprover-community · Dec 6, 2023 · e7aebe0 · e7aebe0
2 parents da80ad9 + a357dd5
commit e7aebe0
Showing 1 changed file with 2 additions and 2 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