feat(data/set): simple lemmas, renaming (#1137)

* feat(data/set): simple lemmas, renaming

* improve projection lemmas

* arguments order

src/data/set/basic.lean

@@ -782,7 +782,7 @@ assume x hx, h hx
 @[simp] theorem preimage_set_of_eq {p : α → Prop} {f : β → α} : f ⁻¹' {a | p a} = {a | p (f a)} :=
 rfl
 
-theorem preimage_id {s : set α} : id ⁻¹' s = s := rfl
+@[simp] theorem preimage_id {s : set α} : id ⁻¹' s = s := rfl
 
 theorem preimage_comp {s : set γ} : (g ∘ f) ⁻¹' s = f ⁻¹' (g ⁻¹' s) := rfl
 
@@ -1338,6 +1338,26 @@ lemma prod_sub_preimage_iff {W : set γ} {f : α × β → γ} :
   set.prod s t ⊆ f ⁻¹' W ↔ ∀ a b, a ∈ s → b ∈ t → f (a, b) ∈ W :=
 by simp [subset_def]
 
+lemma fst_image_prod_subset (s : set α) (t : set β) :
+  prod.fst '' (set.prod s t) ⊆ s :=
+λ _ h, let ⟨_, ⟨h₂, _⟩, h₁⟩ := (set.mem_image _ _ _).1 h in h₁ ▸ h₂
+
+lemma fst_image_prod (s : set β) {t : set α} (ht : t ≠ ∅) :
+  prod.fst '' (set.prod s t) = s :=
+set.subset.antisymm (fst_image_prod_subset _ _)
+  $ λ y y_in, let (⟨x, x_in⟩ : ∃ (x : α), x ∈ t) := set.exists_mem_of_ne_empty ht in
+    ⟨(y, x), ⟨y_in, x_in⟩, rfl⟩
+
+lemma snd_image_prod_subset (s : set α) (t : set β) :
+  prod.snd '' (set.prod s t) ⊆ t :=
+λ _ h, let ⟨_, ⟨_, h₂⟩, h₁⟩ := (set.mem_image _ _ _).1 h in h₁ ▸ h₂
+
+lemma snd_image_prod {s : set α} (hs : s ≠ ∅) (t : set β) :
+  prod.snd '' (set.prod s t) = t :=
+set.subset.antisymm (snd_image_prod_subset _ _)
+  $ λ y y_in, let (⟨x, x_in⟩ : ∃ (x : α), x ∈ s) := set.exists_mem_of_ne_empty hs in
+    ⟨(x, y), ⟨x_in, y_in⟩, rfl⟩
+
 end prod
 
 section pi

src/data/set/lattice.lean

@@ -145,11 +145,11 @@ by simp [compl_Inter, compl_compl]
 theorem Inter_eq_comp_Union_comp (s : ι → set β) : (⋂ i, s i) = - (⋃ i, -s i) :=
 by simp [compl_compl]
 
-theorem inter_Union_left (s : set β) (t : ι → set β) :
+theorem inter_Union (s : set β) (t : ι → set β) :
   s ∩ (⋃ i, t i) = ⋃ i, s ∩ t i :=
 ext $ by simp
 
-theorem inter_Union_right (s : set β) (t : ι → set β) :
+theorem Union_inter (s : set β) (t : ι → set β) :
   (⋃ i, t i) ∩ s = ⋃ i, t i ∩ s :=
 ext $ by simp
 
@@ -161,38 +161,38 @@ theorem Inter_inter_distrib (s : ι → set β) (t : ι → set β) :
   (⋂ i, s i ∩ t i) = (⋂ i, s i) ∩ (⋂ i, t i) :=
 ext $ by simp [forall_and_distrib]
 
-theorem union_Union_left [inhabited ι] (s : set β) (t : ι → set β) :
+theorem union_Union [inhabited ι] (s : set β) (t : ι → set β) :
   s ∪ (⋃ i, t i) = ⋃ i, s ∪ t i :=
 by rw [Union_union_distrib, Union_const]
 
-theorem union_Union_right [inhabited ι] (s : set β) (t : ι → set β) :
+theorem Union_union [inhabited ι] (s : set β) (t : ι → set β) :
   (⋃ i, t i) ∪ s = ⋃ i, t i ∪ s :=
 by rw [Union_union_distrib, Union_const]
 
-theorem inter_Inter_left [inhabited ι] (s : set β) (t : ι → set β) :
+theorem inter_Inter [inhabited ι] (s : set β) (t : ι → set β) :
   s ∩ (⋂ i, t i) = ⋂ i, s ∩ t i :=
 by rw [Inter_inter_distrib, Inter_const]
 
-theorem inter_Inter_right [inhabited ι] (s : set β) (t : ι → set β) :
+theorem Inter_inter [inhabited ι] (s : set β) (t : ι → set β) :
   (⋂ i, t i) ∩ s = ⋂ i, t i ∩ s :=
 by rw [Inter_inter_distrib, Inter_const]
 
 -- classical
-theorem union_Inter_left (s : set β) (t : ι → set β) :
+theorem union_Inter (s : set β) (t : ι → set β) :
   s ∪ (⋂ i, t i) = ⋂ i, s ∪ t i :=
 ext $ assume x, by simp [classical.forall_or_distrib_left]
 
-theorem diff_Union_right (s : set β) (t : ι → set β) :
+theorem Union_diff (s : set β) (t : ι → set β) :
   (⋃ i, t i) \ s = ⋃ i, t i \ s :=
-inter_Union_right _ _
+Union_inter _ _
 
-theorem diff_Union_left [inhabited ι] (s : set β) (t : ι → set β) :
+theorem diff_Union [inhabited ι] (s : set β) (t : ι → set β) :
   s \ (⋃ i, t i) = ⋂ i, s \ t i :=
-by rw [diff_eq, compl_Union, inter_Inter_left]; refl
+by rw [diff_eq, compl_Union, inter_Inter]; refl
 
-theorem diff_Inter_left (s : set β) (t : ι → set β) :
+theorem diff_Inter (s : set β) (t : ι → set β) :
   s \ (⋂ i, t i) = ⋃ i, s \ t i :=
-by rw [diff_eq, compl_Inter, inter_Union_left]; refl
+by rw [diff_eq, compl_Inter, inter_Union]; refl
 
 /- bounded unions and intersections -/
 
@@ -317,6 +317,18 @@ ext (λ x, by simp)
 theorem compl_bInter (s : set α) (t : α → set β) : -(⋂ i ∈ s, t i) = (⋃ i ∈ s, - t i) :=
 ext (λ x, by simp [classical.not_forall])
 
+theorem inter_bUnion (s : set α) (t : α → set β) (u : set β) :
+  u ∩ (⋃ i ∈ s, t i) = ⋃ i ∈ s, u ∩ t i :=
+begin
+  ext x,
+  simp only [exists_prop, mem_Union, mem_inter_eq],
+  exact ⟨λ ⟨hx, ⟨i, is, xi⟩⟩, ⟨i, is, hx, xi⟩, λ ⟨i, is, hx, xi⟩, ⟨hx, ⟨i, is, xi⟩⟩⟩
+end
+
+theorem bUnion_inter (s : set α) (t : α → set β) (u : set β) :
+  (⋃ i ∈ s, t i) ∩ u = (⋃ i ∈ s, t i ∩ u) :=
+by simp [@inter_comm _ _ u, inter_bUnion]
+
 /-- Intersection of a set of sets. -/
 @[reducible] def sInter (S : set (set α)) : set α := Inf S