chore(data/finset): Rename bind to bUnion (#5813)

This commit renames `finset.bind` to `finset.bUnion`.  While this is the monadic bind operation, conceptually it's doing a bounded union of an indexed family of finite sets.  This will help with discoverability of this function.

There was a name conflict in `data.finset.lattice` due to this, since there are a number of theorems about the `set` version of `bUnion`, and for these I prefixed the lemmas with `set_`.

src/algebra/big_operators/basic.lean

@@ -231,28 +231,28 @@ begin
 end
 
 @[to_additive]
-lemma prod_bind [decidable_eq α] {s : finset γ} {t : γ → finset α} :
+lemma prod_bUnion [decidable_eq α] {s : finset γ} {t : γ → finset α} :
   (∀ x ∈ s, ∀ y ∈ s, x ≠ y → disjoint (t x) (t y)) →
-  (∏ x in (s.bind t), f x) = ∏ x in s, ∏ i in t x, f i :=
+  (∏ x in (s.bUnion t), f x) = ∏ x in s, ∏ i in t x, f i :=
 by haveI := classical.dec_eq γ; exact
-finset.induction_on s (λ _, by simp only [bind_empty, prod_empty])
+finset.induction_on s (λ _, by simp only [bUnion_empty, prod_empty])
   (assume x s hxs ih hd,
   have hd' : ∀x∈s, ∀y∈s, x ≠ y → disjoint (t x) (t y),
     from assume _ hx _ hy, hd _ (mem_insert_of_mem hx) _ (mem_insert_of_mem hy),
   have ∀y∈s, x ≠ y,
     from assume _ hy h, by rw [←h] at hy; contradiction,
   have ∀y∈s, disjoint (t x) (t y),
     from assume _ hy, hd _ (mem_insert_self _ _) _ (mem_insert_of_mem hy) (this _ hy),
-  have disjoint (t x) (finset.bind s t),
-    from (disjoint_bind_right _ _ _).mpr this,
-  by simp only [bind_insert, prod_insert hxs, prod_union this, ih hd'])
+  have disjoint (t x) (finset.bUnion s t),
+    from (disjoint_bUnion_right _ _ _).mpr this,
+  by simp only [bUnion_insert, prod_insert hxs, prod_union this, ih hd'])
 
 @[to_additive]
 lemma prod_product {s : finset γ} {t : finset α} {f : γ×α → β} :
   (∏ x in s.product t, f x) = ∏ x in s, ∏ y in t, f (x, y) :=
 begin
   haveI := classical.dec_eq α, haveI := classical.dec_eq γ,
-  rw [product_eq_bind, prod_bind],
+  rw [product_eq_bUnion, prod_bUnion],
   { congr, funext, exact prod_image (λ _ _ _ _ H, (prod.mk.inj H).2) },
   simp only [disjoint_iff_ne, mem_image],
   rintros _ _ _ _ h ⟨_, _⟩ ⟨_, _, ⟨_, _⟩⟩ ⟨_, _⟩ ⟨_, _, ⟨_, _⟩⟩ _,
@@ -274,9 +274,9 @@ lemma prod_sigma {σ : α → Type*}
   (∏ x in s.sigma t, f x) = ∏ a in s, ∏ s in (t a), f ⟨a, s⟩ :=
 by classical;
 calc (∏ x in s.sigma t, f x) =
-       ∏ x in s.bind (λa, (t a).map (function.embedding.sigma_mk a)), f x : by rw sigma_eq_bind
+       ∏ x in s.bUnion (λa, (t a).map (function.embedding.sigma_mk a)), f x : by rw sigma_eq_bUnion
   ... = ∏ a in s, ∏ x in (t a).map (function.embedding.sigma_mk a), f x :
-    prod_bind $ assume a₁ ha a₂ ha₂ h x hx,
+    prod_bUnion $ assume a₁ ha a₂ ha₂ h x hx,
     by { simp only [inf_eq_inter, mem_inter, mem_map, function.embedding.sigma_mk_apply] at hx,
       rcases hx with ⟨⟨y, hy, rfl⟩, ⟨z, hz, hz'⟩⟩, cc }
   ... = ∏ a in s, ∏ s in t a, f ⟨a, s⟩ :
@@ -294,8 +294,8 @@ lemma prod_fiberwise_of_maps_to [decidable_eq γ] {s : finset α} {t : finset γ
   (∏ y in t, ∏ x in s.filter (λ x, g x = y), f x) = ∏ x in s, f x :=
 begin
   letI := classical.dec_eq α,
-  rw [← bind_filter_eq_of_maps_to h] {occs := occurrences.pos [2]},
-  refine (prod_bind $ λ x' hx y' hy hne, _).symm,
+  rw [← bUnion_filter_eq_of_maps_to h] {occs := occurrences.pos [2]},
+  refine (prod_bUnion $ λ x' hx y' hy hne, _).symm,
   rw [disjoint_filter],
   rintros x hx rfl,
   exact hne
@@ -1031,20 +1031,20 @@ end comm_group
   card (s.sigma t) = ∑ a in s, card (t a) :=
 multiset.card_sigma _ _
 
-lemma card_bind [decidable_eq β] {s : finset α} {t : α → finset β}
+lemma card_bUnion [decidable_eq β] {s : finset α} {t : α → finset β}
   (h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → disjoint (t x) (t y)) :
-  (s.bind t).card = ∑ u in s, card (t u) :=
-calc (s.bind t).card = ∑ i in s.bind t, 1 : by simp
-... = ∑ a in s, ∑ i in t a, 1 : finset.sum_bind h
+  (s.bUnion t).card = ∑ u in s, card (t u) :=
+calc (s.bUnion t).card = ∑ i in s.bUnion t, 1 : by simp
+... = ∑ a in s, ∑ i in t a, 1 : finset.sum_bUnion h
 ... = ∑ u in s, card (t u) : by simp
 
-lemma card_bind_le [decidable_eq β] {s : finset α} {t : α → finset β} :
-  (s.bind t).card ≤ ∑ a in s, (t a).card :=
+lemma card_bUnion_le [decidable_eq β] {s : finset α} {t : α → finset β} :
+  (s.bUnion t).card ≤ ∑ a in s, (t a).card :=
 by haveI := classical.dec_eq α; exact
 finset.induction_on s (by simp)
   (λ a s has ih,
-    calc ((insert a s).bind t).card ≤ (t a).card + (s.bind t).card :
-    by rw bind_insert; exact finset.card_union_le _ _
+    calc ((insert a s).bUnion t).card ≤ (t a).card + (s.bUnion t).card :
+    by rw bUnion_insert; exact finset.card_union_le _ _
     ... ≤ ∑ a in insert a s, card (t a) :
     by rw sum_insert has; exact add_le_add_left ih _)
 

src/algebra/big_operators/ring.lean

@@ -69,7 +69,7 @@ begin
       { rw [eq₂, eq₃, eq] },
       rw [pi.cons_same, pi.cons_same] at this,
       exact h this },
-    rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_bind h₁],
+    rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_bUnion h₁],
     refine sum_congr rfl (λ b _, _),
     have h₂ : ∀p₁∈pi s t, ∀p₂∈pi s t, pi.cons s a b p₁ = pi.cons s a b p₂ → p₁ = p₂, from
       assume p₁ h₁ p₂ h₂ eq, pi_cons_injective ha eq,

src/algebra/monoid_algebra.lean

@@ -217,9 +217,9 @@ calc (f * g) x = (∑ a₁ in f.support, ∑ a₂ in g.support, F (a₁, a₂))
   end
 
 lemma support_mul (a b : monoid_algebra k G) :
-  (a * b).support ⊆ a.support.bind (λa₁, b.support.bind $ λa₂, {a₁ * a₂}) :=
-subset.trans support_sum $ bind_mono $ assume a₁ _,
-  subset.trans support_sum $ bind_mono $ assume a₂ _, support_single_subset
+  (a * b).support ⊆ a.support.bUnion (λa₁, b.support.bUnion $ λa₂, {a₁ * a₂}) :=
+subset.trans support_sum $ bUnion_mono $ assume a₁ _,
+  subset.trans support_sum $ bUnion_mono $ assume a₂ _, support_single_subset
 
 @[simp] lemma single_mul_single {a₁ a₂ : G} {b₁ b₂ : k} :
   (single a₁ b₁ : monoid_algebra k G) * single a₂ b₂ = single (a₁ * a₂) (b₁ * b₂) :=
@@ -696,7 +696,7 @@ lemma mul_apply_antidiagonal (f g : add_monoid_algebra k G) (x : G) (s : finset
 @monoid_algebra.mul_apply_antidiagonal k (multiplicative G) _ _ _ _ _ s @hs
 
 lemma support_mul (a b : add_monoid_algebra k G) :
-  (a * b).support ⊆ a.support.bind (λa₁, b.support.bind $ λa₂, {a₁ + a₂}) :=
+  (a * b).support ⊆ a.support.bUnion (λa₁, b.support.bUnion $ λa₂, {a₁ + a₂}) :=
 @monoid_algebra.support_mul k (multiplicative G) _ _ _ _
 
 lemma single_mul_single {a₁ a₂ : G} {b₁ b₂ : k} :

src/category_theory/filtered.lean

@@ -216,15 +216,15 @@ begin
   classical,
   let O := (finset.univ.image F.obj),
   let H : finset (Σ' (X Y : C) (mX : X ∈ O) (mY : Y ∈ O), X ⟶ Y) :=
-    finset.univ.bind (λ X : J, finset.univ.bind (λ Y : J, finset.univ.image (λ f : X ⟶ Y,
+    finset.univ.bUnion (λ X : J, finset.univ.bUnion (λ Y : J, finset.univ.image (λ f : X ⟶ Y,
       ⟨F.obj X, F.obj Y, by simp, by simp, F.map f⟩))),
   obtain ⟨Z, f, w⟩ := sup_exists O H,
   refine ⟨⟨Z, ⟨λ X, f (by simp), _⟩⟩⟩,
   intros j j' g,
   dsimp,
   simp only [category.comp_id],
   apply w,
-  simp only [finset.mem_univ, finset.mem_bind, exists_and_distrib_left,
+  simp only [finset.mem_univ, finset.mem_bUnion, exists_and_distrib_left,
     exists_prop_of_true, finset.mem_image],
   exact ⟨j, rfl, j', g, (by simp)⟩,
 end

src/category_theory/limits/filtered_colimit_commutes_finite_limit.lean

@@ -203,20 +203,20 @@ begin
   -- picking some place to the right of all of
   -- the morphisms `gf f : k' ⟶ kh f` and `hf f : k' ⟶ kf f`.
   -- At this point we're relying on there being only finitely morphisms in `J`.
-  let O := finset.univ.bind (λ j, finset.univ.bind (λ j', finset.univ.image (@kf j j'))) ∪ {k'},
+  let O := finset.univ.bUnion (λ j, finset.univ.bUnion (λ j', finset.univ.image (@kf j j'))) ∪ {k'},
   have kfO : ∀ {j j'} (f : j ⟶ j'), kf f ∈ O := λ j j' f, finset.mem_union.mpr (or.inl (
   begin
-    rw [finset.mem_bind],
+    rw [finset.mem_bUnion],
     refine ⟨j, finset.mem_univ j, _⟩,
-    rw [finset.mem_bind],
+    rw [finset.mem_bUnion],
     refine ⟨j', finset.mem_univ j', _⟩,
     rw [finset.mem_image],
     refine ⟨f, finset.mem_univ _, _⟩,
     refl,
   end)),
   have k'O : k' ∈ O := finset.mem_union.mpr (or.inr (finset.mem_singleton.mpr rfl)),
   let H : finset (Σ' (X Y : K) (mX : X ∈ O) (mY : Y ∈ O), X ⟶ Y) :=
-    finset.univ.bind (λ j : J, finset.univ.bind (λ j' : J, finset.univ.bind (λ f : j ⟶ j',
+    finset.univ.bUnion (λ j : J, finset.univ.bUnion (λ j' : J, finset.univ.bUnion (λ f : j ⟶ j',
       {⟨k', kf f, k'O, kfO f, gf f⟩, ⟨k', kf f, k'O, kfO f, hf f⟩}))),
 
   obtain ⟨k'', i', s'⟩ := is_filtered.sup_exists O H,
@@ -230,18 +230,18 @@ begin
     swap 2,
     exact k'O,
     swap 2,
-    { rw [finset.mem_bind],
+    { rw [finset.mem_bUnion],
       refine ⟨j₁, finset.mem_univ _, _⟩,
-      rw [finset.mem_bind],
+      rw [finset.mem_bUnion],
       refine ⟨j₂, finset.mem_univ _, _⟩,
-      rw [finset.mem_bind],
+      rw [finset.mem_bUnion],
       refine ⟨f, finset.mem_univ _, _⟩,
       simp only [true_or, eq_self_iff_true, and_self, finset.mem_insert, heq_iff_eq], },
-    { rw [finset.mem_bind],
+    { rw [finset.mem_bUnion],
       refine ⟨j₃, finset.mem_univ _, _⟩,
-      rw [finset.mem_bind],
+      rw [finset.mem_bUnion],
       refine ⟨j₄, finset.mem_univ _, _⟩,
-      rw [finset.mem_bind],
+      rw [finset.mem_bUnion],
       refine ⟨f', finset.mem_univ _, _⟩,
       simp only [eq_self_iff_true, or_true, and_self, finset.mem_insert, finset.mem_singleton,
         heq_iff_eq], }

src/computability/turing_machine.lean

@@ -1134,11 +1134,11 @@ end
 /-- The set of all statements in a turing machine, plus one extra value `none` representing the
 halt state. This is used in the TM1 to TM0 reduction. -/
 noncomputable def stmts (M : Λ → stmt) (S : finset Λ) : finset (option stmt) :=
-(S.bind (λ q, stmts₁ (M q))).insert_none
+(S.bUnion (λ q, stmts₁ (M q))).insert_none
 
 theorem stmts_trans {M : Λ → stmt} {S q₁ q₂}
   (h₁ : q₁ ∈ stmts₁ q₂) : some q₂ ∈ stmts M S → some q₁ ∈ stmts M S :=
-by simp only [stmts, finset.mem_insert_none, finset.mem_bind,
+by simp only [stmts, finset.mem_insert_none, finset.mem_bUnion,
   option.mem_def, forall_eq', exists_imp_distrib];
 exact λ l ls h₂, ⟨_, ls, stmts₁_trans h₂ h₁⟩
 
@@ -1152,7 +1152,7 @@ default Λ ∈ S ∧ ∀ q ∈ S, supports_stmt S (M q)
 
 theorem stmts_supports_stmt {M : Λ → stmt} {S q}
   (ss : supports M S) : some q ∈ stmts M S → supports_stmt S q :=
-by simp only [stmts, finset.mem_insert_none, finset.mem_bind,
+by simp only [stmts, finset.mem_insert_none, finset.mem_bUnion,
   option.mem_def, forall_eq', exists_imp_distrib];
 exact λ l ls h, stmts₁_supports_stmt_mono h (ss.2 _ ls)
 
@@ -1292,7 +1292,7 @@ local attribute [simp] TM1.stmts₁_self
 theorem tr_supports {S : finset Λ} (ss : TM1.supports M S) :
   TM0.supports tr (↑(tr_stmts S)) :=
 ⟨finset.mem_product.2 ⟨finset.some_mem_insert_none.2
-  (finset.mem_bind.2 ⟨_, ss.1, TM1.stmts₁_self⟩),
+  (finset.mem_bUnion.2 ⟨_, ss.1, TM1.stmts₁_self⟩),
   finset.mem_univ _⟩,
  λ q a q' s h₁ h₂, begin
   rcases q with ⟨_|q, v⟩, {cases h₁},
@@ -1325,7 +1325,7 @@ theorem tr_supports {S : finset Λ} (ss : TM1.supports M S) :
       exact finset.mem_insert_of_mem (finset.mem_union_left _ TM1.stmts₁_self) } },
   case TM1.stmt.goto : l {
     cases h₁, exact finset.some_mem_insert_none.2
-      (finset.mem_bind.2 ⟨_, hs _ _, TM1.stmts₁_self⟩) },
+      (finset.mem_bUnion.2 ⟨_, hs _ _, TM1.stmts₁_self⟩) },
   case TM1.stmt.halt { cases h₁ }
 end⟩
 
@@ -1629,19 +1629,19 @@ noncomputable def writes : stmt₁ → finset Λ'
 /-- The set of accessible machine states, assuming that the input machine is supported on `S`,
 are the normal states embedded from `S`, plus all write states accessible from these states. -/
 noncomputable def tr_supp (S : finset Λ) : finset Λ' :=
-S.bind (λ l, insert (Λ'.normal l) (writes (M l)))
+S.bUnion (λ l, insert (Λ'.normal l) (writes (M l)))
 
 theorem tr_supports {S} (ss : supports M S) :
   supports tr (tr_supp S) :=
-⟨finset.mem_bind.2 ⟨_, ss.1, finset.mem_insert_self _ _⟩,
+⟨finset.mem_bUnion.2 ⟨_, ss.1, finset.mem_insert_self _ _⟩,
 λ q h, begin
   suffices : ∀ q, supports_stmt S q →
     (∀ q' ∈ writes q, q' ∈ tr_supp M S) →
     supports_stmt (tr_supp M S) (tr_normal dec q) ∧
     ∀ q' ∈ writes q, supports_stmt (tr_supp M S) (tr enc dec M q'),
-  { rcases finset.mem_bind.1 h with ⟨l, hl, h⟩,
+  { rcases finset.mem_bUnion.1 h with ⟨l, hl, h⟩,
     have := this _ (ss.2 _ hl) (λ q' hq,
-      finset.mem_bind.2 ⟨_, hl, finset.mem_insert_of_mem hq⟩),
+      finset.mem_bUnion.2 ⟨_, hl, finset.mem_insert_of_mem hq⟩),
     rcases finset.mem_insert.1 h with rfl | h,
     exacts [this.1, this.2 _ h] },
   intros q hs hw, induction q,
@@ -1673,7 +1673,7 @@ theorem tr_supports {S} (ss : supports M S) :
   case TM1.stmt.goto : l {
     refine ⟨_, λ _, false.elim⟩,
     refine supports_stmt_read _ (λ a _ s, _),
-    exact finset.mem_bind.2 ⟨_, hs _ _, finset.mem_insert_self _ _⟩ },
+    exact finset.mem_bUnion.2 ⟨_, hs _ _, finset.mem_insert_self _ _⟩ },
   case TM1.stmt.halt {
     refine ⟨_, λ _, false.elim⟩,
     simp only [supports_stmt, supports_stmt_move, tr_normal] }
@@ -1903,11 +1903,11 @@ end
 
 /-- The set of statements accessible from initial set `S` of labels. -/
 noncomputable def stmts (M : Λ → stmt) (S : finset Λ) : finset (option stmt) :=
-(S.bind (λ q, stmts₁ (M q))).insert_none
+(S.bUnion (λ q, stmts₁ (M q))).insert_none
 
 theorem stmts_trans {M : Λ → stmt} {S q₁ q₂}
   (h₁ : q₁ ∈ stmts₁ q₂) : some q₂ ∈ stmts M S → some q₁ ∈ stmts M S :=
-by simp only [stmts, finset.mem_insert_none, finset.mem_bind,
+by simp only [stmts, finset.mem_insert_none, finset.mem_bUnion,
   option.mem_def, forall_eq', exists_imp_distrib];
 exact λ l ls h₂, ⟨_, ls, stmts₁_trans h₂ h₁⟩
 
@@ -1920,7 +1920,7 @@ default Λ ∈ S ∧ ∀ q ∈ S, supports_stmt S (M q)
 
 theorem stmts_supports_stmt {M : Λ → stmt} {S q}
   (ss : supports M S) : some q ∈ stmts M S → supports_stmt S q :=
-by simp only [stmts, finset.mem_insert_none, finset.mem_bind,
+by simp only [stmts, finset.mem_insert_none, finset.mem_bUnion,
   option.mem_def, forall_eq', exists_imp_distrib];
 exact λ l ls h, stmts₁_supports_stmt_mono h (ss.2 _ ls)
 
@@ -2384,19 +2384,19 @@ end
 
 /-- The support of a set of TM2 states in the TM2 emulator. -/
 noncomputable def tr_supp (S : finset Λ) : finset Λ' :=
-S.bind (λ l, insert (normal l) (tr_stmts₁ (M l)))
+S.bUnion (λ l, insert (normal l) (tr_stmts₁ (M l)))
 
 theorem tr_supports {S} (ss : TM2.supports M S) :
   TM1.supports tr (tr_supp S) :=
-⟨finset.mem_bind.2 ⟨_, ss.1, finset.mem_insert.2 $ or.inl rfl⟩,
+⟨finset.mem_bUnion.2 ⟨_, ss.1, finset.mem_insert.2 $ or.inl rfl⟩,
 λ l' h, begin
   suffices : ∀ q (ss' : TM2.supports_stmt S q)
     (sub : ∀ x ∈ tr_stmts₁ q, x ∈ tr_supp M S),
     TM1.supports_stmt (tr_supp M S) (tr_normal q) ∧
     (∀ l' ∈ tr_stmts₁ q, TM1.supports_stmt (tr_supp M S) (tr M l')),
-  { rcases finset.mem_bind.1 h with ⟨l, lS, h⟩,
+  { rcases finset.mem_bUnion.1 h with ⟨l, lS, h⟩,
     have := this _ (ss.2 l lS) (λ x hx,
-      finset.mem_bind.2 ⟨_, lS, finset.mem_insert_of_mem hx⟩),
+      finset.mem_bUnion.2 ⟨_, lS, finset.mem_insert_of_mem hx⟩),
     rcases finset.mem_insert.1 h with rfl | h;
     [exact this.1, exact this.2 _ h] },
   clear h l', refine stmt_st_rec _ _ _ _ _; intros,
@@ -2434,7 +2434,7 @@ theorem tr_supports {S} (ss : TM2.supports M S) :
   { -- goto
     rw tr_stmts₁, unfold TM2to1.tr_normal TM1.supports_stmt,
     unfold TM2.supports_stmt at ss',
-    exact ⟨λ _ v, finset.mem_bind.2 ⟨_, ss' v, finset.mem_insert_self _ _⟩, λ _, false.elim⟩ },
+    exact ⟨λ _ v, finset.mem_bUnion.2 ⟨_, ss' v, finset.mem_insert_self _ _⟩, λ _, false.elim⟩ },
   { exact ⟨trivial, λ _, false.elim⟩ } -- halt
 end⟩
 

src/data/dfinsupp.lean

@@ -742,13 +742,13 @@ lemma support_sum {ι₁ : Type u₁} [decidable_eq ι₁] {β₁ : ι₁ → Ty
   [Π i₁, has_zero (β₁ i₁)] [Π i (x : β₁ i), decidable (x ≠ 0)]
   [Π i, add_comm_monoid (β i)] [Π i (x : β i), decidable (x ≠ 0)]
   {f : Π₀ i₁, β₁ i₁} {g : Π i₁, β₁ i₁ → Π₀ i, β i} :
-  (f.sum g).support ⊆ f.support.bind (λi, (g i (f i)).support) :=
+  (f.sum g).support ⊆ f.support.bUnion (λi, (g i (f i)).support) :=
 have ∀i₁ : ι, f.sum (λ (i : ι₁) (b : β₁ i), (g i b) i₁) ≠ 0 →
     (∃ (i : ι₁), f i ≠ 0 ∧ ¬ (g i (f i)) i₁ = 0),
   from assume i₁ h,
   let ⟨i, hi, ne⟩ := finset.exists_ne_zero_of_sum_ne_zero h in
   ⟨i, (f.mem_support_iff i).mp hi, ne⟩,
-by simpa [finset.subset_iff, mem_support_iff, finset.mem_bind, sum_apply] using this
+by simpa [finset.subset_iff, mem_support_iff, finset.mem_bUnion, sum_apply] using this
 
 @[simp, to_additive] lemma prod_one [Π i, add_comm_monoid (β i)] [Π i (x : β i), decidable (x ≠ 0)]
   [comm_monoid γ] {f : Π₀ i, β i} :