refactor(data/set/lattice): Generalize mem_bUnion_iff and `mem_bInt…

…er_iff` to dependent families (#11485)

They're now called `mem_Union₂` and `mem_Inter₂`.

src/algebra/algebra/subalgebra.lean

@@ -567,7 +567,7 @@ lemma mem_inf {S T : subalgebra R A} {x : A} : x ∈ S ⊓ T ↔ x ∈ S ∧ x 
 lemma coe_Inf (S : set (subalgebra R A)) : (↑(Inf S) : set A) = ⋂ s ∈ S, ↑s := Inf_image
 
 lemma mem_Inf {S : set (subalgebra R A)} {x : A} : x ∈ Inf S ↔ ∀ p ∈ S, x ∈ p :=
-by simp only [← set_like.mem_coe, coe_Inf, set.mem_bInter_iff]
+by simp only [← set_like.mem_coe, coe_Inf, set.mem_Inter₂]
 
 @[simp] lemma Inf_to_submodule (S : set (subalgebra R A)) :
   (Inf S).to_submodule = Inf (subalgebra.to_submodule '' S) :=

src/algebra/lie/subalgebra.lean

@@ -446,7 +446,7 @@ def lie_span : lie_subalgebra R L := Inf {N | s ⊆ N}
 variables {R L s}
 
 lemma mem_lie_span {x : L} : x ∈ lie_span R L s ↔ ∀ K : lie_subalgebra R L, s ⊆ K → x ∈ K :=
-by { change x ∈ (lie_span R L s : set L) ↔ _, erw Inf_coe, exact set.mem_bInter_iff, }
+by { change x ∈ (lie_span R L s : set L) ↔ _, erw Inf_coe, exact set.mem_Inter₂, }
 
 lemma subset_lie_span : s ⊆ lie_span R L s :=
 by { intros m hm, erw mem_lie_span, intros K hK, exact hK hm, }

src/algebra/lie/submodule.lean

@@ -418,7 +418,7 @@ def lie_span : lie_submodule R L M := Inf {N | s ⊆ N}
 variables {R L s}
 
 lemma mem_lie_span {x : M} : x ∈ lie_span R L s ↔ ∀ N : lie_submodule R L M, s ⊆ N → x ∈ N :=
-by { change x ∈ (lie_span R L s : set M) ↔ _, erw Inf_coe, exact mem_bInter_iff, }
+by { change x ∈ (lie_span R L s : set M) ↔ _, erw Inf_coe, exact mem_Inter₂, }
 
 lemma subset_lie_span : s ⊆ lie_span R L s :=
 by { intros m hm, erw mem_lie_span, intros N hN, exact hN hm, }

src/algebra/module/submodule_lattice.lean

@@ -184,7 +184,7 @@ by rw [infi, Inf_coe]; ext a; simp; exact
 ⟨λ h i, h _ i rfl, λ h i x e, e ▸ h _⟩
 
 @[simp] lemma mem_Inf {S : set (submodule R M)} {x : M} : x ∈ Inf S ↔ ∀ p ∈ S, x ∈ p :=
-set.mem_bInter_iff
+set.mem_Inter₂
 
 @[simp] theorem mem_infi {ι} (p : ι → submodule R M) {x} :
   x ∈ (⨅ i, p i) ↔ ∀ i, x ∈ p i :=

src/algebra/support.lean

@@ -213,7 +213,7 @@ end
 
 lemma support_prod_subset [comm_monoid_with_zero A] (s : finset α) (f : α → β → A) :
   support (λ x, ∏ i in s, f i x) ⊆ ⋂ i ∈ s, support (f i) :=
-λ x hx, mem_bInter_iff.2 $ λ i hi H, hx $ finset.prod_eq_zero hi H
+λ x hx, mem_Inter₂.2 $ λ i hi H, hx $ finset.prod_eq_zero hi H
 
 lemma support_prod [comm_monoid_with_zero A] [no_zero_divisors A] [nontrivial A]
   (s : finset α) (f : α → β → A) :

src/algebraic_geometry/structure_sheaf.lean

@@ -776,7 +776,7 @@ begin
     intros x hx,
     erw topological_space.opens.mem_supr,
     have := ht_cover hx,
-    rw [← finset.set_bUnion_coe, set.mem_bUnion_iff] at this,
+    rw [← finset.set_bUnion_coe, set.mem_Union₂] at this,
     rcases this with ⟨i, i_mem, x_mem⟩,
     use [i, i_mem] },
 

