chore: use inferInstanceAs in measure theory (leanprover-community#37206)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/Logic/Encodable/Pi.lean

@@ -30,11 +30,11 @@ variable {α : Type*}
 
 /-- If `α` is encodable, then so is `Vector α n`. -/
 instance List.Vector.encodable [Encodable α] {n} : Encodable (List.Vector α n) :=
-  Subtype.encodable
+  inferInstanceAs <| Encodable (Subtype _)
 
 /-- If `α` is countable, then so is `Vector α n`. -/
 instance List.Vector.countable [Countable α] {n} : Countable (List.Vector α n) :=
-  Subtype.countable
+  inferInstanceAs <| Countable (Subtype _)
 
 /-- If `α` is encodable, then so is `Fin n → α`. -/
 instance finArrow [Encodable α] {n} : Encodable (Fin n → α) :=

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -701,10 +701,10 @@ instance Real.borelSpace : BorelSpace ℝ :=
   ⟨rfl⟩
 
 instance NNReal.measurableSpace : MeasurableSpace ℝ≥0 :=
-  Subtype.instMeasurableSpace
+  inferInstanceAs <| MeasurableSpace (Subtype _)
 
 instance NNReal.borelSpace : BorelSpace ℝ≥0 :=
-  Subtype.borelSpace _
+  inferInstanceAs <| BorelSpace (Subtype _)
 
 instance ENNReal.measurableSpace : MeasurableSpace ℝ≥0∞ :=
   borel ℝ≥0∞

Mathlib/MeasureTheory/Function/LpSpace/Basic.lean

@@ -416,7 +416,7 @@ theorem coe_LpSubmodule : (LpSubmodule 𝕜 E p μ).toAddSubgroup = Lp E p μ :=
   rfl
 
 instance instModule : Module 𝕜 (Lp E p μ) :=
-  { (LpSubmodule 𝕜 E p μ).module with }
+  fast_instance% (LpSubmodule 𝕜 E p μ).module
 
 theorem coeFn_smul (c : 𝕜) (f : Lp E p μ) : ⇑(c • f) =ᵐ[μ] c • ⇑f :=
   AEEqFun.coeFn_smul _ _

Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

@@ -260,7 +260,7 @@ theorem coeFn_smul [IsScalarTower R ℝ≥0 ℝ≥0] (c : R) (μ : FiniteMeasure
   funext; simp [← ENNReal.coe_inj, ENNReal.coe_smul]
 
 set_option backward.isDefEq.respectTransparency false in
-instance instAddCommMonoid : AddCommMonoid (FiniteMeasure Ω) :=
+instance instAddCommMonoid : AddCommMonoid (FiniteMeasure Ω) := fast_instance%
   toMeasure_injective.addCommMonoid _ toMeasure_zero toMeasure_add fun _ _ ↦ toMeasure_smul _ _
 
 /-- Coercion is an `AddMonoidHom`. -/
@@ -331,7 +331,8 @@ theorem restrict_nonzero_iff (μ : FiniteMeasure Ω) (A : Set Ω) : μ.restrict
   simp
 
 /-- The type of finite measures is a measurable space when equipped with the Giry monad. -/
-instance : MeasurableSpace (FiniteMeasure Ω) := Subtype.instMeasurableSpace
+instance : MeasurableSpace (FiniteMeasure Ω) :=
+  inferInstanceAs <| MeasurableSpace (Subtype _)
 
 /-- The set of all finite measures is a measurable set in the Giry monad. -/
 lemma measurableSet_isFiniteMeasure : MeasurableSet { μ : Measure Ω | IsFiniteMeasure μ } := by

Mathlib/MeasureTheory/Measure/NullMeasurable.lean

@@ -85,7 +85,7 @@ instance NullMeasurableSpace.instSubsingleton [h : Subsingleton α] :
   h
 
 instance NullMeasurableSpace.instMeasurableSpace : MeasurableSpace (NullMeasurableSpace α μ) :=
-  @eventuallyMeasurableSpace α inferInstance (ae μ) _
+  fast_instance% @eventuallyMeasurableSpace α inferInstance (ae μ) _
 
 /-- A set is called `NullMeasurableSet` if it can be approximated by a measurable set up to
 a set of null measure. -/

Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

@@ -244,7 +244,8 @@ theorem toFiniteMeasure_nonzero (μ : ProbabilityMeasure Ω) : μ.toFiniteMeasur
   simp [← FiniteMeasure.mass_nonzero_iff]
 
 /-- The type of probability measures is a measurable space when equipped with the Giry monad. -/
-instance : MeasurableSpace (ProbabilityMeasure Ω) := Subtype.instMeasurableSpace
+instance : MeasurableSpace (ProbabilityMeasure Ω) :=
+  inferInstanceAs <| MeasurableSpace (Subtype _)
 
 lemma measurableSet_isProbabilityMeasure :
     MeasurableSet { μ : Measure Ω | IsProbabilityMeasure μ } := by