refactor(Topology/IsLocalHomeomorph): various small clean-ups (#9150)

- revamp and extend the module docstring
- add some lemma docstrings
- use EqOn where possible
- use \mapsto instead of =>
- replace one terminal rfl by the explicit lemma invoked

Mathlib/Topology/IsLocalHomeomorph.lean

@@ -15,12 +15,19 @@ This file defines local homeomorphisms.
 
 ## Main definitions
 
-* `IsLocalHomeomorph`: A function `f : X → Y` satisfies `IsLocalHomeomorph` if for each
-  point `x : X`, the restriction of `f` to some open neighborhood `U` of `x` gives a homeomorphism
+For a function `f : X → Y ` between topological spaces, we say
+* `IsLocalHomeomorphOn f s` if `f` is a local homeomorphism around each point of `s`: for each
+  `x : X`, the restriction of `f` to some open neighborhood `U` of `x` gives a homeomorphism
   between `U` and an open subset of `Y`.
+* `IsLocalHomeomorph f`: `f` is a local homeomorphism, i.e. it's a local homeomorphism on `univ`.
+
+Note that `IsLocalHomeomorph` is a global condition. This is in contrast to
+`PartialHomeomorph`, which is a homeomorphism between specific open subsets.
+
+## Main results
+* local homeomorphisms are locally injective open maps
+* more!
 
-  Note that `IsLocalHomeomorph` is a global condition. This is in contrast to
-  `PartialHomeomorph`, which is a homeomorphism between specific open subsets.
 -/
 
 
@@ -56,24 +63,24 @@ namespace IsLocalHomeomorphOn
 /-- Proves that `f` satisfies `IsLocalHomeomorphOn f s`. The condition `h` is weaker than the
 definition of `IsLocalHomeomorphOn f s`, since it only requires `e : PartialHomeomorph X Y` to
 agree with `f` on its source `e.source`, as opposed to on the whole space `X`. -/
-theorem mk (h : ∀ x ∈ s, ∃ e : PartialHomeomorph X Y, x ∈ e.source ∧ ∀ y ∈ e.source, f y = e y) :
+theorem mk (h : ∀ x ∈ s, ∃ e : PartialHomeomorph X Y, x ∈ e.source ∧ Set.EqOn f e e.source) :
     IsLocalHomeomorphOn f s := by
   intro x hx
   obtain ⟨e, hx, he⟩ := h x hx
   exact
     ⟨{ e with
         toFun := f
-        map_source' := fun x hx => by rw [he x hx]; exact e.map_source' hx
-        left_inv' := fun x hx => by rw [he x hx]; exact e.left_inv' hx
-        right_inv' := fun y hy => by rw [he _ (e.map_target' hy)]; exact e.right_inv' hy
+        map_source' := fun _x hx ↦ by rw [he hx]; exact e.map_source' hx
+        left_inv' := fun _x hx ↦ by rw [he hx]; exact e.left_inv' hx
+        right_inv' := fun _y hy ↦ by rw [he (e.map_target' hy)]; exact e.right_inv' hy
         continuousOn_toFun := (continuousOn_congr he).mpr e.continuousOn_toFun },
       hx, rfl⟩
 #align is_locally_homeomorph_on.mk IsLocalHomeomorphOn.mk
 
 variable {g f s t}
 
-theorem mono {t : Set X} (hf : IsLocalHomeomorphOn f t) (hst : s ⊆ t) :
-    IsLocalHomeomorphOn f s := fun x hx ↦ hf x (hst hx)
+theorem mono {t : Set X} (hf : IsLocalHomeomorphOn f t) (hst : s ⊆ t) : IsLocalHomeomorphOn f s :=
+  fun x hx ↦ hf x (hst hx)
 
 theorem of_comp_left (hgf : IsLocalHomeomorphOn (g ∘ f) s) (hg : IsLocalHomeomorphOn g (f '' s))
     (cont : ∀ x ∈ s, ContinuousAt f x) : IsLocalHomeomorphOn f s := mk f s fun x hx ↦ by
