feat(data/finset/basic): product, bUnion, sdiff lemmas (#8321)

src/data/finset/basic.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Minchao Wu, Mario Carneiro
 -/
 import data.multiset.finset_ops
-import tactic.monotonicity
 import tactic.apply
+import tactic.monotonicity
 import tactic.nth_rewrite
 
 /-!
@@ -1142,6 +1142,10 @@ end
 @[simp] lemma sdiff_subset (s t : finset α) : s \ t ⊆ s :=
 show s \ t ≤ s, from sdiff_le
 
+lemma sdiff_ssubset {s t : finset α} (h : t ⊆ s) (ht : t.nonempty) :
+  s \ t ⊂ s :=
+sdiff_lt (le_iff_subset.2 h) ht.ne_empty
+
 lemma union_sdiff_distrib (s₁ s₂ t : finset α) : (s₁ ∪ s₂) \ t = s₁ \ t ∪ s₂ \ t :=
 sup_sdiff
 
@@ -2523,6 +2527,15 @@ by haveI := classical.dec_eq α; exact
 finset.induction_on s rfl (λ a s has ih,
   by simp only [bUnion_insert, image_union, ih])
 
+lemma bUnion_bUnion [decidable_eq γ] (s : finset α) (f : α → finset β) (g : β → finset γ) :
+  (s.bUnion f).bUnion g = s.bUnion (λ a, (f a).bUnion g) :=
+begin
+  ext,
+  simp only [finset.mem_bUnion, exists_prop],
+  simp_rw [←exists_and_distrib_right, ←exists_and_distrib_left, and_assoc],
+  rw exists_comm,
+end
+
 theorem bind_to_finset [decidable_eq α] (s : multiset α) (t : α → multiset β) :
   (s.bind t).to_finset = s.to_finset.bUnion (λa, (t a).to_finset) :=
 ext $ λ x, by simp only [multiset.mem_to_finset, mem_bUnion, multiset.mem_bind, exists_prop]
@@ -2548,6 +2561,11 @@ begin
   exact subset_of_eq singleton_bUnion.symm,
 end
 
+@[simp] lemma bUnion_subset_iff_forall_subset {α β : Type*} [decidable_eq β]
+  {s : finset α} {t : finset β} {f : α → finset β} : s.bUnion f ⊆ t ↔ ∀ x ∈ s, f x ⊆ t :=
+⟨λ h x hx, (subset_bUnion_of_mem f hx).trans h,
+ λ h x hx, let ⟨a, ha₁, ha₂⟩ := mem_bUnion.mp hx in h _ ha₁ ha₂⟩
+
 lemma bUnion_singleton {f : α → β} : s.bUnion (λa, {f a}) = s.image f :=
 ext $ λ x, by simp only [mem_bUnion, mem_image, mem_singleton, eq_comm]
 
@@ -2590,6 +2608,11 @@ theorem product_eq_bUnion [decidable_eq α] [decidable_eq β] (s : finset α) (t
 ext $ λ ⟨x, y⟩, by simp only [mem_product, mem_bUnion, mem_image, exists_prop, prod.mk.inj_iff,
   and.left_comm, exists_and_distrib_left, exists_eq_right, exists_eq_left]
 
+@[simp] lemma product_bUnion {β γ : Type*} [decidable_eq γ]
+  (s : finset α) (t : finset β) (f : α × β → finset γ) :
+  (s.product t).bUnion f = s.bUnion (λ a, t.bUnion (λ b, f (a, b))) :=
+by { classical, simp_rw [product_eq_bUnion, bUnion_bUnion, image_bUnion] }
+
 @[simp] theorem card_product (s : finset α) (t : finset β) : card (s.product t) = card s * card t :=
 multiset.card_product _ _
 

src/order/boolean_algebra.lean

@@ -323,6 +323,14 @@ calc x \ y = x ↔ x \ y = x \ ⊥ : by rw sdiff_bot
 theorem sdiff_eq_self_iff_disjoint' : x \ y = x ↔ disjoint x y :=
 by rw [sdiff_eq_self_iff_disjoint, disjoint.comm]
 
+lemma sdiff_lt (hx : y ≤ x) (hy : y ≠ ⊥) :
+  x \ y < x :=
+begin
+  refine sdiff_le.lt_of_ne (λ h, hy _),
+  rw [sdiff_eq_self_iff_disjoint', disjoint_iff] at h,
+  rw [←h, inf_eq_right.mpr hx],
+end
+
 -- cf. `is_compl.antimono`
 lemma sdiff_le_sdiff_self (h : z ≤ x) : w \ x ≤ w \ z :=
 le_of_inf_le_sup_le