chore(data/{equiv,set}/basic): image_preimage (#5465)

* `equiv.symm_image_image`: add `@[simp]`;
* `equiv.image_preimage`, `equiv.preimage_image`: new `simp` lemmas;
* `set.image_preimage_eq`, `set.preimage_image_eq`: make `s : set _` an explicit argument;
* `function.injective.preimage_image`, `function.surjective.image_preimage`: new aliases for `set.preimage_image_eq`
  and `set.image_preimage_eq` with arguments reversed

Also golf a proof about `separated`.

src/analysis/convex/basic.lean

@@ -117,7 +117,7 @@ lemma segment_translate_preimage (a b c : E) : (λ x, a + x) ⁻¹' [a + b, a +
 set.ext $ λ x, mem_segment_translate a
 
 lemma segment_translate_image (a b c: E) : (λx, a + x) '' [b, c] = [a + b, a + c] :=
-segment_translate_preimage a b c ▸ image_preimage_eq $ add_left_surjective a
+segment_translate_preimage a b c ▸ image_preimage_eq _ $ add_left_surjective a
 
 /-! ### Convexity of sets -/
 /-- Convexity of sets -/

src/data/equiv/basic.lean

@@ -260,9 +260,15 @@ protected lemma subset_image {α β} (e : α ≃ β) (s : set α) (t : set β) :
   t ⊆ e '' s ↔ e.symm '' t ⊆ s :=
 by rw [set.image_subset_iff, e.image_eq_preimage]
 
-lemma symm_image_image {α β} (f : equiv α β) (s : set α) : f.symm '' (f '' s) = s :=
+@[simp] lemma symm_image_image {α β} (f : equiv α β) (s : set α) : f.symm '' (f '' s) = s :=
 by { rw [← set.image_comp], simp }
 
+@[simp] lemma image_preimage {α β} (e : α ≃ β) (s : set β) : e '' (e ⁻¹' s) = s :=
+e.surjective.image_preimage s
+
+@[simp] lemma preimage_image {α β} (e : α ≃ β) (s : set α) : e ⁻¹' (e '' s) = s :=
+set.preimage_image_eq s e.injective
+
 protected lemma image_compl {α β} (f : equiv α β) (s : set α) :
   f '' sᶜ = (f '' s)ᶜ :=
 set.image_compl_eq f.bijective

src/data/set/basic.lean

@@ -1357,14 +1357,14 @@ subset.antisymm
   (λ x ⟨y, hy, e⟩, h e ▸ hy)
   (subset_preimage_image f s)
 
-theorem image_preimage_eq {f : α → β} {s : set β} (h : surjective f) : f '' (f ⁻¹' s) = s :=
+theorem image_preimage_eq {f : α → β} (s : set β) (h : surjective f) : f '' (f ⁻¹' s) = s :=
 subset.antisymm
   (image_preimage_subset f s)
   (λ x hx, let ⟨y, e⟩ := h x in ⟨y, (e.symm ▸ hx : f y ∈ s), e⟩)
 
-lemma preimage_eq_preimage {f : β → α} (hf : surjective f) : f ⁻¹' s = preimage f t ↔ s = t :=
+lemma preimage_eq_preimage {f : β → α} (hf : surjective f) : f ⁻¹' s = f ⁻¹' t ↔ s = t :=
 iff.intro
-  (assume eq, by rw [← @image_preimage_eq β α f s hf, ← @image_preimage_eq β α f t hf, eq])
+  (assume eq, by rw [← image_preimage_eq s hf, ← image_preimage_eq t hf, eq])
   (assume eq, eq ▸ rfl)
 
 lemma image_inter_preimage (f : α → β) (s : set α) (t : set β) :
@@ -1756,11 +1756,17 @@ variables {ι : Sort*} {α : Type*} {β : Type*} {f : α → β}
 lemma surjective.preimage_injective (hf : surjective f) : injective (preimage f) :=
 assume s t, (preimage_eq_preimage hf).1
 
+lemma injective.preimage_image (hf : injective f) (s : set α) : f ⁻¹' (f '' s) = s :=
+preimage_image_eq s hf
+
 lemma injective.preimage_surjective (hf : injective f) : surjective (preimage f) :=
-by { intro s, use f '' s, rw preimage_image_eq _ hf }
+by { intro s, use f '' s, rw hf.preimage_image }
+
+lemma surjective.image_preimage (hf : surjective f) (s : set β) : f '' (f ⁻¹' s) = s :=
+image_preimage_eq s hf
 
 lemma surjective.image_surjective (hf : surjective f) : surjective (image f) :=
-by { intro s, use f ⁻¹' s, rw image_preimage_eq hf }
+by { intro s, use f ⁻¹' s, rw hf.image_preimage }
 
 lemma injective.image_injective (hf : injective f) : injective (image f) :=
 by { intros s t h, rw [←preimage_image_eq s hf, ←preimage_image_eq t hf, h] }

src/order/semiconj_Sup.lean

@@ -73,7 +73,7 @@ lemma semiconj.symm_adjoint [partial_order α] [preorder β]
   function.semiconj g' fb fa :=
 begin
   refine λ y, (hg' _).unique _,
-  rw [← @image_preimage_eq _ _ _ {x | g x ≤ fb y} fa.surjective, preimage_set_of_eq],
+  rw [← fa.surjective.image_preimage {x | g x ≤ fb y}, preimage_set_of_eq],
   simp only [h.eq, ← fb.map_rel_iff, fa.left_ord_continuous (hg' _)]
 end
 

src/topology/homeomorph.lean

@@ -142,7 +142,8 @@ closed_embedding_of_embedding_closed h.embedding h.is_closed_map
 @[simp] lemma is_open_preimage (h : α ≃ₜ β) {s : set β} : is_open (h ⁻¹' s) ↔ is_open s :=
 begin
   refine ⟨λ hs, _, continuous_def.1 h.continuous_to_fun s⟩,
-  rw [← (image_preimage_eq h.to_equiv.surjective : _ = s)], exact h.is_open_map _ hs
+  rw [← h.surjective.image_preimage s],
+  exact h.is_open_map _ hs
 end
 
 /-- If an bijective map `e : α ≃ β` is continuous and open, then it is a homeomorphism. -/

src/topology/maps.lean

@@ -239,7 +239,7 @@ lemma to_quotient_map {f : α → β}
     split,
     { exact continuous_def.1 cont s },
     { assume h,
-      rw ← @image_preimage_eq _ _ _ s surj,
+      rw ← surj.image_preimage s,
       exact open_map _ h }
   end⟩
 

src/topology/uniform_space/separation.lean

@@ -245,27 +245,10 @@ begin
     suffices : (x, y) ∈ 𝓢 α ↔ x = y, by simpa only [mem_id_rel],
     refine ⟨λ H, h ⟨mk_mem_prod x_in y_in, H⟩, _⟩,
     rintro rfl,
-    apply id_rel_sub_separation_relation α,
-    rw mem_id_rel },
-  { -- For legibility purpose, let's have explicit coercion C s : ↥s → α  for every α and s : set α
-    let C : Π {β : Type*} (s : set β) (x : s), β := λ _ _, subtype.val,
-    let Δ := diagonal,
-    change _ ⊆ Δ _,
-    change (prod.map (C s) (C s)) ⁻¹' (𝓢 α) = Δ _ at h,
-    rw [inter_comm, ← subtype.image_preimage_coe,  image_subset_iff],
-    change (C _) ⁻¹' _ ⊆ (C _) ⁻¹' _,
-
-    let φ : ↥s × ↥s → (s.prod s)  := (λ x : s × s, ⟨(x.1.1, x.2.1), mk_mem_prod x.1.2 x.2.2⟩),
-    have φ_surj : surjective φ :=
-      λ ⟨⟨x, y⟩, ⟨x_in, y_in⟩⟩, ⟨(⟨x, x_in⟩, ⟨y, y_in⟩), rfl⟩,
-
-    have CCCφ: prod.map (C s) (C s) = C (s.prod s) ∘ φ, by ext ; refl,
-
-    have ΔΔ: (prod.map (C s) (C s)) ⁻¹' (Δ α) = Δ s := set.preimage_coe_coe_diagonal s,
-    apply_fun (image φ) at h,
-    rw [ ← ΔΔ, CCCφ, preimage_comp, preimage_comp,
-        image_preimage_eq φ_surj, image_preimage_eq φ_surj] at h,
-    rw h },
+    exact id_rel_sub_separation_relation α rfl },
+  { rintros ⟨x, y⟩ ⟨⟨x_in, y_in⟩, hS⟩,
+    have A : (⟨⟨x, x_in⟩, ⟨y, y_in⟩⟩ : ↥s × ↥s) ∈ prod.map (coe : s → α) (coe : s → α) ⁻¹' 𝓢 α := hS,
+    simpa using h.subset A }
 end
 
 lemma eq_of_uniformity_inf_nhds_of_is_separated {s : set α} (hs : is_separated s) :