@@ -84,8 +91,7 @@ theorem of_comp_left (hgf : IsLocalHomeomorphOn (g ∘ f) s) (hg : IsLocalHomeom
     fun y hy ↦ ?_⟩
   change f y = g.symm (gf y)
   have : f y ∈ g.source := by apply interior_subset hy.1.2
-  rw [← he, g.eq_symm_apply this (by apply g.map_source this)]
-  rfl
+  rw [← he, g.eq_symm_apply this (by apply g.map_source this), Function.comp_apply]
 
 theorem of_comp_right (hgf : IsLocalHomeomorphOn (g ∘ f) s) (hf : IsLocalHomeomorphOn f s) :
     IsLocalHomeomorphOn g (f '' s) := mk g _ <| by
@@ -108,7 +114,7 @@ protected theorem continuousAt (hf : IsLocalHomeomorphOn f s) {x : X} (hx : x 
 #align is_locally_homeomorph_on.continuous_at IsLocalHomeomorphOn.continuousAt
 
 protected theorem continuousOn (hf : IsLocalHomeomorphOn f s) : ContinuousOn f s :=
-  ContinuousAt.continuousOn fun _x => hf.continuousAt
+  ContinuousAt.continuousOn fun _x ↦ hf.continuousAt
 #align is_locally_homeomorph_on.continuous_on IsLocalHomeomorphOn.continuousOn
 
 protected theorem comp (hg : IsLocalHomeomorphOn g t) (hf : IsLocalHomeomorphOn f s)
@@ -157,10 +163,10 @@ namespace IsLocalHomeomorph
 /-- Proves that `f` satisfies `IsLocalHomeomorph f`. The condition `h` is weaker than the
 definition of `IsLocalHomeomorph f`, since it only requires `e : PartialHomeomorph X Y` to
 agree with `f` on its source `e.source`, as opposed to on the whole space `X`. -/
-theorem mk (h : ∀ x : X, ∃ e : PartialHomeomorph X Y, x ∈ e.source ∧ ∀ y ∈ e.source, f y = e y) :
+theorem mk (h : ∀ x : X, ∃ e : PartialHomeomorph X Y, x ∈ e.source ∧ Set.EqOn f e e.source) :
     IsLocalHomeomorph f :=
   isLocalHomeomorph_iff_isLocalHomeomorphOn_univ.mpr
-    (IsLocalHomeomorphOn.mk f Set.univ fun x _hx => h x)
+    (IsLocalHomeomorphOn.mk f Set.univ fun x _hx ↦ h x)
 #align is_locally_homeomorph.mk IsLocalHomeomorph.mk
 
 variable {g f}
@@ -177,20 +183,24 @@ theorem map_nhds_eq (hf : IsLocalHomeomorph f) (x : X) : (𝓝 x).map f = 𝓝 (
   hf.isLocalHomeomorphOn.map_nhds_eq (Set.mem_univ x)
 #align is_locally_homeomorph.map_nhds_eq IsLocalHomeomorph.map_nhds_eq
 
+/-- A local homeomorphism is continuous. -/
 protected theorem continuous (hf : IsLocalHomeomorph f) : Continuous f :=
   continuous_iff_continuousOn_univ.mpr hf.isLocalHomeomorphOn.continuousOn
 #align is_locally_homeomorph.continuous IsLocalHomeomorph.continuous
 
+/-- A local homeomorphism is an open map. -/
 protected theorem isOpenMap (hf : IsLocalHomeomorph f) : IsOpenMap f :=
-  IsOpenMap.of_nhds_le fun x => ge_of_eq (hf.map_nhds_eq x)
+  IsOpenMap.of_nhds_le fun x ↦ ge_of_eq (hf.map_nhds_eq x)
 #align is_locally_homeomorph.is_open_map IsLocalHomeomorph.isOpenMap
 
+/-- The composition of local homeomorphisms is a local homeomorphism. -/
 protected theorem comp (hg : IsLocalHomeomorph g) (hf : IsLocalHomeomorph f) :
     IsLocalHomeomorph (g ∘ f) :=
   isLocalHomeomorph_iff_isLocalHomeomorphOn_univ.mpr
     (hg.isLocalHomeomorphOn.comp hf.isLocalHomeomorphOn (Set.univ.mapsTo_univ f))
 #align is_locally_homeomorph.comp IsLocalHomeomorph.comp
 
+/-- An injective local homeomorphism is an open embedding. -/
 theorem openEmbedding_of_injective (hf : IsLocalHomeomorph f) (hi : f.Injective) :
     OpenEmbedding f :=
   openEmbedding_of_continuous_injective_open hf.continuous hi hf.isOpenMap