feat: port MeasureTheory.MeasurableSpace (#2174)

Co-authored-by: Johan Commelin <johan@commelin.net>

Mathlib.lean

@@ -781,6 +781,7 @@ import Mathlib.Mathport.Attributes
 import Mathlib.Mathport.Notation
 import Mathlib.Mathport.Rename
 import Mathlib.Mathport.Syntax
+import Mathlib.MeasureTheory.MeasurableSpace
 import Mathlib.MeasureTheory.MeasurableSpaceDef
 import Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
 import Mathlib.NumberTheory.Divisors

Mathlib/Data/Set/UnionLift.lean

@@ -79,6 +79,19 @@ theorem unionᵢLift_of_mem (x : T) {i : ι} (hx : (x : α) ∈ S i) :
     unionᵢLift S f hf T hT x = f i ⟨x, hx⟩ := by cases' x with x hx; exact hf _ _ _ _ _
 #align set.Union_lift_of_mem Set.unionᵢLift_of_mem
 
+theorem preimage_unionᵢLift (t : Set β) :
+    unionᵢLift S f hf T hT ⁻¹' t =
+      inclusion hT ⁻¹' (⋃ i, inclusion (subset_unionᵢ S i) '' (f i ⁻¹' t)) := by
+  ext x
+  simp only [mem_preimage, mem_unionᵢ, mem_image]
+  constructor
+  · rcases mem_unionᵢ.1 (hT x.prop) with ⟨i, hi⟩
+    refine fun h => ⟨i, ⟨x, hi⟩, ?_, rfl⟩
+    rwa [unionᵢLift_of_mem x hi] at h
+  · rintro ⟨i, ⟨y, hi⟩, h, hxy⟩
+    obtain rfl : y = x := congr_arg Subtype.val hxy
+    rwa [unionᵢLift_of_mem x hi]
+
 /-- `unionᵢLift_const` is useful for proving that `unionᵢLift` is a homomorphism
   of algebraic structures when defined on the Union of algebraic subobjects.
   For example, it could be used to prove that the lift of a collection
@@ -150,7 +163,7 @@ variable {S : ι → Set α} {f : ∀ (i) (_ : S i), β}
 noncomputable def liftCover (S : ι → Set α) (f : ∀ (i) (_ : S i), β)
     (hf : ∀ (i j) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩)
     (hS : unionᵢ S = univ) (a : α) : β :=
-  unionᵢLift S f hf univ (hS ▸ Set.Subset.refl _) ⟨a, trivial⟩
+  unionᵢLift S f hf univ hS.symm.subset ⟨a, trivial⟩
 #align set.lift_cover Set.liftCover
 
 @[simp]
@@ -163,4 +176,9 @@ theorem liftCover_of_mem {i : ι} {x : α} (hx : (x : α) ∈ S i) :
   unionᵢLift_of_mem (⟨x, trivial⟩ : {_z // True}) hx
 #align set.lift_cover_of_mem Set.liftCover_of_mem
 
+theorem preimage_liftCover (t : Set β) : liftCover S f hf hS ⁻¹' t = ⋃ i, (↑) '' (f i ⁻¹' t) := by
+  change (unionᵢLift S f hf univ hS.symm.subset ∘ fun a => ⟨a, mem_univ a⟩) ⁻¹' t = _
+  rw [preimage_comp, preimage_unionᵢLift]
+  ext; simp
+
 end Set

Mathlib/Logic/Equiv/Set.lean

@@ -219,10 +219,7 @@ protected def pempty (α) : (∅ : Set α) ≃ PEmpty :=
 /-- If sets `s` and `t` are separated by a decidable predicate, then `s ∪ t` is equivalent to
 `s ⊕ t`. -/
 protected def union' {α} {s t : Set α} (p : α → Prop) [DecidablePred p] (hs : ∀ x ∈ s, p x)
-    (ht : ∀ x ∈ t, ¬p x) :
-    (s ∪ t : Set α) ≃
-      Sum s
-        t where
+    (ht : ∀ x ∈ t, ¬p x) : (s ∪ t : Set α) ≃ s ⊕ t where
   toFun x :=
     if hp : p x then Sum.inl ⟨_, x.2.resolve_right fun xt => ht _ xt hp⟩
     else Sum.inr ⟨_, x.2.resolve_left fun xs => hp (hs _ xs)⟩
@@ -237,7 +234,7 @@ protected def union' {α} {s t : Set α} (p : α → Prop) [DecidablePred p] (hs
 
 /-- If sets `s` and `t` are disjoint, then `s ∪ t` is equivalent to `s ⊕ t`. -/
 protected def union {α} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : s ∩ t ⊆ ∅) :
