feat(MeasureTheory): generalize some theorem to Sort* (#9769)

Generalize some theorems from `{β : Type*} [Countable β] (f : β → α)`
to `{ι : Sort*} [Countable ι] (f : ι → α)`.
This way they automatically work for `f : (p : Prop) → α`.

* Generalize `MeasureTheory.OuterMeasure.iUnion_null`,
  `MeasureTheory.OuterMeasure.iUnion_null_iff`,
  `MeasureTheory.measure_iUnion_null`, and
  `MeasureTheory.measure_iUnion_null_iff`.
* Deprecate `MeasureTheory.OuterMeasure.iUnion_null_iff'`
  and `MeasureTheory.measure_iUnion_null_iff'`.
* Generalize `MeasureTheory.exists_measurable_superset_forall_eq`
  and `MeasureTheory.exists_measure_pos_of_not_measure_iUnion_null`.
* Reorder implicit arguments in some theorems (move `ι` around).

Mathlib/MeasureTheory/Group/FundamentalDomain.lean

@@ -681,9 +681,8 @@ variable [Countable G] [Group G] [MulAction G α] [MeasurableSpace α] {μ : Mea
 
 @[to_additive MeasureTheory.IsAddFundamentalDomain.measure_addFundamentalFrontier]
 theorem measure_fundamentalFrontier : μ (fundamentalFrontier G s) = 0 := by
-  simpa only [fundamentalFrontier, iUnion₂_inter, measure_iUnion_null_iff', one_smul,
-    measure_iUnion_null_iff, inter_comm s, Function.onFun] using fun g (hg : g ≠ 1) =>
-    hs.aedisjoint hg
+  simpa only [fundamentalFrontier, iUnion₂_inter, one_smul, measure_iUnion_null_iff, inter_comm s,
+    Function.onFun] using fun g (hg : g ≠ 1) => hs.aedisjoint hg
 #align measure_theory.is_fundamental_domain.measure_fundamental_frontier MeasureTheory.IsFundamentalDomain.measure_fundamentalFrontier
 #align measure_theory.is_add_fundamental_domain.measure_add_fundamental_frontier MeasureTheory.IsAddFundamentalDomain.measure_addFundamentalFrontier
 

Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

@@ -64,7 +64,7 @@ open Function MeasurableSpace
 
 open Classical Topology BigOperators Filter ENNReal NNReal
 
-variable {α β γ δ ι : Type*}
+variable {α β γ δ : Type*} {ι : Sort*}
 
 namespace MeasureTheory
 
@@ -216,7 +216,7 @@ theorem exists_measurable_superset (μ : Measure α) (s : Set α) :
 
 /-- For every set `s` and a countable collection of measures `μ i` there exists a measurable
 superset `t ⊇ s` such that each measure `μ i` takes the same value on `s` and `t`. -/
-theorem exists_measurable_superset_forall_eq {ι} [Countable ι] (μ : ι → Measure α) (s : Set α) :
+theorem exists_measurable_superset_forall_eq [Countable ι] (μ : ι → Measure α) (s : Set α) :
     ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ i, μ i t = μ i s := by
   simpa only [← measure_eq_trim] using
     OuterMeasure.exists_measurable_superset_forall_eq_trim (fun i => (μ i).toOuterMeasure) s
@@ -267,7 +267,7 @@ theorem measure_biUnion_lt_top {s : Set β} {f : β → Set α} (hs : s.Finite)
   apply ENNReal.sum_lt_top; simpa only [Finite.mem_toFinset]
 #align measure_theory.measure_bUnion_lt_top MeasureTheory.measure_biUnion_lt_top
 
-theorem measure_iUnion_null [Countable β] {s : β → Set α} : (∀ i, μ (s i) = 0) → μ (⋃ i, s i) = 0 :=
+theorem measure_iUnion_null [Countable ι] {s : ι → Set α} : (∀ i, μ (s i) = 0) → μ (⋃ i, s i) = 0 :=
   μ.toOuterMeasure.iUnion_null
 #align measure_theory.measure_Union_null MeasureTheory.measure_iUnion_null
 
@@ -277,15 +277,12 @@ theorem measure_iUnion_null_iff [Countable ι] {s : ι → Set α} :
   μ.toOuterMeasure.iUnion_null_iff
 #align measure_theory.measure_Union_null_iff MeasureTheory.measure_iUnion_null_iff
 
-/-- A version of `measure_iUnion_null_iff` for unions indexed by Props
-TODO: in the long run it would be better to combine this with `measure_iUnion_null_iff` by
-generalising to `Sort`. -/
--- @[simp] -- Porting note: simp can prove this
+@[deprecated] -- Deprecated since 14 January 2024
 theorem measure_iUnion_null_iff' {ι : Prop} {s : ι → Set α} : μ (⋃ i, s i) = 0 ↔ ∀ i, μ (s i) = 0 :=
-  μ.toOuterMeasure.iUnion_null_iff'
+  measure_iUnion_null_iff
 #align measure_theory.measure_Union_null_iff' MeasureTheory.measure_iUnion_null_iff'
 
-theorem measure_biUnion_null_iff {s : Set ι} (hs : s.Countable) {t : ι → Set α} :
+theorem measure_biUnion_null_iff {ι : Type*} {s : Set ι} (hs : s.Countable) {t : ι → Set α} :
     μ (⋃ i ∈ s, t i) = 0 ↔ ∀ i ∈ s, μ (t i) = 0 :=
   μ.toOuterMeasure.biUnion_null_iff hs
 #align measure_theory.measure_bUnion_null_iff MeasureTheory.measure_biUnion_null_iff
@@ -336,7 +333,7 @@ theorem measure_union_eq_top_iff : μ (s ∪ t) = ∞ ↔ μ s = ∞ ∨ μ t =
   not_iff_not.1 <| by simp only [← lt_top_iff_ne_top, ← Ne.def, not_or, measure_union_lt_top_iff]
 #align measure_theory.measure_union_eq_top_iff MeasureTheory.measure_union_eq_top_iff
 
-theorem exists_measure_pos_of_not_measure_iUnion_null [Countable β] {s : β → Set α}
+theorem exists_measure_pos_of_not_measure_iUnion_null [Countable ι] {s : ι → Set α}
     (hs : μ (⋃ n, s n) ≠ 0) : ∃ n, 0 < μ (s n) := by
   contrapose! hs
   exact measure_iUnion_null fun n => nonpos_iff_eq_zero.1 (hs n)
@@ -416,20 +413,19 @@ instance instCountableInterFilter : CountableInterFilter μ.ae := by
   unfold Measure.ae; infer_instance
 #align measure_theory.measure.ae.countable_Inter_filter MeasureTheory.instCountableInterFilter
 
-theorem ae_all_iff {ι : Sort*} [Countable ι] {p : α → ι → Prop} :
-    (∀ᵐ a ∂μ, ∀ i, p a i) ↔ ∀ i, ∀ᵐ a ∂μ, p a i :=
+theorem ae_all_iff [Countable ι] {p : α → ι → Prop} : (∀ᵐ a ∂μ, ∀ i, p a i) ↔ ∀ i, ∀ᵐ a ∂μ, p a i :=
   eventually_countable_forall
 #align measure_theory.ae_all_iff MeasureTheory.ae_all_iff
 
-theorem all_ae_of {ι : Sort _} {p : α → ι → Prop} (hp : ∀ᵐ a ∂μ, ∀ i, p a i) (i : ι) :
+theorem all_ae_of {p : α → ι → Prop} (hp : ∀ᵐ a ∂μ, ∀ i, p a i) (i : ι) :
     ∀ᵐ a ∂μ, p a i := by
   filter_upwards [hp] with a ha using ha i
 
 lemma ae_iff_of_countable [Countable α] {p : α → Prop} : (∀ᵐ x ∂μ, p x) ↔ ∀ x, μ {x} ≠ 0 → p x := by
   rw [ae_iff, measure_null_iff_singleton]
   exacts [forall_congr' fun _ ↦ not_imp_comm, Set.to_countable _]
 
-theorem ae_ball_iff {S : Set ι} (hS : S.Countable) {p : α → ∀ i ∈ S, Prop} :
+theorem ae_ball_iff {ι : Type*} {S : Set ι} (hS : S.Countable) {p : α → ∀ i ∈ S, Prop} :
     (∀ᵐ x ∂μ, ∀ i (hi : i ∈ S), p x i hi) ↔ ∀ i (hi : i ∈ S), ∀ᵐ x ∂μ, p x i hi :=
   eventually_countable_ball hS
 #align measure_theory.ae_ball_iff MeasureTheory.ae_ball_iff

Mathlib/MeasureTheory/Measure/OuterMeasure.lean

@@ -110,36 +110,32 @@ protected theorem iUnion (m : OuterMeasure α) {β} [Countable β] (s : β → S
   rel_iSup_tsum m m.empty (· ≤ ·) m.iUnion_nat s
 #align measure_theory.outer_measure.Union MeasureTheory.OuterMeasure.iUnion
 
-theorem iUnion_null [Countable β] (m : OuterMeasure α) {s : β → Set α} (h : ∀ i, m (s i) = 0) :
-    m (⋃ i, s i) = 0 := by simpa [h] using m.iUnion s
-#align measure_theory.outer_measure.Union_null MeasureTheory.OuterMeasure.iUnion_null
-
-@[simp]
-theorem iUnion_null_iff [Countable β] (m : OuterMeasure α) {s : β → Set α} :
-    m (⋃ i, s i) = 0 ↔ ∀ i, m (s i) = 0 :=
-  ⟨fun h _ => m.mono_null (subset_iUnion _ _) h, m.iUnion_null⟩
-#align measure_theory.outer_measure.Union_null_iff MeasureTheory.OuterMeasure.iUnion_null_iff
-
-/-- A version of `iUnion_null_iff` for unions indexed by Props.
-TODO: in the long run it would be better to combine this with `iUnion_null_iff` by
-generalising to `Sort`. -/
-@[simp]
-theorem iUnion_null_iff' (m : OuterMeasure α) {ι : Prop} {s : ι → Set α} :
-    m (⋃ i, s i) = 0 ↔ ∀ i, m (s i) = 0 :=
-    ⟨ fun h i => mono_null m (subset_iUnion s i) h,
-      by by_cases i : ι <;> simp [i]⟩
-#align measure_theory.outer_measure.Union_null_iff' MeasureTheory.OuterMeasure.iUnion_null_iff'
-
 theorem biUnion_null_iff (m : OuterMeasure α) {s : Set β} (hs : s.Countable) {t : β → Set α} :
     m (⋃ i ∈ s, t i) = 0 ↔ ∀ i ∈ s, m (t i) = 0 := by
-  haveI := hs.toEncodable
-  rw [biUnion_eq_iUnion, iUnion_null_iff, SetCoe.forall']
+  refine ⟨fun h i hi ↦ m.mono_null (subset_biUnion_of_mem hi) h, fun h ↦ ?_⟩
+  have _ := hs.toEncodable
+  simpa [h] using m.iUnion fun x : s ↦ t x
 #align measure_theory.outer_measure.bUnion_null_iff MeasureTheory.OuterMeasure.biUnion_null_iff
 
 theorem sUnion_null_iff (m : OuterMeasure α) {S : Set (Set α)} (hS : S.Countable) :
     m (⋃₀ S) = 0 ↔ ∀ s ∈ S, m s = 0 := by rw [sUnion_eq_biUnion, m.biUnion_null_iff hS]
 #align measure_theory.outer_measure.sUnion_null_iff MeasureTheory.OuterMeasure.sUnion_null_iff
 
+@[simp]
+theorem iUnion_null_iff {ι : Sort*} [Countable ι] (m : OuterMeasure α) {s : ι → Set α} :
+    m (⋃ i, s i) = 0 ↔ ∀ i, m (s i) = 0 := by
+  rw [← sUnion_range, m.sUnion_null_iff (countable_range s), forall_range_iff]
+#align measure_theory.outer_measure.Union_null_iff MeasureTheory.OuterMeasure.iUnion_null_iff
+
+alias ⟨_, iUnion_null⟩ := iUnion_null_iff
+#align measure_theory.outer_measure.Union_null MeasureTheory.OuterMeasure.iUnion_null
+
+@[deprecated] -- Deprecated since 14 January 2024
+theorem iUnion_null_iff' (m : OuterMeasure α) {ι : Prop} {s : ι → Set α} :
+    m (⋃ i, s i) = 0 ↔ ∀ i, m (s i) = 0 :=
+  m.iUnion_null_iff
+#align measure_theory.outer_measure.Union_null_iff' MeasureTheory.OuterMeasure.iUnion_null_iff'
+
 protected theorem iUnion_finset (m : OuterMeasure α) (s : β → Set α) (t : Finset β) :
     m (⋃ i ∈ t, s i) ≤ ∑ i in t, m (s i) :=
   rel_iSup_sum m m.empty (· ≤ ·) m.iUnion_nat s t