src/analysis/box_integral/partition/basic.lean

@@ -169,7 +169,7 @@ lemma Union_def : π.Union = ⋃ J ∈ π, ↑J := rfl
 
 lemma Union_def' : π.Union = ⋃ J ∈ π.boxes, ↑J := rfl
 
-@[simp] lemma mem_Union : x ∈ π.Union ↔ ∃ J ∈ π, x ∈ J := set.mem_bUnion_iff
+@[simp] lemma mem_Union : x ∈ π.Union ↔ ∃ J ∈ π, x ∈ J := set.mem_Union₂
 
 @[simp] lemma Union_single (h : J ≤ I) : (single I J h).Union = J := by simp [Union_def]
 

src/analysis/box_integral/partition/split.lean

@@ -287,7 +287,7 @@ begin
     refine ⟨_, ⟨J₁, ⟨h₁, subset.trans _ (π.subset_Union hJ)⟩, rfl⟩, le_rfl⟩,
     exact ht I J hJ J₁ h₁ (mt disjoint_iff.1 hne) },
   { rw mem_filter at hJ,
-    rcases set.mem_bUnion_iff.1 (hJ.2 J.upper_mem) with ⟨J', hJ', hmem⟩,
+    rcases set.mem_Union₂.1 (hJ.2 J.upper_mem) with ⟨J', hJ', hmem⟩,
     refine ⟨J', hJ', ht I _ hJ' _ hJ.1 $ box.not_disjoint_coe_iff_nonempty_inter.2 _⟩,
     exact ⟨J.upper, hmem, J.upper_mem⟩  }
 end

src/analysis/box_integral/partition/tagged.lean

@@ -58,7 +58,7 @@ lemma Union_def : π.Union = ⋃ J ∈ π, ↑J := rfl
 
 @[simp] lemma Union_to_prepartition : π.to_prepartition.Union = π.Union := rfl
 
-@[simp] lemma mem_Union : x ∈ π.Union ↔ ∃ J ∈ π, x ∈ J := set.mem_bUnion_iff
+@[simp] lemma mem_Union : x ∈ π.Union ↔ ∃ J ∈ π, x ∈ J := set.mem_Union₂
 
 lemma subset_Union (h : J ∈ π) : ↑J ⊆ π.Union := subset_bUnion_of_mem h
 
@@ -278,7 +278,7 @@ def disj_union (π₁ π₂ : tagged_prepartition I) (h : disjoint π₁.Union 
   tag_mem_Icc := λ J, by { dunfold finset.piecewise, split_ifs,
     exacts [π₁.tag_mem_Icc J, π₂.tag_mem_Icc J]  } }
 
-@[simp] lemma disj_union_boxes (h : disjoint π₁.Union π₂.Union) : 
+@[simp] lemma disj_union_boxes (h : disjoint π₁.Union π₂.Union) :
   (π₁.disj_union π₂ h).boxes = π₁.boxes ∪ π₂.boxes := rfl
 
 @[simp] lemma mem_disj_union (h : disjoint π₁.Union π₂.Union) :

src/analysis/convex/cone.lean

@@ -111,11 +111,10 @@ lemma mem_inf {x} : x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T := iff.rfl
 
 instance : has_Inf (convex_cone 𝕜 E) :=
 ⟨λ S, ⟨⋂ s ∈ S, ↑s,