-    (s ∪ t : Set α) ≃ Sum s t :=
+    (s ∪ t : Set α) ≃ s ⊕ t :=
   Set.union' (fun x => x ∈ s) (fun _ => id) fun _ xt xs => H ⟨xs, xt⟩
 #align equiv.set.union Equiv.Set.union
 
@@ -551,6 +548,34 @@ noncomputable def rangeSplittingImageEquiv {α β : Type _} (f : α → β) (s :
 #align equiv.set.range_splitting_image_equiv_symm_apply_coe Equiv.Set.rangeSplittingImageEquiv_symm_apply_coe
 #align equiv.set.range_splitting_image_equiv_apply_coe_coe Equiv.Set.rangeSplittingImageEquiv_apply_coe_coe
 
+/-- Equivalence between the range of `Sum.inl : α → α ⊕ β` and `α`. -/
+@[simps symm_apply_coe]
+def rangeInl (α β : Type _) : Set.range (Sum.inl : α → α ⊕ β) ≃ α where
+  toFun
+  | ⟨.inl x, _⟩ => x
+  | ⟨.inr _, h⟩ => False.elim <| by rcases h with ⟨x, h'⟩; cases h'
+  invFun x := ⟨.inl x, mem_range_self _⟩
+  left_inv := fun ⟨_, _, rfl⟩ => rfl
+  right_inv x := rfl
+
+@[simp] lemma rangeInl_apply_inl {α : Type _} (β : Type _) (x : α) :
+    (rangeInl α β) ⟨.inl x, mem_range_self _⟩ = x :=
+  rfl
+
+/-- Equivalence between the range of `Sum.inr : β → α ⊕ β` and `β`. -/
+@[simps symm_apply_coe]
+def rangeInr (α β : Type _) : Set.range (Sum.inr : β → α ⊕ β) ≃ β where
+  toFun
+  | ⟨.inl _, h⟩ => False.elim <| by rcases h with ⟨x, h'⟩; cases h'
+  | ⟨.inr x, _⟩ => x
+  invFun x := ⟨.inr x, mem_range_self _⟩
+  left_inv := fun ⟨_, _, rfl⟩ => rfl
+  right_inv x := rfl
+
+@[simp] lemma rangeInr_apply_inr (α : Type _) {β : Type _} (x : β) :
+    (rangeInr α β) ⟨.inr x, mem_range_self _⟩ = x :=
+  rfl
+
 end Set
 
 /-- If `f : α → β` has a left-inverse when `α` is nonempty, then `α` is computably equivalent to the
@@ -617,10 +642,8 @@ theorem self_comp_ofInjective_symm {α β} {f : α → β} (hf : Injective f) :
 theorem ofLeftInverse_eq_ofInjective {α β : Type _} (f : α → β) (f_inv : Nonempty α → β → α)
     (hf : ∀ h : Nonempty α, LeftInverse (f_inv h) f) :
     ofLeftInverse f f_inv hf =
-      ofInjective f
-        ((em (Nonempty α)).elim (fun h => (hf h).injective) fun h _ _ _ => by
-          haveI : Subsingleton α := subsingleton_of_not_nonempty h
-          simp) := by
+      ofInjective f ((isEmpty_or_nonempty α).elim (fun h _ _ _ => Subsingleton.elim _ _)
+        (fun h => (hf h).injective)) := by
   ext
   simp
 #align equiv.of_left_inverse_eq_of_injective Equiv.ofLeftInverse_eq_ofInjective