feat(data/set/n_ary): Distributivity of ∩ (#17924)

`set.image2 f` for `injective2 f` distributes over intersection.

Also move the required results from `data.set.prod` to `data.set.n_ary`. As a bonus, this makes quite a few files not depend on `data.set.n_ary` anymore and matches the import direction for the corresponding `finset` files.

src/data/finset/n_ary.lean

@@ -109,6 +109,14 @@ coe_injective $ by { push_cast, exact image2_union_left }
 lemma image₂_union_right [decidable_eq β] : image₂ f s (t ∪ t') = image₂ f s t ∪ image₂ f s t' :=
 coe_injective $ by { push_cast, exact image2_union_right }
 
+lemma image₂_inter_left [decidable_eq α] (hf : injective2 f) :
+  image₂ f (s ∩ s') t = image₂ f s t ∩ image₂ f s' t :=
+coe_injective $ by { push_cast, exact image2_inter_left hf }
+
+lemma image₂_inter_right [decidable_eq β] (hf : injective2 f) :
+  image₂ f s (t ∩ t') = image₂ f s t ∩ image₂ f s t' :=
+coe_injective $ by { push_cast, exact image2_inter_right hf }
+
 lemma image₂_inter_subset_left [decidable_eq α] :
   image₂ f (s ∩ s') t ⊆ image₂ f s t ∩ image₂ f s' t :=
 coe_subset.1 $ by { push_cast, exact image2_inter_subset_left }

src/data/set/n_ary.lean

@@ -3,8 +3,7 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
-import data.set.basic
-import data.set.image
+import data.set.prod
 
 /-!
 # N-ary images of sets
@@ -64,6 +63,24 @@ lemma forall_image2_iff {p : γ → Prop} :
   image2 f s t ⊆ u ↔ ∀ (x ∈ s) (y ∈ t), f x y ∈ u :=
 forall_image2_iff
 
+variables (f)
+
+@[simp] lemma image_prod : (λ x : α × β, f x.1 x.2) '' s ×ˢ t = image2 f s t :=
+ext $ λ a,
+⟨ by { rintro ⟨_, _, rfl⟩, exact ⟨_, _, (mem_prod.1 ‹_›).1, (mem_prod.1 ‹_›).2, rfl⟩ },
+  by { rintro ⟨_, _, _, _, rfl⟩, exact ⟨(_, _), ⟨‹_›, ‹_›⟩, rfl⟩ }⟩
+
+@[simp] lemma image_uncurry_prod (s : set α) (t : set β) : uncurry f '' s ×ˢ t = image2 f s t :=
+image_prod _
+
+@[simp] lemma image2_mk_eq_prod : image2 prod.mk s t = s ×ˢ t := ext $ by simp
+
+@[simp] lemma image2_curry (f : α × β → γ) (s : set α) (t : set β) :
+  image2 (λ a b, f (a, b)) s t = f '' s ×ˢ t :=
+by simp [←image_uncurry_prod, uncurry]
+
+variables {f}
+
 lemma image2_union_left : image2 f (s ∪ s') t = image2 f s t ∪ image2 f s' t :=
 begin
   ext c,
@@ -82,6 +99,12 @@ begin
     simp [mem_union, *] }
 end
 
+lemma image2_inter_left (hf : injective2 f) : image2 f (s ∩ s') t = image2 f s t ∩ image2 f s' t :=
+by simp_rw [←image_uncurry_prod, inter_prod, ←image_inter hf.uncurry]
+
+lemma image2_inter_right (hf : injective2 f) : image2 f s (t ∩ t') = image2 f s t ∩ image2 f s t' :=
+by simp_rw [←image_uncurry_prod, prod_inter, ←image_inter hf.uncurry]
+
 @[simp] lemma image2_empty_left : image2 f ∅ t = ∅ := ext $ by simp
 @[simp] lemma image2_empty_right : image2 f s ∅ = ∅ := ext $ by simp
 

src/data/set/prod.lean

@@ -3,8 +3,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johannes Hölzl, Patrick Massot
 -/
-import data.set.basic
-import data.set.n_ary
+import data.set.image
 
 /-!
 # Sets in product and pi types
@@ -291,20 +290,6 @@ begin
   refl,
 end
 
-@[simp] lemma image_prod (f : α → β → γ) : (λ x : α × β, f x.1 x.2) '' s ×ˢ t = image2 f s t :=
-set.ext $ λ a,
-⟨ by { rintro ⟨_, _, rfl⟩, exact ⟨_, _, (mem_prod.mp ‹_›).1, (mem_prod.mp ‹_›).2, rfl⟩ },
-  by { rintro ⟨_, _, _, _, rfl⟩, exact ⟨(_, _), mem_prod.mpr ⟨‹_›, ‹_›⟩, rfl⟩ }⟩
-
-@[simp] lemma image2_mk_eq_prod : image2 prod.mk s t = s ×ˢ t := ext $ by simp
-
-@[simp] lemma image2_curry (f : α × β → γ) (s : set α) (t : set β) :
-  image2 (λ a b, f (a, b)) s t = (s ×ˢ t).image f :=
-by rw [←image2_mk_eq_prod, image_image2]
-
-@[simp] lemma image_uncurry_prod (f : α → β → γ) (s : set α) (t : set β) :
-  uncurry f '' s ×ˢ t = image2 f s t := by { rw ←image2_curry, refl }
-
 section mono
 
 variables [preorder α] {f : α → set β} {g : α → set γ}

src/order/bounds/basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Yury Kudryashov
 -/
 import data.set.intervals.basic
+import data.set.n_ary
 
 /-!