-  λ c hc x hx, mem_bInter $ λ s hs, s.smul_mem hc $ by apply mem_bInter_iff.1 hx s hs,
-  λ x hx y hy, mem_bInter $ λ s hs, s.add_mem (by apply mem_bInter_iff.1 hx s hs)
-    (by apply mem_bInter_iff.1 hy s hs)⟩⟩
+  λ c hc x hx, mem_bInter $ λ s hs, s.smul_mem hc $ mem_Inter₂.1 hx s hs,
+  λ x hx y hy, mem_bInter $ λ s hs, s.add_mem (mem_Inter₂.1 hx s hs) (mem_Inter₂.1 hy s hs)⟩⟩
 
-lemma mem_Inf {x : E} {S : set (convex_cone 𝕜 E)} : x ∈ Inf S ↔ ∀ s ∈ S, x ∈ s := mem_bInter_iff
+lemma mem_Inf {x : E} {S : set (convex_cone 𝕜 E)} : x ∈ Inf S ↔ ∀ s ∈ S, x ∈ s := mem_Inter₂
 
 variables (𝕜)
 

src/analysis/convex/extreme.lean

@@ -118,7 +118,7 @@ lemma is_extreme_bInter {F : set (set E)} (hF : F.nonempty)
 begin
   obtain ⟨B, hB⟩ := hF,
   refine ⟨(bInter_subset_of_mem hB).trans (hAF B hB).1, λ x₁ x₂ hx₁A hx₂A x hxF hx, _⟩,
-  simp_rw mem_bInter_iff at ⊢ hxF,
+  simp_rw mem_Inter₂ at ⊢ hxF,
   have h := λ B hB, (hAF B hB).2 x₁ x₂ hx₁A hx₂A x (hxF B hB) hx,
   exact ⟨λ B hB, (h B hB).1, λ B hB, (h B hB).2⟩,
 end

src/analysis/convex/simplicial_complex/basic.lean

@@ -68,7 +68,7 @@ instance : has_mem (finset E) (simplicial_complex 𝕜 E) := ⟨λ s K, s ∈ K.
 /-- The underlying space of a simplicial complex is the union of its faces. -/
 def space (K : simplicial_complex 𝕜 E) : set E := ⋃ s ∈ K.faces, convex_hull 𝕜 (s : set E)
 
-lemma mem_space_iff : x ∈ K.space ↔ ∃ s ∈ K.faces, x ∈ convex_hull 𝕜 (s : set E) := mem_bUnion_iff
+lemma mem_space_iff : x ∈ K.space ↔ ∃ s ∈ K.faces, x ∈ convex_hull 𝕜 (s : set E) := mem_Union₂
 
 lemma convex_hull_subset_space (hs : s ∈ K.faces) : convex_hull 𝕜 ↑s ⊆ K.space :=
 subset_bUnion_of_mem hs
@@ -134,7 +134,7 @@ lemma vertices_eq : K.vertices = ⋃ k ∈ K.faces, (k : set E) :=
 begin
   ext x,
   refine ⟨λ h, mem_bUnion h $ mem_coe.2 $ mem_singleton_self x, λ h, _⟩,
-  obtain ⟨s, hs, hx⟩ := mem_bUnion_iff.1 h,
+  obtain ⟨s, hs, hx⟩ := mem_Union₂.1 h,
   exact K.down_closed hs (finset.singleton_subset_iff.2 $ mem_coe.1 hx) (singleton_ne_empty _),
 end
 

src/data/finset/basic.lean

@@ -836,7 +836,7 @@ begin
     obtain ⟨i : ι , hic : i ∈ c, hti : (t : set α) ⊆ f i⟩ :=
       htc (set.subset.trans (t.subset_insert b) hbtc),
     obtain ⟨j, hjc, hbj⟩ : ∃ j ∈ c, b ∈ f j,
