diff --git a/Mathlib/MeasureTheory/Integral/Bochner.lean b/Mathlib/MeasureTheory/Integral/Bochner.lean
index 8364a26b9cc82..7dfa7c53300d6 100644
--- a/Mathlib/MeasureTheory/Integral/Bochner.lean
+++ b/Mathlib/MeasureTheory/Integral/Bochner.lean
@@ -1656,6 +1656,7 @@ theorem integral_subtype_comap {α} [MeasurableSpace α] {μ : Measure α} {s :
   rw [← map_comap_subtype_coe hs]
   exact ((MeasurableEmbedding.subtype_coe hs).integral_map _).symm
 
+attribute [local instance] Measure.Subtype.measureSpace in
 theorem integral_subtype {α} [MeasureSpace α] {s : Set α} (hs : MeasurableSet s) (f : α → G) :
     ∫ x : s, f x = ∫ x in s, f x := integral_subtype_comap hs f
 #align measure_theory.set_integral_eq_subtype MeasureTheory.integral_subtype
diff --git a/Mathlib/MeasureTheory/Integral/Periodic.lean b/Mathlib/MeasureTheory/Integral/Periodic.lean
index de9e66bcd7044..850cddf377ae9 100644
--- a/Mathlib/MeasureTheory/Integral/Periodic.lean
+++ b/Mathlib/MeasureTheory/Integral/Periodic.lean
@@ -142,6 +142,7 @@ noncomputable def measurableEquivIco (a : ℝ) : AddCircle T ≃ᵐ Ico a (a + T
   measurable_invFun := AddCircle.measurable_mk'.comp measurable_subtype_coe
 #align add_circle.measurable_equiv_Ico AddCircle.measurableEquivIco
 
+attribute [local instance] Subtype.measureSpace in
 /-- The lower integral of a function over `AddCircle T` is equal to the lower integral over an
 interval (t, t + T] in `ℝ` of its lift to `ℝ`. -/
 protected theorem lintegral_preimage (t : ℝ) (f : AddCircle T → ℝ≥0∞) :
@@ -164,6 +165,7 @@ protected theorem lintegral_preimage (t : ℝ) (f : AddCircle T → ℝ≥0∞)
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
 
+attribute [local instance] Subtype.measureSpace in
 /-- The integral of an almost-everywhere strongly measurable function over `AddCircle T` is equal
 to the integral over an interval (t, t + T] in `ℝ` of its lift to `ℝ`. -/
 protected theorem integral_preimage (t : ℝ) (f : AddCircle T → E) :
diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
index e1f2f0bfd16bf..0835d2bb5adfa 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -1453,11 +1453,17 @@ section MeasureSpace
 
 variable {s : Set α} [MeasureSpace α] {p : α → Prop}
 
-instance Subtype.measureSpace : MeasureSpace (Subtype p) :=
-  { Subtype.instMeasurableSpace with
-    volume := Measure.comap Subtype.val volume }
+/-- In a measure space, one can restrict the measure to a subtype to get a new measure space.
+
+Not registered as an instance, as there are other natural choices such as the normalized restriction
+for a probability measure, or the subspace measure when restricting to a vector subspace. Enable
+locally if needed with `attribute [local instance] Measure.Subtype.measureSpace`. -/
+def Subtype.measureSpace : MeasureSpace (Subtype p) where
+  volume := Measure.comap Subtype.val volume
 #align measure_theory.measure.subtype.measure_space MeasureTheory.Measure.Subtype.measureSpace
 
+attribute [local instance] Subtype.measureSpace
+
 theorem Subtype.volume_def : (volume : Measure s) = volume.comap Subtype.val :=
   rfl
 #align measure_theory.measure.subtype.volume_def MeasureTheory.Measure.Subtype.volume_def
@@ -4214,12 +4220,12 @@ variable [MeasureSpace α] {s t : Set α}
 
 /-!
 ### Volume on `s : Set α`
--/
 
+Note the instance is provided earlier as `Subtype.measureSpace`.
+-/
+attribute [local instance] Subtype.measureSpace
 
-instance SetCoe.measureSpace (s : Set α) : MeasureSpace s :=
-  ⟨comap ((↑) : s → α) volume⟩
-#align set_coe.measure_space SetCoe.measureSpace
+#align set_coe.measure_space MeasureTheory.Measure.Subtype.measureSpace
 
 theorem volume_set_coe_def (s : Set α) : (volume : Measure s) = comap ((↑) : s → α) volume :=
   rfl