chore(algebra/big_operators/basic): golf results about bUnion (#17501)

While the diff adds lines overall, these are new lemmas that were previously missing.

src/algebra/big_operators/basic.lean

@@ -368,16 +368,8 @@ by simp
 @[to_additive]
 lemma prod_bUnion [decidable_eq α] {s : finset γ} {t : γ → finset α}
   (hs : set.pairwise_disjoint ↑s t) :
-  (∏ x in (s.bUnion t), f x) = ∏ x in s, ∏ i in t x, f i :=
-begin
-  haveI := classical.dec_eq γ,
-  induction s using finset.induction_on with x s hxs ih hd,
-  { simp_rw [bUnion_empty, prod_empty] },
-  { simp_rw [coe_insert, set.pairwise_disjoint_insert, mem_coe] at hs,
-    have : disjoint (t x) (finset.bUnion s t),
-    { exact (disjoint_bUnion_right _ _ _).mpr (λ y hy, hs.2 y hy $ λ H, hxs $ H.substr hy) },
-    rw [bUnion_insert, prod_insert hxs, prod_union this, ih hs.1] }
-end
+  (∏ x in s.bUnion t, f x) = ∏ x in s, ∏ i in t x, f i :=
+by rw [←disj_Union_eq_bUnion _ _ hs, prod_disj_Union]
 
 /-- Product over a sigma type equals the product of fiberwise products. For rewriting
 in the reverse direction, use `finset.prod_sigma'`.  -/
@@ -386,16 +378,7 @@ in the reverse direction, use `finset.sum_sigma'`"]
 lemma prod_sigma {σ : α → Type*}
   (s : finset α) (t : Π a, finset (σ a)) (f : sigma σ → β) :
   (∏ 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.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_bUnion $ λ a₁ ha a₂ ha₂ h, disjoint_left.mpr $
-      by { simp_rw [mem_map, function.embedding.sigma_mk_apply],
-           rintros _ ⟨y, hy, rfl⟩ ⟨z, hz, hz'⟩,
-           exact h (congr_arg sigma.fst hz'.symm) }
-  ... = ∏ a in s, ∏ s in t a, f ⟨a, s⟩ :
-    prod_congr rfl $ λ _ _, prod_map _ _ _
+by simp_rw [←disj_Union_map_sigma_mk, prod_disj_Union, prod_map, function.embedding.sigma_mk_apply]
 
 @[to_additive]
 lemma prod_sigma' {σ : α → Type*}
@@ -501,12 +484,8 @@ lemma prod_fiberwise_of_maps_to [decidable_eq γ] {s : finset α} {t : finset γ
   (h : ∀ x ∈ s, g x ∈ t) (f : α → β) :
   (∏ y in t, ∏ x in s.filter (λ x, g x = y), f x) = ∏ x in s, f x :=
 begin
-  letI := classical.dec_eq α,
-  rw [← bUnion_filter_eq_of_maps_to h] {occs := occurrences.pos [2]},
-  refine (prod_bUnion $ λ x' hx y' hy hne, _).symm,
-  rw [function.on_fun, disjoint_filter],
-  rintros x hx rfl,
-  exact hne
+  rw [← disj_Union_filter_eq_of_maps_to h] {occs := occurrences.pos [2]},
+  rw prod_disj_Union,
 end
 
 @[to_additive]
@@ -1731,7 +1710,8 @@ lemma sup_powerset_len {α : Type*} [decidable_eq α] (x : multiset α) :
 begin
   convert bind_powerset_len x,
   rw [multiset.bind, multiset.join, ←finset.range_coe, ←finset.sum_eq_multiset_sum],
-  exact eq.symm (finset_sum_eq_sup_iff_disjoint.mpr (λ _ _ _ _ h, disjoint_powerset_len x h)),
+  exact eq.symm (finset_sum_eq_sup_iff_disjoint.mpr
+    (λ _ _ _ _ h, pairwise_disjoint_powerset_len x h)),
 end
 
 @[simp] lemma to_finset_sum_count_eq (s : multiset α) :

src/algebra/big_operators/ring.lean

@@ -249,15 +249,7 @@ end
 `card s = k`, for `k = 1, ..., card s`"]
 lemma prod_powerset [comm_monoid β] (s : finset α) (f : finset α → β) :
   ∏ t in powerset s, f t = ∏ j in range (card s + 1), ∏ t in powerset_len j s, f t :=
-begin
-  classical,
-  rw [powerset_card_bUnion, prod_bUnion],
-  intros i hi j hj hij,
-  rw [function.on_fun, powerset_len_eq_filter, powerset_len_eq_filter, disjoint_filter],
-  intros x hx hc hnc,
-  apply hij,
-  rwa ← hc,
-end
+by rw [powerset_card_disj_Union, prod_disj_Union]
 
 lemma sum_range_succ_mul_sum_range_succ [non_unital_non_assoc_semiring β] (n k : ℕ) (f g : ℕ → β) :
   (∑ i in range (n+1), f i) * (∑ i in range (k+1), g i) =

src/data/finset/basic.lean

@@ -2771,6 +2771,16 @@ lemma disj_Union_disj_Union (s : finset α) (f : α → finset β) (g : β → f
       end) :=
 eq_of_veq $ multiset.bind_assoc.trans (multiset.attach_bind_coe _ _).symm
 
+lemma disj_Union_filter_eq_of_maps_to [decidable_eq β] {s : finset α} {t : finset β} {f : α → β}
+  (h : ∀ x ∈ s, f x ∈ t) :
+  t.disj_Union (λ a, s.filter $ (λ c, f c = a))
+    (λ x' hx y' hy hne, disjoint_filter_filter' _ _ begin
+      simp_rw [pi.disjoint_iff, Prop.disjoint_iff],
+      rintros i ⟨rfl, rfl⟩,
+      exact hne rfl,
+    end) = s :=
+ext $ λ b, by simpa using h b
+
 end disj_Union
 
 section bUnion
@@ -2900,8 +2910,8 @@ end
 
 lemma bUnion_filter_eq_of_maps_to [decidable_eq α] {s : finset α} {t : finset β} {f : α → β}
   (h : ∀ x ∈ s, f x ∈ t) :
-  t.bUnion (λa, s.filter $ (λc, f c = a)) = s :=
-ext $ λ b, by simpa using h b
+  t.bUnion (λ a, s.filter $ (λ c, f c = a)) = s :=
+by simpa only [disj_Union_eq_bUnion] using disj_Union_filter_eq_of_maps_to h
 
 lemma image_bUnion_filter_eq [decidable_eq α] (s : finset β) (g : β → α) :
   (s.image g).bUnion (λa, s.filter $ (λc, g c = a)) = s :=

src/data/finset/powerset.lean

@@ -222,17 +222,28 @@ begin
     simp }
 end
 
-lemma powerset_card_bUnion [decidable_eq (finset α)] (s : finset α) :
-  finset.powerset s = (range (s.card + 1)).bUnion (λ i, powerset_len i s) :=
+lemma pairwise_disjoint_powerset_len (s : finset α) :
+  _root_.pairwise (λ i j, disjoint (s.powerset_len i) (s.powerset_len j)) :=
+λ i j hij, finset.disjoint_left.mpr $ λ x hi hj, hij $
+  (mem_powerset_len.mp hi).2.symm.trans (mem_powerset_len.mp hj).2
+
+lemma powerset_card_disj_Union (s : finset α) :
+  finset.powerset s =
+    (range (s.card + 1)).disj_Union (λ i, powerset_len i s)
+      (s.pairwise_disjoint_powerset_len.set_pairwise _) :=
 begin
   refine ext (λ a, ⟨λ ha, _, λ ha, _ ⟩),
-  { rw mem_bUnion,
+  { rw mem_disj_Union,
     exact ⟨a.card, mem_range.mpr (nat.lt_succ_of_le (card_le_of_subset (mem_powerset.mp ha))),
       mem_powerset_len.mpr ⟨mem_powerset.mp ha, rfl⟩⟩ },
-  { rcases mem_bUnion.mp ha with ⟨i, hi, ha⟩,
+  { rcases mem_disj_Union.mp ha with ⟨i, hi, ha⟩,
     exact mem_powerset.mpr (mem_powerset_len.mp ha).1, }
 end
 
+lemma powerset_card_bUnion [decidable_eq (finset α)] (s : finset α) :
+  finset.powerset s = (range (s.card + 1)).bUnion (λ i, powerset_len i s) :=
+by simpa only [disj_Union_eq_bUnion] using powerset_card_disj_Union s
+
 lemma powerset_len_sup [decidable_eq α] (u : finset α) (n : ℕ) (hn : n < u.card) :
   (powerset_len n.succ u).sup id = u :=
 begin

src/data/finset/sigma.lean

@@ -53,6 +53,21 @@ by simp only [← not_nonempty_iff_eq_empty, sigma_nonempty, not_exists]
 @[mono] lemma sigma_mono (hs : s₁ ⊆ s₂) (ht : ∀ i, t₁ i ⊆ t₂ i) : s₁.sigma t₁ ⊆ s₂.sigma t₂ :=
 λ ⟨i, a⟩ h, let ⟨hi, ha⟩ := mem_sigma.1 h in mem_sigma.2 ⟨hs hi, ht i ha⟩
 
+lemma pairwise_disjoint_map_sigma_mk :
+  (s : set ι).pairwise_disjoint (λ i, (t i).map (embedding.sigma_mk i)) :=
+begin
+  intros i hi j hj hij,
+  rw [function.on_fun, disjoint_left],
+  simp_rw [mem_map, function.embedding.sigma_mk_apply],
+  rintros _ ⟨y, hy, rfl⟩ ⟨z, hz, hz'⟩,
+  exact hij (congr_arg sigma.fst hz'.symm)
+end
+
+@[simp]
+lemma disj_Union_map_sigma_mk :
+  s.disj_Union (λ i, (t i).map (embedding.sigma_mk i))
+    pairwise_disjoint_map_sigma_mk = s.sigma t := rfl
+
 lemma sigma_eq_bUnion [decidable_eq (Σ i, α i)] (s : finset ι) (t : Π i, finset (α i)) :
   s.sigma t = s.bUnion (λ i, (t i).map $ embedding.sigma_mk i) :=
 by { ext ⟨x, y⟩, simp [and.left_comm] }

src/data/multiset/powerset.lean

@@ -256,9 +256,9 @@ begin
   { cases n; simp [ih, map_comp_cons], },
 end
 
-lemma disjoint_powerset_len (s : multiset α) {i j : ℕ} (h : i ≠ j) :
-  multiset.disjoint (s.powerset_len i) (s.powerset_len j) :=
-λ x hi hj, h (eq.trans (multiset.mem_powerset_len.mp hi).right.symm
+lemma pairwise_disjoint_powerset_len (s : multiset α) :
+  _root_.pairwise (λ i j, multiset.disjoint (s.powerset_len i) (s.powerset_len j)) :=
+λ i j h x hi hj, h (eq.trans (multiset.mem_powerset_len.mp hi).right.symm
   (multiset.mem_powerset_len.mp hj).right)
 
 lemma bind_powerset_len {α : Type*} (S : multiset α) :