-      by simpa [set.mem_bUnion_iff] using hbtc (t.mem_insert_self b),
+      by simpa [set.mem_Union₂] using hbtc (t.mem_insert_self b),
     rcases hc j hjc i hic with ⟨k, hkc, hk, hk'⟩,
     use [k, hkc],
     rw [coe_insert, set.insert_subset],

src/data/semiquot.lean

@@ -106,7 +106,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 ∈ q, b ∈ f a := set.mem_bUnion_iff
+  b ∈ bind q f ↔ ∃ a ∈ q, b ∈ f a := set.mem_Union₂
 
 instance : monad semiquot :=
 { pure := @semiquot.pure,

src/data/set/accumulate.lean

@@ -20,7 +20,7 @@ def accumulate [has_le α] (s : α → set β) (x : α) : set β := ⋃ y ≤ x,
 variable {s}
 lemma accumulate_def [has_le α] {x : α} : accumulate s x = ⋃ y ≤ x, s y := rfl
 @[simp] lemma mem_accumulate [has_le α] {x : α} {z : β} : z ∈ accumulate s x ↔ ∃ y ≤ x, z ∈ s y :=
-mem_bUnion_iff
+mem_Union₂
 
 lemma subset_accumulate [preorder α] {x : α} : s x ⊆ accumulate s x :=
 λ z, mem_bUnion le_rfl

src/data/set/lattice.lean

@@ -77,10 +77,18 @@ notation `⋂` binders `, ` r:(scoped f, Inter f) := r
 ⟨λ ⟨t, ⟨⟨a, (t_eq : s a = t)⟩, (h : x ∈ t)⟩⟩, ⟨a, t_eq.symm ▸ h⟩,
   λ ⟨a, h⟩, ⟨s a, ⟨⟨a, rfl⟩, h⟩⟩⟩
 
+theorem mem_Union₂ {x : γ} {β : α → Sort*} {s : Π a, β a → set γ} :
+  x ∈ (⋃ a b, s a b) ↔ ∃ a b, x ∈ s a b :=
+by simp only [set.mem_Union]
+
 @[simp] theorem mem_Inter {x : β} {s : ι → set β} : x ∈ Inter s ↔ ∀ i, x ∈ s i :=
 ⟨λ (h : ∀ a ∈ {a : set β | ∃ i, s i = a}, x ∈ a) a, h (s a) ⟨a, rfl⟩,
   λ h t ⟨a, (eq : s a = t)⟩, eq ▸ h a⟩
 
+theorem mem_Inter₂ {x : γ} {β : α → Sort*} {s : Π a, β a → set γ} :
+  x ∈ (⋂ a b, s a b) ↔ ∀ a b, x ∈ s a b :=
+by simp only [set.mem_Inter]
+
 theorem mem_sUnion {x : α} {S : set (set α)} : x ∈ ⋃₀ S ↔ ∃ t ∈ S, x ∈ t := iff.rfl
 
 instance : complete_boolean_algebra (set α) :=
@@ -482,23 +490,13 @@ by simp only [Inter_or, Inter_inter_distrib, Inter_Inter_eq_left]
 
 /-! ### Bounded unions and intersections -/
 
-theorem mem_bUnion_iff {s : set α} {t : α → set β} {y : β} :
-  y ∈ (⋃ x ∈ s, t x) ↔ ∃ x ∈ s, y ∈ t x := by simp
-
-lemma mem_bUnion_iff' {p : α → Prop} {t : α → set β} {y : β} :
-  y ∈ (⋃ i (h : p i), t i) ↔ ∃ i (h : p i), y ∈ t i :=
-mem_bUnion_iff
-
-theorem mem_bInter_iff {s : set α} {t : α → set β} {y : β} :
-  y ∈ (⋂ x ∈ s, t x) ↔ ∀ x ∈ s, y ∈ t x := by simp
-
 theorem mem_bUnion {s : set α} {t : α → set β} {x : α} {y : β} (xs : x ∈ s) (ytx : y ∈ t x) :
   y ∈ ⋃ x ∈ s, t x :=
-mem_bUnion_iff.2 ⟨x, ⟨xs, ytx⟩⟩
+mem_Union₂.2 ⟨x, ⟨xs, ytx⟩⟩
 
 theorem mem_bInter {s : set α} {t : α → set β} {y : β} (h : ∀ x ∈ s, y ∈ t x) :
   y ∈ ⋂ x ∈ s, t x :=
-mem_bInter_iff.2 h
+mem_Inter₂.2 h
 
 theorem bUnion_subset {s : set α} {t : set β} {u : α → set β} (h : ∀ x ∈ s, u x ⊆ t) :
   (⋃ x ∈ s, u x) ⊆ t :=

src/data/set/pairwise.lean

@@ -325,7 +325,7 @@ lemma bUnion_diff_bUnion_eq {s t : set ι} {f : ι → set α} (h : (s ∪ t).pa
 begin
   refine (bUnion_diff_bUnion_subset f s t).antisymm
     (bUnion_subset $ λ i hi a ha, (mem_diff _).2 ⟨mem_bUnion hi.1 ha, _⟩),
-  rw mem_bUnion_iff, rintro ⟨j, hj, haj⟩,
+  rw mem_Union₂, rintro ⟨j, hj, haj⟩,
   exact h (or.inl hi.1) (or.inr hj) (ne_of_mem_of_not_mem hj hi.2).symm ⟨ha, haj⟩,
 end
 

src/dynamics/ergodic/conservative.lean

@@ -90,7 +90,7 @@ begin
   have : μ ((s ∩ (f^[n]) ⁻¹' s) \ T) ≠ 0, by rwa [measure_diff_null hμT],
   rcases hf.exists_mem_image_mem ((hs.inter (hf.measurable.iterate n hs)).diff hT) this
     with ⟨x, ⟨⟨hxs, hxn⟩, hxT⟩, m, hm0, ⟨hxms, hxm⟩, hxx⟩,
-  refine hxT ⟨hxs, mem_bUnion_iff.2 ⟨n + m, _, _⟩⟩,
+  refine hxT ⟨hxs, mem_Union₂.2 ⟨n + m, _, _⟩⟩,
   { exact add_le_add hn (nat.one_le_of_lt $ pos_iff_ne_zero.2 hm0) },
   { rwa [set.mem_preimage, ← iterate_add_apply] at hxm }
 end

src/group_theory/subgroup/basic.lean

@@ -522,14 +522,14 @@ lemma mem_inf {p p' : subgroup G} {x : G} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈
 @[to_additive]
 instance : has_Inf (subgroup G) :=
 ⟨λ s,
-  { inv_mem' := λ x hx, set.mem_bInter $ λ i h, i.inv_mem (by apply set.mem_bInter_iff.1 hx i h),
+  { inv_mem' := λ x hx, set.mem_bInter $ λ i h, i.inv_mem (by apply set.mem_Inter₂.1 hx i h),
     .. (⨅ S ∈ s, subgroup.to_submonoid S).copy (⋂ S ∈ s, ↑S) (by simp) }⟩
 
 @[simp, norm_cast, to_additive]
 lemma coe_Inf (H : set (subgroup G)) : ((Inf H : subgroup G) : set G) = ⋂ s ∈ H, ↑s := rfl
 
 @[simp, to_additive]
-lemma mem_Inf {S : set (subgroup G)} {x : G} : x ∈ Inf S ↔ ∀ p ∈ S, x ∈ p := set.mem_bInter_iff
+lemma mem_Inf {S : set (subgroup G)} {x : G} : x ∈ Inf S ↔ ∀ p ∈ S, x ∈ p := set.mem_Inter₂
 
 @[to_additive]
 lemma mem_infi {ι : Sort*} {S : ι → subgroup G} {x : G} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i :=
@@ -1316,7 +1316,7 @@ the elements of `s`. -/
 def conjugates_of_set (s : set G) : set G := ⋃ a ∈ s, conjugates_of a
 
 lemma mem_conjugates_of_set_iff {x : G} : x ∈ conjugates_of_set s ↔ ∃ a ∈ s, is_conj a x :=
-set.mem_bUnion_iff
+set.mem_Union₂
 
 theorem subset_conjugates_of_set : s ⊆ conjugates_of_set s :=
 λ (x : G) (h : x ∈ s), mem_conjugates_of_set_iff.2 ⟨x, h, is_conj.refl _⟩

src/group_theory/submonoid/basic.lean

@@ -175,13 +175,13 @@ instance : has_Inf (submonoid M) :=
 { carrier := ⋂ t ∈ s, ↑t,
   one_mem' := set.mem_bInter $ λ i h, i.one_mem,
   mul_mem' := λ x y hx hy, set.mem_bInter $ λ i h,
-    i.mul_mem (by apply set.mem_bInter_iff.1 hx i h) (by apply set.mem_bInter_iff.1 hy i h) }⟩
+    i.mul_mem (by apply set.mem_Inter₂.1 hx i h) (by apply set.mem_Inter₂.1 hy i h) }⟩
 
 @[simp, norm_cast, to_additive]
 lemma coe_Inf (S : set (submonoid M)) : ((Inf S : submonoid M) : set M) = ⋂ s ∈ S, ↑s := rfl
 
 @[to_additive]
-lemma mem_Inf {S : set (submonoid M)} {x : M} : x ∈ Inf S ↔ ∀ p ∈ S, x ∈ p := set.mem_bInter_iff
+lemma mem_Inf {S : set (submonoid M)} {x : M} : x ∈ Inf S ↔ ∀ p ∈ S, x ∈ p := set.mem_Inter₂
 
 @[to_additive]
 lemma mem_infi {ι : Sort*} {S : ι → submonoid M} {x : M} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i :=

src/linear_algebra/affine_space/affine_subspace.lean

@@ -546,10 +546,10 @@ instance : complete_lattice (affine_subspace k P) :=
   bot_le := λ _ _, false.elim,
   Sup := λ s, affine_span k (⋃ s' ∈ s, (s' : set P)),
   Inf := λ s, mk (⋂ s' ∈ s, (s' : set P))
-                 (λ c p1 p2 p3 hp1 hp2 hp3, set.mem_bInter_iff.2 $ λ s2 hs2,
-                   s2.smul_vsub_vadd_mem c (set.mem_bInter_iff.1 hp1 s2 hs2)
-                                           (set.mem_bInter_iff.1 hp2 s2 hs2)
-                                           (set.mem_bInter_iff.1 hp3 s2 hs2)),
+                 (λ c p1 p2 p3 hp1 hp2 hp3, set.mem_Inter₂.2 $ λ s2 hs2, begin
+                   rw set.mem_Inter₂ at *,
+                   exact s2.smul_vsub_vadd_mem c (hp1 s2 hs2) (hp2 s2 hs2) (hp3 s2 hs2)
+                 end),
   le_Sup := λ _ _ h, set.subset.trans (set.subset_bUnion_of_mem h) (subset_span_points k _),
   Sup_le := λ _ _ h, span_points_subset_coe_of_subset_coe (set.bUnion_subset h),
   Inf_le := λ _ _, set.bInter_subset_of_mem,

src/linear_algebra/basic.lean

@@ -792,8 +792,7 @@ def span (s : set M) : submodule R M := Inf {p | s ⊆ p}
 end
 
 variables {s t : set M}
-lemma mem_span : x ∈ span R s ↔ ∀ p : submodule R M, s ⊆ p → x ∈ p :=
-mem_bInter_iff
+lemma mem_span : x ∈ span R s ↔ ∀ p : submodule R M, s ⊆ p → x ∈ p := mem_Inter₂
 
 lemma subset_span : s ⊆ span R s :=
 λ x h, mem_span.2 $ λ p hp, hp h

src/measure_theory/constructions/borel_space.lean

@@ -431,8 +431,8 @@ begin
   { refine set.finite_of_forall_between_eq_endpoints (s \ u) (λ x hx y hy z hz hxy hyz, _),
     by_contra h,
     push_neg at h,
-    exact hy.2 (mem_bUnion_iff.mpr ⟨x, hx.1,
-      mem_bUnion_iff.mpr ⟨z, hz.1, lt_of_le_of_ne hxy h.1, lt_of_le_of_ne hyz h.2⟩⟩) },
+    exact hy.2 (mem_Union₂.mpr ⟨x, hx.1,
+      mem_Union₂.mpr ⟨z, hz.1, lt_of_le_of_ne hxy h.1, lt_of_le_of_ne hyz h.2⟩⟩) },
   have : u ⊆ s :=
     bUnion_subset (λ x hx, bUnion_subset (λ y hy, Ioo_subset_Icc_self.trans (h.out hx hy))),
   rw ← union_diff_cancel this,

src/measure_theory/covering/besicovitch.lean

@@ -994,15 +994,15 @@ begin
       { have A : x ∈ range q.c, by simpa only [not_exists, exists_prop, mem_Union, mem_closed_ball,
           not_and, not_le, mem_set_of_eq, subtype.range_coe_subtype, mem_diff] using h'x,
         simpa only [mem_Union, mem_image] using hS A },
-      refine mem_bUnion_iff.2 ⟨y, or.inr _, _⟩,
+      refine mem_Union₂.2 ⟨y, or.inr _, _⟩,
       { simp only [mem_Union, mem_image],
         exact ⟨i, y, ySi, rfl⟩ },
       { have : (y : α) ∈ s' := y.2,
         simp only [r, if_pos this],
         exact ball_subset_closed_ball xy } },
     { obtain ⟨y, yt0, hxy⟩ : ∃ (y : α), y ∈ t0 ∧ x ∈ closed_ball y (r0 y),
         by simpa [hx, -mem_closed_ball] using h'x,
-      refine mem_bUnion_iff.2 ⟨y, or.inl yt0, _⟩,
+      refine mem_Union₂.2 ⟨y, or.inl yt0, _⟩,
       rwa r_t0 _ yt0 } },
   -- the only nontrivial property is the measure control, which we check now
   { -- the sets in the first step have measure at most `μ s + ε / 2`

src/measure_theory/covering/vitali.lean

@@ -466,20 +466,20 @@ protected def vitali_family [metric_space α] [measurable_space α] [opens_measu
       exact ⟨a, mem_bUnion xs xa, (fsubset x xs xa).1, hax⟩ },
     have A₂ : ∀ a ∈ t, (interior a).nonempty,
     { rintros a ha,
-      rcases mem_bUnion_iff.1 ha with ⟨x, xs, xa⟩,
+      rcases mem_Union₂.1 ha with ⟨x, xs, xa⟩,
       exact (fsubset x xs xa).2.2.1 },
     have A₃ : ∀ a ∈ t, is_closed a,
     { rintros a ha,
-      rcases mem_bUnion_iff.1 ha with ⟨x, xs, xa⟩,
+      rcases mem_Union₂.1 ha with ⟨x, xs, xa⟩,
       exact (fsubset x xs xa).2.1 },
     have A₄ : ∀ a ∈ t, ∃ x ∈ a, μ (closed_ball x (3 * diam a)) ≤ C * μ a,
     { rintros a ha,
-      rcases mem_bUnion_iff.1 ha with ⟨x, xs, xa⟩,
+      rcases mem_Union₂.1 ha with ⟨x, xs, xa⟩,
       exact ⟨x, (fsubset x xs xa).1, (fsubset x xs xa).2.2.2⟩ },
     obtain ⟨u, ut, u_count, u_disj, μu⟩ :
       ∃ u ⊆ t, u.countable ∧ u.pairwise disjoint ∧ μ (s \ ⋃ a ∈ u, a) = 0 :=
         exists_disjoint_covering_ae μ s t A₁ A₂ A₃ C A₄,
-    have : ∀ a ∈ u, ∃ x ∈ s, a ∈ f x := λ a ha, mem_bUnion_iff.1 (ut ha),
+    have : ∀ a ∈ u, ∃ x ∈ s, a ∈ f x := λ a ha, mem_Union₂.1 (ut ha),
     choose! x hx using this,
     have inj_on_x : inj_on x u,
     { assume a ha b hb hab,

src/model_theory/basic.lean

@@ -457,8 +457,7 @@ instance : has_Inf (L.substructure M) :=
 lemma coe_Inf (S : set (L.substructure M)) :
   ((Inf S : L.substructure M) : set M) = ⋂ s ∈ S, ↑s := rfl
 
-lemma mem_Inf {S : set (L.substructure M)} {x : M} : x ∈ Inf S ↔ ∀ p ∈ S, x ∈ p :=
-  set.mem_bInter_iff
+lemma mem_Inf {S : set (L.substructure M)} {x : M} : x ∈ Inf S ↔ ∀ p ∈ S, x ∈ p := set.mem_Inter₂
 
 lemma mem_infi {ι : Sort*} {S : ι → L.substructure M} {x : M} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i :=
 by simp only [infi, mem_Inf, set.forall_range_iff]

src/order/filter/basic.lean

@@ -401,7 +401,7 @@ instance : complete_lattice (filter α) := original_complete_lattice.copy
                            (@inf_le_right (filter α) _ _ _ _ hb)
        end)
   end
-  /- Sup -/ (join ∘ 𝓟) (by { ext s x, exact (@mem_bInter_iff _ _ s filter.sets x).symm.trans
+  /- Sup -/ (join ∘ 𝓟) (by { ext s x, exact mem_Inter₂.symm.trans
     (set.ext_iff.1 (sInter_image _ _) x).symm})
   /- Inf -/ _ rfl
 

src/order/ideal.lean

@@ -372,13 +372,13 @@ instance : has_Inf (ideal P) :=
     begin
       simp only [←hS, sup_mem_iff, mem_coe, set.mem_Inter],
       intro hI,
-      rw set.mem_bInter_iff at *,
+      rw set.mem_Inter₂ at *,
       exact ⟨hx _ hI, hy _ hI⟩
     end,
     le_sup_left, le_sup_right⟩⟩,
   mem_of_le := λ x y hxy hy,
     begin
-      rw set.mem_bInter_iff at *,
+      rw set.mem_Inter₂ at *,
       exact λ I hI, mem_of_le I ‹_› (hy I hI)
     end } }
 

src/ring_theory/finiteness.lean

@@ -660,7 +660,7 @@ begin
   have hincl : of' R M '' f.support ⊆
     ⋃ (g : add_monoid_algebra R M) (H : g ∈ S), of' R M '' g.support,
   { intros s hs,
-    exact set.mem_bUnion_iff.2 ⟨f, ⟨hf, hs⟩⟩ },
+    exact set.mem_Union₂.2 ⟨f, ⟨hf, hs⟩⟩ },
   exact adjoin_mono hincl (mem_adjoin_support f)
 end
 
@@ -816,7 +816,7 @@ begin
   have hincl : (of R M) '' f.support ⊆
     ⋃ (g : monoid_algebra R M) (H : g ∈ S), of R M '' g.support,
   { intros s hs,
-    exact set.mem_bUnion_iff.2 ⟨f, ⟨hf, hs⟩⟩ },
+    exact set.mem_Union₂.2 ⟨f, ⟨hf, hs⟩⟩ },
   exact adjoin_mono hincl (mem_adjoint_support f)
 end