feat(data/set/lattice): new lemma Union_singleton_eq_range (#10819)

src/data/set/basic.lean

@@ -1673,6 +1673,8 @@ alias range_iff_surjective ↔ _ function.surjective.range_eq
 
 @[simp] theorem range_id : range (@id α) = univ := range_iff_surjective.2 surjective_id
 
+@[simp] theorem range_id' : range (λ (x : α), x) = univ := range_id
+
 @[simp] theorem _root_.prod.range_fst [nonempty β] : range (prod.fst : α × β → α) = univ :=
 prod.fst_surjective.range_eq
 

src/data/set/intervals/proj_Icc.lean

@@ -84,7 +84,7 @@ f ∘ proj_Icc a b h
 
 @[simp] lemma Icc_extend_range (f : Icc a b → β) :
   range (Icc_extend h f) = range f :=
-by simp [Icc_extend, range_comp f]
+by simp only [Icc_extend, range_comp f, range_proj_Icc, range_id']
 
 lemma Icc_extend_of_le_left (f : Icc a b → β) (hx : x ≤ a) :
   Icc_extend h f x = f ⟨a, left_mem_Icc.2 h⟩ :=

src/data/set/lattice.lean

@@ -843,10 +843,14 @@ lemma Union_subset_Union2 {s : ι → set α} {t : ι₂ → set α} (h : ∀ i,
 lemma Union_subset_Union_const {s : set α} (h : ι → ι₂) : (⋃ i : ι, s) ⊆ (⋃ j : ι₂, s) :=
 @supr_le_supr_const (set α) ι ι₂ _ s h
 
-@[simp] lemma Union_of_singleton (α : Type*) : (⋃ x, {x} : set α) = univ :=
-Union_eq_univ_iff.2 $ λ x, ⟨x, rfl⟩
+@[simp] lemma Union_singleton_eq_range {α β : Type*} (f : α → β) :
+  (⋃ (x : α), {f x}) = range f :=
+by { ext x, simp [@eq_comm _ x] }
 
-@[simp] lemma Union_of_singleton_coe (s : set α) :
+lemma Union_of_singleton (α : Type*) : (⋃ x, {x} : set α) = univ :=
+by simp
+
+lemma Union_of_singleton_coe (s : set α) :
   (⋃ (i : s), {i} : set α) = s :=
 by simp
 

src/measure_theory/constructions/borel_space.lean

@@ -1410,7 +1410,7 @@ begin
     simp only [mem_Union, mem_singleton_iff], rintro ⟨a, b, h, rfl⟩,
     rw (set.ext (λ x, _) : Ioo (a : ℝ) b = (⋃c>a, (Iio c)ᶜ) ∩ Iio b),
     { have hg : ∀ q : ℚ, g.measurable_set' (Iio q) :=
-        λ q, generate_measurable.basic (Iio q) (by { simp, exact ⟨_, rfl⟩ }),
+        λ q, generate_measurable.basic (Iio q) (by simp),
       refine @measurable_set.inter _ g _ _ _ (hg _),
       refine @measurable_set.bUnion _ _ g _ _ (countable_encodable _) (λ c h, _),
       exact @measurable_set.compl _ _ g (hg _) },

src/measure_theory/integral/lebesgue.lean

@@ -236,7 +236,7 @@ theorem map_map (g : β → γ) (h: γ → δ) (f : α →ₛ β) : (f.map g).ma
 
 @[simp] theorem range_map [decidable_eq γ] (g : β → γ) (f : α →ₛ β) :
   (f.map g).range = f.range.image g :=
-finset.coe_injective $ by simp [range_comp]
+finset.coe_injective $ by simp only [coe_range, coe_map, finset.coe_image, range_comp]
 
 @[simp] theorem map_const (g : β → γ) (b : β) : (const α b).map g = const α (g b) := rfl