chore(BorelSpace): make MeasurableSpace arguments implicit (#17819)

... rather than instance arguments. This is motivated by non-canonical sigma-algebras showing up in the theory of Gibbs measures.

From GibbsMeasure

Author: YaelDillies

Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean

@@ -94,8 +94,8 @@ end OrderTopology
 
 section Orders
 
-variable [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α]
-variable [MeasurableSpace δ]
+variable [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α]
+variable {mδ : MeasurableSpace δ}
 
 section Preorder
 
@@ -473,7 +473,7 @@ end LinearOrder
 
 section Lattice
 
-variable [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ]
+variable [TopologicalSpace γ] {mγ : MeasurableSpace γ} [BorelSpace γ]
 
 instance (priority := 100) ContinuousSup.measurableSup [Sup γ] [ContinuousSup γ] :
     MeasurableSup γ where
@@ -499,9 +499,9 @@ end Orders
 
 section BorelSpace
 
-variable [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α]
-variable [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β]
-variable [MeasurableSpace δ]
+variable [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
+variable [TopologicalSpace β] {mβ : MeasurableSpace β} [BorelSpace β]
+variable {mδ : MeasurableSpace δ}
 
 section LinearOrder
 
@@ -721,7 +721,7 @@ end LinearOrder
 section ConditionallyCompleteLattice
 
 @[measurability]
-theorem Measurable.iSup_Prop {α} [MeasurableSpace α] [ConditionallyCompleteLattice α]
+theorem Measurable.iSup_Prop {α} {mα : MeasurableSpace α} [ConditionallyCompleteLattice α]
     (p : Prop) {f : δ → α} (hf : Measurable f) : Measurable fun b => ⨆ _ : p, f b := by
   classical
   simp_rw [ciSup_eq_ite]
@@ -730,7 +730,7 @@ theorem Measurable.iSup_Prop {α} [MeasurableSpace α] [ConditionallyCompleteLat
   · exact measurable_const
 
 @[measurability]
-theorem Measurable.iInf_Prop {α} [MeasurableSpace α] [ConditionallyCompleteLattice α]
+theorem Measurable.iInf_Prop {α} {mα : MeasurableSpace α} [ConditionallyCompleteLattice α]
     (p : Prop) {f : δ → α} (hf : Measurable f) : Measurable fun b => ⨅ _ : p, f b := by
   classical
   simp_rw [ciInf_eq_ite]
@@ -923,7 +923,7 @@ section ENNReal
 /-- One can cut out `ℝ≥0∞` into the sets `{0}`, `Ico (t^n) (t^(n+1))` for `n : ℤ` and `{∞}`. This
 gives a way to compute the measure of a set in terms of sets on which a given function `f` does not
 fluctuate by more than `t`. -/
-theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow {α : Type*} [MeasurableSpace α]
+theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow {α : Type*} {mα : MeasurableSpace α}
     (μ : Measure α) {f : α → ℝ≥0∞} (hf : Measurable f) {s : Set α} (hs : MeasurableSet s)
     {t : ℝ≥0} (ht : 1 < t) :
     μ s =

Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean

@@ -130,7 +130,7 @@ theorem measure_ext_Ioo_rat {μ ν : Measure ℝ} [IsLocallyFiniteMeasure μ]
 
 end Real
 
-variable [MeasurableSpace α]
+variable {mα : MeasurableSpace α}
 
 @[measurability, fun_prop]
 theorem measurable_real_toNNReal : Measurable Real.toNNReal :=
@@ -217,15 +217,15 @@ def ennrealEquivSum : ℝ≥0∞ ≃ᵐ ℝ≥0 ⊕ Unit :=
 
 open Function (uncurry)
 
-theorem measurable_of_measurable_nnreal_prod [MeasurableSpace β] [MeasurableSpace γ]
+theorem measurable_of_measurable_nnreal_prod {_ : MeasurableSpace β} {_ : MeasurableSpace γ}
     {f : ℝ≥0∞ × β → γ} (H₁ : Measurable fun p : ℝ≥0 × β => f (p.1, p.2))
     (H₂ : Measurable fun x => f (∞, x)) : Measurable f :=
   let e : ℝ≥0∞ × β ≃ᵐ (ℝ≥0 × β) ⊕ (Unit × β) :=
     (ennrealEquivSum.prodCongr (MeasurableEquiv.refl β)).trans
       (MeasurableEquiv.sumProdDistrib _ _ _)
   e.symm.measurable_comp_iff.1 <| measurable_sum H₁ (H₂.comp measurable_id.snd)
 
-theorem measurable_of_measurable_nnreal_nnreal [MeasurableSpace β] {f : ℝ≥0∞ × ℝ≥0∞ → β}
+theorem measurable_of_measurable_nnreal_nnreal {_ : MeasurableSpace β} {f : ℝ≥0∞ × ℝ≥0∞ → β}
     (h₁ : Measurable fun p : ℝ≥0 × ℝ≥0 => f (p.1, p.2)) (h₂ : Measurable fun r : ℝ≥0 => f (∞, r))
     (h₃ : Measurable fun r : ℝ≥0 => f (r, ∞)) : Measurable f :=
   measurable_of_measurable_nnreal_prod
@@ -382,8 +382,8 @@ theorem AEMeasurable.ennreal_tsum {ι} [Countable ι] {f : ι → α → ℝ≥0
   exact fun s => Finset.aemeasurable_sum s fun i _ => h i
 
 @[measurability, fun_prop]
-theorem AEMeasurable.nnreal_tsum {α : Type*} [MeasurableSpace α] {ι : Type*} [Countable ι]
-    {f : ι → α → NNReal} {μ : MeasureTheory.Measure α} (h : ∀ i : ι, AEMeasurable (f i) μ) :
+theorem AEMeasurable.nnreal_tsum {α : Type*} {_ : MeasurableSpace α} {ι : Type*} [Countable ι]
+    {f : ι → α → NNReal} {μ : Measure α} (h : ∀ i : ι, AEMeasurable (f i) μ) :
     AEMeasurable (fun x : α => ∑' i : ι, f i x) μ := by
   simp_rw [NNReal.tsum_eq_toNNReal_tsum]
   exact (AEMeasurable.ennreal_tsum fun i => (h i).coe_nnreal_ennreal).ennreal_toNNReal
@@ -470,9 +470,8 @@ end NNReal
 spanning measurable sets with finite measure on which `f` is bounded.
 See also `StronglyMeasurable.exists_spanning_measurableSet_norm_le` for functions into normed
 groups. -/
--- We redeclare `α` to temporarily avoid the `[MeasurableSpace α]` instance.
-theorem exists_spanning_measurableSet_le {α : Type*} {m : MeasurableSpace α} {f : α → ℝ≥0}
-    (hf : Measurable f) (μ : Measure α) [SigmaFinite μ] :
+theorem exists_spanning_measurableSet_le {f : α → ℝ≥0} (hf : Measurable f) (μ : Measure α)
+    [SigmaFinite μ] :
     ∃ s : ℕ → Set α,
       (∀ n, MeasurableSet (s n) ∧ μ (s n) < ∞ ∧ ∀ x ∈ s n, f x ≤ n) ∧
       ⋃ i, s i = Set.univ := by