chore(data/set/lattice): use ∃ x ∈ s instead of ∃ x, x ∈ s ∧ in `…

…mem_bUnion_iff` (#1877)

This seems to be more in line with the rest of the library

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/data/semiquot.lean

@@ -27,6 +27,7 @@ variables {α : Type*} {β : Type*}
 
 instance : has_mem α (semiquot α) := ⟨λ a q, a ∈ q.s⟩
 
+/-- Construct a `semiquot α` from `h : a ∈ s` where `s : set α`. -/
 def mk {a : α} {s : set α} (h : a ∈ s) : semiquot α :=
 ⟨s, trunc.mk ⟨a, h⟩⟩
 
@@ -46,15 +47,18 @@ theorem eq_mk_of_mem {q : semiquot α} {a : α} (h : a ∈ q) :
 theorem ne_empty (q : semiquot α) : q.s ≠ ∅ :=
 let ⟨a, h⟩ := q.exists_mem in set.ne_empty_of_mem h
 
+/-- `pure a` is `a` reinterpreted as an unspecified element of `{a}`. -/
 protected def pure (a : α) : semiquot α := mk (set.mem_singleton a)
 
 @[simp] theorem mem_pure' {a b : α} : a ∈ semiquot.pure b ↔ a = b :=
 set.mem_singleton_iff
 
+/-- Replace `s` in a `semiquot` with a superset. -/
 def blur' (q : semiquot α) {s : set α} (h : q.s ⊆ s) : semiquot α :=
 ⟨s, trunc.lift (λ a : q.s, trunc.mk ⟨a.1, h a.2⟩)
   (λ _ _, trunc.eq _ _) q.2⟩
 
+/-- Replace `s` in a `q : semiquot α` with a union `s ∪ q.s` -/
 def blur (s : set α) (q : semiquot α) : semiquot α :=
 blur' q (set.subset_union_right s q.s)
 
@@ -65,12 +69,16 @@ by unfold blur; congr; exact set.union_eq_self_of_subset_right h
 @[simp] theorem mem_blur' (q : semiquot α) {s : set α} (h : q.s ⊆ s)
   {a : α} : a ∈ blur' q h ↔ a ∈ s := iff.rfl
 
+/-- Convert a `trunc α` to a `semiquot α`. -/
 def of_trunc (q : trunc α) : semiquot α :=
 ⟨set.univ, q.map (λ a, ⟨a, trivial⟩)⟩
 
+/-- Convert a `semiquot α` to a `trunc α`. -/
 def to_trunc (q : semiquot α) : trunc α :=
 q.2.map subtype.val
 
+/-- If `f` is a constant on `q.s`, then `q.lift_on f` is the value of `f`
+at any point of `q`. -/
 def lift_on (q : semiquot α) (f : α → β) (h : ∀ a b ∈ q, f a = f b) : β :=
 trunc.lift_on q.2 (λ x, f x.1) (λ x y, h _ _ x.2 y.2)
 
@@ -90,7 +98,7 @@ def bind (q : semiquot α) (f : α → semiquot β) : semiquot β :=
  q.2.bind (λ a, (f a.1).2.map (λ b, ⟨b.1, set.mem_bUnion a.2 b.2⟩))⟩
 
 @[simp] theorem mem_bind (q : semiquot α) (f : α → semiquot β) (b : β) :
-  b ∈ bind q f ↔ ∃ a, a ∈ q ∧ b ∈ f a := set.mem_bUnion_iff
+  b ∈ bind q f ↔ ∃ a ∈ q, b ∈ f a := set.mem_bUnion_iff
 
 instance : monad semiquot :=
 { pure := @semiquot.pure,
@@ -134,7 +142,7 @@ set.singleton_subset_iff
 
 def is_pure (q : semiquot α) := ∀ a b ∈ q, a = b
 
-def get (q) (h : @is_pure α q) : α := lift_on q id h
+def get (q : semiquot α) (h : q.is_pure) : α := lift_on q id h
 
 theorem get_mem {q : semiquot α} (p) : get q p ∈ q :=
 let ⟨a, h⟩ := exists_mem q in
@@ -162,6 +170,7 @@ theorem is_pure.min {s t : semiquot α} (h : is_pure t) : s ≤ t ↔ s = t :=
 theorem is_pure_of_subsingleton [subsingleton α] (q : semiquot α) : is_pure q
 | a b aq bq := subsingleton.elim _ _
 
+/-- `univ : semiquot α` represents an unspecified element of `univ : set α`. -/
 def univ [inhabited α] : semiquot α :=
 mk $ set.mem_univ (default _)
 

src/data/set/lattice.lean

@@ -180,7 +180,7 @@ by rw [diff_eq, compl_Inter, inter_Union]; refl
 /- bounded unions and intersections -/
 
 theorem mem_bUnion_iff {s : set α} {t : α → set β} {y : β} :
-  y ∈ (⋃ x ∈ s, t x) ↔ ∃ x, x ∈ s ∧ y ∈ t x := by simp
+  y ∈ (⋃ x ∈ s, t x) ↔ ∃ x ∈ s, y ∈ t x := by simp
 
 theorem mem_bInter_iff {s : set α} {t : α → set β} {y : β} :
   y ∈ (⋂ x ∈ s, t x) ↔ ∀ x ∈ s, y ∈ t x := by simp

src/group_theory/subgroup.lean

@@ -567,7 +567,7 @@ lemma mem_conjugates_self {a : α} : a ∈ conjugates a := is_conj_refl _
 the elements of s. -/
 def conjugates_of_set (s : set α) : set α := ⋃ a ∈ s, conjugates a
 
-lemma mem_conjugates_of_set_iff {x : α} : x ∈ conjugates_of_set s ↔ ∃ a : α, a ∈ s ∧ is_conj a x :=
+lemma mem_conjugates_of_set_iff {x : α} : x ∈ conjugates_of_set s ↔ ∃ a ∈ s, is_conj a x :=
 set.mem_bUnion_iff
 
 theorem subset_conjugates_of_set : s ⊆ conjugates_of_set s :=

src/topology/bounded_continuous_function.lean

@@ -270,8 +270,7 @@ begin
   rintro ⟨f, hf⟩ ⟨g, hg⟩ f_eq_g,
   /- If two functions have the same approximation, then they are within distance ε -/
   refine lt_of_le_of_lt ((dist_le $ le_of_lt ε₁0).2 (λ x, _)) εε₁,
-  have : ∃x', x' ∈ tα ∧ x ∈ U x' := mem_bUnion_iff.1 (htα (mem_univ x)),
-  rcases this with ⟨x', x'tα, hx'⟩,
+  obtain ⟨x', x'tα, hx'⟩ : ∃x' ∈ tα, x ∈ U x' := mem_bUnion_iff.1 (htα (mem_univ x)),
   refine calc dist (f x) (g x)
       ≤ dist (f x) (f x') + dist (g x) (g x') + dist (f x') (g x') : dist_triangle4_right _ _ _ _
   ... ≤ ε₂ + ε₂ + ε₁/2 : le_of_lt (add_lt_add (add_lt_add _ _) _)

src/topology/metric_space/closeds.lean

@@ -199,7 +199,7 @@ instance closeds.compact_space [compact_space α] : compact_space (closeds α) :
     refine Hausdorff_edist_le_of_mem_edist _ _,
     { assume x hx,
       have : x ∈ ⋃y ∈ s, ball y δ := hs (by simp),
-      rcases mem_bUnion_iff.1 this with ⟨y, ⟨ys, dy⟩⟩,
+      rcases mem_bUnion_iff.1 this with ⟨y, ys, dy⟩,
       have : edist y x < δ := by simp at dy; rwa [edist_comm] at dy,
       exact ⟨y, ⟨ys, ⟨x, hx, this⟩⟩, le_of_lt dy⟩ },
     { rintros x ⟨hx1, ⟨y, yu, hy⟩⟩,

src/topology/metric_space/gromov_hausdorff.lean

@@ -639,13 +639,13 @@ begin
     { -- by construction, `s p` is `ε`-dense
       assume x,
       have : x ∈ ⋃y∈(s p), ball y ε := (hs p).2 (mem_univ _),
-      rcases mem_bUnion_iff.1 this with ⟨y, ⟨ys, hy⟩⟩,
+      rcases mem_bUnion_iff.1 this with ⟨y, ys, hy⟩,
       exact ⟨y, ys, le_of_lt hy⟩ },
     show ∀x : q.rep, ∃ (z : s p), dist x (Φ z) ≤ ε,
     { -- by construction, `s q` is `ε`-dense, and it is the range of `Φ`
       assume x,
       have : x ∈ ⋃y∈(s q), ball y ε := (hs q).2 (mem_univ _),
-      rcases mem_bUnion_iff.1 this with ⟨y, ⟨ys, hy⟩⟩,
+      rcases mem_bUnion_iff.1 this with ⟨y, ys, hy⟩,
       let i := ((E q).to_fun ⟨y, ys⟩).1,
       let hi := ((E q).to_fun ⟨y, ys⟩).2,
       have ihi_eq : (⟨i, hi⟩ : fin (N q)) = (E q).to_fun ⟨y, ys⟩, by rw fin.ext_iff,
@@ -780,13 +780,13 @@ begin
     { -- by construction, `s p` is `ε`-dense
       assume x,
       have : x ∈ ⋃y∈(s p), ball y (u n) := (hs p pt) (mem_univ _),
-      rcases mem_bUnion_iff.1 this with ⟨y, ⟨ys, hy⟩⟩,
+      rcases mem_bUnion_iff.1 this with ⟨y, ys, hy⟩,
       exact ⟨y, ys, le_trans (le_of_lt hy) u_le_ε⟩ },
     show ∀x : q.rep, ∃ (z : s p), dist x (Φ z) ≤ ε,
     { -- by construction, `s q` is `ε`-dense, and it is the range of `Φ`
       assume x,
       have : x ∈ ⋃y∈(s q), ball y (u n) := (hs q qt) (mem_univ _),
-      rcases mem_bUnion_iff.1 this with ⟨y, ⟨ys, hy⟩⟩,
+      rcases mem_bUnion_iff.1 this with ⟨y, ys, hy⟩,
       let i := ((E q).to_fun ⟨y, ys⟩).1,
       let hi := ((E q).to_fun ⟨y, ys⟩).2,
       have ihi_eq : (⟨i, hi⟩ : fin (N q)) = (E q).to_fun ⟨y, ys⟩, by rw fin.ext_iff,