From 1c491695ee6586e02b5f1da82271cb9754762e77 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 18 Jun 2023 01:58:00 -0500
Subject: [PATCH] feat: add instances for `MeasurableSpace.CountablyGenerated`

---
 Mathlib/MeasureTheory/MeasurableSpace.lean    | 28 +++++++++++++++++--
 .../MeasureTheory/Measure/OuterMeasure.lean   |  7 ++---
 2 files changed, 28 insertions(+), 7 deletions(-)

diff --git a/Mathlib/MeasureTheory/MeasurableSpace.lean b/Mathlib/MeasureTheory/MeasurableSpace.lean
index 449139effdb67..e319883dacead 100644
--- a/Mathlib/MeasureTheory/MeasurableSpace.lean
+++ b/Mathlib/MeasureTheory/MeasurableSpace.lean
@@ -1639,9 +1639,33 @@ variable (α)
 /-- We say a measurable space is countably generated
 if can be generated by a countable set of sets.-/
 class CountablyGenerated [m : MeasurableSpace α] : Prop where
-  IsCountablyGenerated : ∃ b : Set (Set α), b.Countable ∧ m = generateFrom b
+  isCountablyGenerated : ∃ b : Set (Set α), b.Countable ∧ m = generateFrom b
 #align measurable_space.countably_generated MeasurableSpace.CountablyGenerated
 
+variable {α}
+
+theorem CountablyGenerated.comap [m : MeasurableSpace β] [h : CountablyGenerated β] (f : α → β) :
+    @CountablyGenerated α (.comap f m) := by
+  rcases h with ⟨⟨b, hbc, rfl⟩⟩
+  rw [comap_generateFrom]
+  letI := generateFrom (preimage f '' b)
+  exact ⟨_, hbc.image _, rfl⟩
+
+theorem CountablyGenerated.sup {m₁ m₂ : MeasurableSpace β} (h₁ : @CountablyGenerated β m₁)
+    (h₂ : @CountablyGenerated β m₂) : @CountablyGenerated β (m₁ ⊔ m₂) := by
+  rcases h₁ with ⟨⟨b₁, hb₁c, rfl⟩⟩
+  rcases h₂ with ⟨⟨b₂, hb₂c, rfl⟩⟩
+  exact @mk _ (_ ⊔ _) ⟨_, hb₁c.union hb₂c, generateFrom_sup_generateFrom⟩
+
+instance [MeasurableSpace α] [CountablyGenerated α] {p : α → Prop} :
+    CountablyGenerated { x // p x } := .comap _
+
+instance [MeasurableSpace α] [CountablyGenerated α] [MeasurableSpace β] [CountablyGenerated β] :
+    CountablyGenerated (α × β) :=
+  .sup (.comap Prod.fst) (.comap Prod.snd)
+
+variable (α)
+
 open Classical
 
 /-- If a measurable space is countably generated, it admits a measurable injection
@@ -1649,7 +1673,7 @@ into the Cantor space `ℕ → Bool` (equipped with the product sigma algebra).
 theorem measurable_injection_nat_bool_of_countablyGenerated [MeasurableSpace α]
     [h : CountablyGenerated α] [MeasurableSingletonClass α] :
     ∃ f : α → ℕ → Bool, Measurable f ∧ Function.Injective f := by
-  obtain ⟨b, bct, hb⟩ := h.IsCountablyGenerated
+  obtain ⟨b, bct, hb⟩ := h.isCountablyGenerated
   obtain ⟨e, he⟩ := Set.Countable.exists_eq_range (bct.insert ∅) (insert_nonempty _ _)
   rw [← generateFrom_insert_empty, he] at hb
   refine' ⟨fun x n => x ∈ e n, _, _⟩
diff --git a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean
index c63a12f44bf14..90615df0cc184 100644
--- a/Mathlib/MeasureTheory/Measure/OuterMeasure.lean
+++ b/Mathlib/MeasureTheory/Measure/OuterMeasure.lean
@@ -169,11 +169,8 @@ theorem null_of_locally_null [TopologicalSpace α] [SecondCountableTopology α]
 theorem exists_mem_forall_mem_nhds_within_pos [TopologicalSpace α] [SecondCountableTopology α]
     (m : OuterMeasure α) {s : Set α} (hs : m s ≠ 0) : ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, 0 < m t := by
   contrapose! hs
-  simp only [nonpos_iff_eq_zero, ← exists_prop] at hs
-  apply m.null_of_locally_null s
-  intro x hx
-  specialize hs x hx
-  exact Iff.mp bex_def hs
+  simp only [nonpos_iff_eq_zero] at hs
+  exact m.null_of_locally_null s hs
 #align measure_theory.outer_measure.exists_mem_forall_mem_nhds_within_pos MeasureTheory.OuterMeasure.exists_mem_forall_mem_nhds_within_pos
 
 /-- If `s : ι → Set α` is a sequence of sets, `S = ⋃ n, s n`, and `m (S \ s n)` tends to zero along