feat: add image_restrictPreimage (#11640)

- add the theorem `image_restrictPreimage`; use it to simplify the proof of `Set.restrictPreimage_isClosedMap`
- add the equivalent for open maps `Set.restrictPreimage_isOpenMap`.
- delete `IsClosedMap.restrictPreimage`, which duplicates `Set.restrictPreimage_isClosedMap`



Co-authored-by: BGuillemet <115193742+BGuillemet@users.noreply.github.com>

Mathlib/Data/Set/Function.lean

@@ -564,10 +564,15 @@ section
 
 variable (t f)
 
-theorem range_restrictPreimage : range (t.restrictPreimage f) = Subtype.val ⁻¹' range f := by
+variable (s) in
+theorem image_restrictPreimage :
+    t.restrictPreimage f '' (Subtype.val ⁻¹' s) = Subtype.val ⁻¹' (f '' s) := by
   delta Set.restrictPreimage
-  rw [MapsTo.range_restrict, Set.image_preimage_eq_inter_range, Set.preimage_inter,
-    Subtype.coe_preimage_self, Set.univ_inter]
+  rw [← (Subtype.coe_injective).image_injective.eq_iff, ← image_comp, MapsTo.restrict_commutes,
+    image_comp, Subtype.image_preimage_coe, Subtype.image_preimage_coe, image_preimage_inter]
+
+theorem range_restrictPreimage : range (t.restrictPreimage f) = Subtype.val ⁻¹' range f := by
+  simp only [← image_univ, ← image_restrictPreimage, preimage_univ]
 #align set.range_restrict_preimage Set.range_restrictPreimage
 
 variable {f} {U : ι → Set β}

Mathlib/Topology/Constructions.lean

@@ -1097,17 +1097,6 @@ theorem IsOpenMap.restrict {f : X → Y} (hf : IsOpenMap f) {s : Set X} (hs : Is
   hf.comp hs.isOpenMap_subtype_val
 #align is_open_map.restrict IsOpenMap.restrict
 
-lemma IsClosedMap.restrictPreimage {f : X → Y} (hcl : IsClosedMap f) (T : Set Y) :
-    IsClosedMap (T.restrictPreimage f) := by
-  rw [isClosedMap_iff_clusterPt] at hcl ⊢
-  intro A ⟨y, hyT⟩ hy
-  rw [Set.restrictPreimage, MapClusterPt, ← inducing_subtype_val.mapClusterPt_iff, MapClusterPt,
-      map_map, MapsTo.restrict_commutes, ← map_map, ← MapClusterPt, map_principal] at hy
-  rcases hcl _ y hy with ⟨x, hxy, hx⟩
-  have hxT : f x ∈ T := hxy ▸ hyT
-  refine ⟨⟨x, hxT⟩, Subtype.ext hxy, ?_⟩
-  rwa [← inducing_subtype_val.mapClusterPt_iff, MapClusterPt, map_principal]
-
 nonrec theorem IsClosed.closedEmbedding_subtype_val {s : Set X} (hs : IsClosed s) :
     ClosedEmbedding ((↑) : s → X) :=
   closedEmbedding_subtype_val hs

Mathlib/Topology/LocalAtTarget.lean

@@ -63,17 +63,29 @@ theorem Set.restrictPreimage_closedEmbedding (s : Set β) (h : ClosedEmbedding f
 alias ClosedEmbedding.restrictPreimage := Set.restrictPreimage_closedEmbedding
 #align closed_embedding.restrict_preimage ClosedEmbedding.restrictPreimage
 
-theorem Set.restrictPreimage_isClosedMap (s : Set β) (H : IsClosedMap f) :
+theorem IsClosedMap.restrictPreimage (H : IsClosedMap f) (s : Set β) :
     IsClosedMap (s.restrictPreimage f) := by
-  rintro t ⟨u, hu, e⟩
-  refine' ⟨⟨_, (H _ (IsOpen.isClosed_compl hu)).1, _⟩⟩
-  rw [← (congr_arg HasCompl.compl e).trans (compl_compl t)]
-  simp only [Set.preimage_compl, compl_inj_iff]
-  ext ⟨x, hx⟩
-  suffices (∃ y, y ∉ u ∧ f y = x) ↔ ∃ y, y ∉ u ∧ f y ∈ s ∧ f y = x by
-    simpa [Set.restrictPreimage, ← Subtype.coe_inj]
-  exact ⟨fun ⟨a, b, c⟩ => ⟨a, b, c.symm ▸ hx, c⟩, fun ⟨a, b, _, c⟩ => ⟨a, b, c⟩⟩
-#align set.restrict_preimage_is_closed_map Set.restrictPreimage_isClosedMap
+  intro t
+  suffices ∀ u, IsClosed u → Subtype.val ⁻¹' u = t →
+    ∃ v, IsClosed v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t by
+      simpa [isClosed_induced_iff]
+  exact fun u hu e => ⟨f '' u, H u hu, by simp [← e, image_restrictPreimage]⟩
+
+@[deprecated] -- since 2024-04-02
+theorem Set.restrictPreimage_isClosedMap (s : Set β) (H : IsClosedMap f) :
+    IsClosedMap (s.restrictPreimage f) := H.restrictPreimage s
+
+theorem IsOpenMap.restrictPreimage (H : IsOpenMap f) (s : Set β) :
+    IsOpenMap (s.restrictPreimage f) := by
+  intro t
+  suffices ∀ u, IsOpen u → Subtype.val ⁻¹' u = t →
+    ∃ v, IsOpen v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t by
+      simpa [isOpen_induced_iff]
+  exact fun u hu e => ⟨f '' u, H u hu, by simp [← e, image_restrictPreimage]⟩
+
+@[deprecated] -- since 2024-04-02
+theorem Set.restrictPreimage_isOpenMap (s : Set β) (H : IsOpenMap f) :
+    IsOpenMap (s.restrictPreimage f) := H.restrictPreimage s
 
 theorem isOpen_iff_inter_of_iSup_eq_top (s : Set β) : IsOpen s ↔ ∀ i, IsOpen (s ∩ U i) := by
   constructor
@@ -103,7 +115,7 @@ theorem isClosed_iff_coe_preimage_of_iSup_eq_top (s : Set β) :
 
 theorem isClosedMap_iff_isClosedMap_of_iSup_eq_top :
     IsClosedMap f ↔ ∀ i, IsClosedMap ((U i).1.restrictPreimage f) := by
-  refine' ⟨fun h i => Set.restrictPreimage_isClosedMap _ h, _⟩
+  refine' ⟨fun h i => h.restrictPreimage _, _⟩
   rintro H s hs
   rw [isClosed_iff_coe_preimage_of_iSup_eq_top hU]
   intro i