chore(data/equiv/local_equiv,topology/local_homeomorph,data/set/funct…

…ion): review (#6306)

## `data/equiv/local_equiv`:

* move `local_equiv.inj_on` lemmas closer to each other, add missing lemmas;
* rename `local_equiv.bij_on_source` to `local_equiv.bij_on`;
* rename `local_equiv.inv_image_target_eq_souce` to `local_equiv.symm_image_target_eq_souce`;

## `data/set/function`

* add `set.inj_on.mem_of_mem_image`, `set.inj_on.mem_image_iff`, `set.inj_on.preimage_image_inter`;
* add `set.left_inv_on.image_image'` and `set.left_inv_on.image_image`;
* add `function.left_inverse.right_inv_on_range`;
* move `set.inj_on.inv_fun_on_image` to golf the proof;

## `topology/local_homeomorph`

* add lemmas like `local_homeomorph.inj_on`;
* golf the definition of `open_embedding.to_local_homeomorph`, make `f` explicit.

src/data/equiv/local_equiv.lean

@@ -163,22 +163,23 @@ instance : has_coe_to_fun (local_equiv α β) := ⟨_, local_equiv.to_fun⟩
 @[simp, mfld_simps] lemma map_source {x : α} (h : x ∈ e.source) : e x ∈ e.target :=
 e.map_source' h
 
-protected lemma maps_to : maps_to e e.source e.target := λ _, e.map_source
-
 @[simp, mfld_simps] lemma map_target {x : β} (h : x ∈ e.target) : e.symm x ∈ e.source :=
 e.map_target' h
 
-lemma symm_maps_to : maps_to e.symm e.target e.source := e.symm.maps_to
-
 @[simp, mfld_simps] lemma left_inv {x : α} (h : x ∈ e.source) : e.symm (e x) = x :=
 e.left_inv' h
 
-protected lemma left_inv_on : left_inv_on e.symm e e.source := λ _, e.left_inv
-
 @[simp, mfld_simps] lemma right_inv {x : β} (h : x ∈ e.target) : e (e.symm x) = x :=
 e.right_inv' h
 
-protected lemma right_inv_on : right_inv_on e.symm e e.target := λ _, e.right_inv
+protected lemma maps_to : maps_to e e.source e.target := λ x, e.map_source
+lemma symm_maps_to : maps_to e.symm e.target e.source := e.symm.maps_to
+protected lemma left_inv_on : left_inv_on e.symm e e.source := λ x, e.left_inv
+protected lemma right_inv_on : right_inv_on e.symm e e.target := λ x, e.right_inv
+protected lemma inv_on : inv_on e.symm e e.source e.target := ⟨e.left_inv_on, e.right_inv_on⟩
+protected lemma inj_on : inj_on e e.source := e.left_inv_on.inj_on
+protected lemma bij_on : bij_on e e.source e.target := e.inv_on.bij_on e.maps_to e.symm_maps_to
+protected lemma surj_on : surj_on e e.source e.target := e.bij_on.surj_on
 
 /-- Associating to a local_equiv an equiv between the source and the target -/
 protected def to_equiv : equiv (e.source) (e.target) :=
@@ -191,12 +192,7 @@ protected def to_equiv : equiv (e.source) (e.target) :=
 @[simp, mfld_simps] lemma symm_target : e.symm.target = e.source := rfl
 @[simp, mfld_simps] lemma symm_symm : e.symm.symm = e := by { cases e, refl }
 
-/-- A local equiv induces a bijection between its source and target -/
-lemma bij_on_source : bij_on e e.source e.target :=
-inv_on.bij_on ⟨e.left_inv_on, e.right_inv_on⟩ e.maps_to e.symm_maps_to
-
-lemma image_source_eq_target : e '' e.source = e.target :=
-e.bij_on_source.image_eq
+lemma image_source_eq_target : e '' e.source = e.target := e.bij_on.image_eq
 
 lemma image_inter_source_eq' (s : set α) :
   e '' (s ∩ e.source) = e.target ∩ e.symm ⁻¹' s :=
@@ -240,8 +236,8 @@ e.symm.source_inter_preimage_inv_preimage _
 lemma source_subset_preimage_target : e.source ⊆ e ⁻¹' e.target :=
 λx hx, e.map_source hx
 
-lemma inv_image_target_eq_source : e.symm '' e.target = e.source :=
-e.symm.bij_on_source.image_eq
+lemma symm_image_target_eq_source : e.symm '' e.target = e.source :=
+e.symm.image_source_eq_target
 
 lemma target_subset_preimage_source : e.target ⊆ e.symm ⁻¹' e.source :=
 λx hx, e.map_target hx

src/data/set/function.lean

@@ -243,17 +243,22 @@ lemma inj_on_iff_injective : inj_on f s ↔ injective (restrict f s) :=
 ⟨λ H a b h, subtype.eq $ H a.2 b.2 h,
  λ H a as b bs h, congr_arg subtype.val $ @H ⟨a, as⟩ ⟨b, bs⟩ h⟩
 
-lemma inj_on.inv_fun_on_image [nonempty α] (h : inj_on f s₂) (ht : s₁ ⊆ s₂) :
-  (inv_fun_on f s₂) '' (f '' s₁) = s₁ :=
-begin
-  have : eq_on ((inv_fun_on f s₂) ∘ f) id s₁, from λz hz, inv_fun_on_eq' h (ht hz),
-  rw [← image_comp, this.image_eq, image_id]
-end
-
 lemma inj_on_preimage {B : set (set β)} (hB : B ⊆ powerset (range f)) :
   inj_on (preimage f) B :=
 λ s hs t ht hst, (preimage_eq_preimage' (hB hs) (hB ht)).1 hst
 
+lemma inj_on.mem_of_mem_image {x} (hf : inj_on f s) (hs : s₁ ⊆ s) (h : x ∈ s) (h₁ : f x ∈ f '' s₁) :
+  x ∈ s₁ :=
+let ⟨x', h', eq⟩ := h₁ in hf (hs h') h eq ▸ h'
+
+lemma inj_on.mem_image_iff {x} (hf : inj_on f s) (hs : s₁ ⊆ s) (hx : x ∈ s) :
+  f x ∈ f '' s₁ ↔ x ∈ s₁ :=
+⟨hf.mem_of_mem_image hs hx, mem_image_of_mem f⟩
+
+lemma inj_on.preimage_image_inter (hf : inj_on f s) (hs : s₁ ⊆ s) :
+  f ⁻¹' (f '' s₁) ∩ s = s₁ :=
+ext $ λ x, ⟨λ ⟨h₁, h₂⟩, hf.mem_of_mem_image hs h₂ h₁, λ h, ⟨mem_image_of_mem _ h, hs h⟩⟩
+
 /-! ### Surjectivity on a set -/
 
 /-- `f` is surjective from `a` to `b` if `b` is contained in the image of `a`. -/
@@ -446,6 +451,14 @@ begin
   rintro _ ⟨h₁, x, hx, rfl⟩, exact ⟨⟨h₁, by rwa hf hx⟩, mem_image_of_mem _ hx⟩
 end
 
+theorem left_inv_on.image_image (hf : left_inv_on f' f s) :
+  f' '' (f '' s) = s :=
+by rw [image_image, image_congr hf, image_id']
+
+theorem left_inv_on.image_image' (hf : left_inv_on f' f s)  (hs : s₁ ⊆ s) :
+  f' '' (f '' s₁) = s₁ :=
+(hf.mono hs).image_image
+
 /-! ### Right inverse -/
 
 /-- `g` is a right inverse to `f` on `b` if `f (g x) = x` for all `x ∈ b`. -/
@@ -517,6 +530,10 @@ theorem inj_on.left_inv_on_inv_fun_on [nonempty α] (h : inj_on f s) :
   left_inv_on (inv_fun_on f s) f s :=
 λ x hx, inv_fun_on_eq' h hx
 
+lemma inj_on.inv_fun_on_image [nonempty α] (h : inj_on f s₂) (ht : s₁ ⊆ s₂) :
+  (inv_fun_on f s₂) '' (f '' s₁) = s₁ :=
+h.left_inv_on_inv_fun_on.image_image' ht
+
 theorem surj_on.right_inv_on_inv_fun_on [nonempty α] (h : surj_on f s t) :
   right_inv_on (inv_fun_on f s) f t :=
 λ y hy, inv_fun_on_eq $ mem_image_iff_bex.1 $ h hy
@@ -706,6 +723,10 @@ lemma surjective.surj_on (hf : surjective f) (s : set β) :
   surj_on f univ s :=
 (surjective_iff_surj_on_univ.1 hf).mono (subset.refl _) (subset_univ _)
 
+lemma left_inverse.right_inv_on_range {g : β → α} (h : left_inverse f g) :
+  right_inv_on f g (range g) :=
+forall_range_iff.2 $ λ i, congr_arg g (h i)
+
 namespace semiconj
 
 lemma maps_to_image (h : semiconj f fa fb) (ha : maps_to fa s t) :

src/topology/local_homeomorph.lean

@@ -108,16 +108,20 @@ e.left_inv' h
 @[simp, mfld_simps] lemma right_inv {x : β} (h : x ∈ e.target) : e (e.symm x) = x :=
 e.right_inv' h
 
+protected lemma maps_to : maps_to e e.source e.target := λ x, e.map_source
+protected lemma symm_maps_to : maps_to e.symm e.target e.source := e.symm.maps_to
+protected lemma left_inv_on : left_inv_on e.symm e e.source := λ x, e.left_inv
+protected lemma right_inv_on : right_inv_on e.symm e e.target := λ x, e.right_inv
+protected lemma inv_on : inv_on e.symm e e.source e.target := ⟨e.left_inv_on, e.right_inv_on⟩
+protected lemma inj_on : inj_on e e.source := e.left_inv_on.inj_on
+protected lemma bij_on : bij_on e e.source e.target := e.inv_on.bij_on e.maps_to e.symm_maps_to
+protected lemma surj_on : surj_on e e.source e.target := e.bij_on.surj_on
+
 lemma source_preimage_target : e.source ⊆ e ⁻¹' e.target := λ _ h, map_source e h
 
 lemma eq_of_local_equiv_eq {e e' : local_homeomorph α β}
   (h : e.to_local_equiv = e'.to_local_equiv) : e = e' :=
-begin
-  cases e, cases e',
-  dsimp at *,
-  induction h,
-  refl
-end
+by { cases e, cases e', cases h, refl }
 
 lemma eventually_left_inverse (e : local_homeomorph α β) {x} (hx : x ∈ e.source) :
   ∀ᶠ y in 𝓝 x, e.symm (e y) = y :=
@@ -257,7 +261,7 @@ def of_continuous_open_restrict (e : local_equiv α β) (hc : continuous_on e e.
 
 /-- A `local_equiv` with continuous open forward map and an open source is a `local_homeomorph`. -/
 def of_continuous_open (e : local_equiv α β) (hc : continuous_on e e.source)
-  (ho : is_open_map  e) (hs : is_open e.source) :
+  (ho : is_open_map e) (hs : is_open e.source) :
   local_homeomorph α β :=
 of_continuous_open_restrict e hc (ho.restrict hs) hs
 
@@ -700,15 +704,15 @@ def to_homeomorph_of_source_eq_univ_target_eq_univ (h : e.source = (univ : set 
 
 /-- A local homeomorphism whose source is all of `α` defines an open embedding of `α` into `β`.  The
 converse is also true; see `open_embedding.to_local_homeomorph`. -/
-lemma to_open_embedding (h : e.source = set.univ) : open_embedding e.to_fun :=
+lemma to_open_embedding (h : e.source = set.univ) : open_embedding e :=
 begin
   apply open_embedding_of_continuous_injective_open,
   { apply continuous_iff_continuous_on_univ.mpr,
     rw ← h,
     exact e.continuous_to_fun },
   { apply set.injective_iff_inj_on_univ.mpr,
     rw ← h,
-    exact e.to_local_equiv.bij_on_source.inj_on },
+    exact e.inj_on },
   { intros U hU,
     simpa only [h, subset_univ] with mfld_simps using e.image_open_of_open hU}
 end
@@ -737,61 +741,18 @@ end homeomorph
 
 namespace open_embedding
 variables [nonempty α]
-variables {f : α → β} (h : open_embedding f)
-include f h
-
-/-- An open embedding of `α` into `β`, with `α` nonempty, defines a local equivalence whose source
-is all of `α`.  This is mainly an auxiliary lemma for the stronger result `to_local_homeomorph`. -/
-noncomputable def to_local_equiv : local_equiv α β :=
-set.inj_on.to_local_equiv f set.univ (set.injective_iff_inj_on_univ.mp h.to_embedding.inj)
-
-@[simp, mfld_simps] lemma to_local_equiv_coe : (h.to_local_equiv : α → β) = f := rfl
-@[simp, mfld_simps] lemma to_local_equiv_source : h.to_local_equiv.source = set.univ := rfl
-
-@[simp, mfld_simps] lemma to_local_equiv_target : h.to_local_equiv.target = set.range f :=
-begin
-  rw ←local_equiv.image_source_eq_target,
-  ext,
-  split,
-  { exact λ ⟨a, _, h'⟩, ⟨a, h'⟩ },
-  { exact λ ⟨a, h'⟩, ⟨a, by trivial, h'⟩ }
-end
-
-lemma open_target : is_open h.to_local_equiv.target :=
-by simpa only with mfld_simps using h.open_range
-
-lemma continuous_inv_fun : continuous_on h.to_local_equiv.inv_fun h.to_local_equiv.target :=
-begin
-  apply (continuous_on_open_iff h.open_target).mpr,
-  intros t ht,
-  simp only with mfld_simps,
-  convert h.open_iff_image_open.mp ht,
-  ext y,
-  have hinv : ∀ x : α, (f x = y) → h.to_local_equiv.symm y = x :=
-    λ x hxy, by { simpa only [hxy.symm] with mfld_simps using h.to_local_equiv.left_inv },
-  simp only [mem_image, mem_range] with mfld_simps,
-  split,
-  { rintros ⟨⟨x, hxy⟩, hy⟩,
-    refine ⟨x, _, hxy⟩,
-    rwa (hinv x hxy) at hy },
-  { rintros ⟨x, hx, hxy⟩,
-    refine ⟨⟨x, hxy⟩, _⟩,
-    rwa ← (hinv x hxy) at hx }
-end
+variables (f : α → β) (h : open_embedding f)
 
 /-- An open embedding of `α` into `β`, with `α` nonempty, defines a local homeomorphism whose source
 is all of `α`.  The converse is also true; see `local_homeomorph.to_open_embedding`. -/
 noncomputable def to_local_homeomorph : local_homeomorph α β :=
-{ to_local_equiv := h.to_local_equiv,
-  open_source := is_open_univ,
-  open_target := h.open_target,
-  continuous_to_fun := by simpa only with mfld_simps using h.continuous.continuous_on,
-  continuous_inv_fun := h.continuous_inv_fun }
+local_homeomorph.of_continuous_open
+  ((h.to_embedding.inj.inj_on univ).to_local_equiv _ _)
+  h.continuous.continuous_on h.is_open_map is_open_univ
 
-@[simp, mfld_simps] lemma to_local_homeomorph_coe : (h.to_local_homeomorph : α → β) = f := rfl
-@[simp, mfld_simps] lemma source : h.to_local_homeomorph.source = set.univ := rfl
-@[simp, mfld_simps] lemma target : h.to_local_homeomorph.target = set.range f :=
-h.to_local_equiv_target
+@[simp, mfld_simps] lemma to_local_homeomorph_coe : ⇑(h.to_local_homeomorph f) = f := rfl
+@[simp, mfld_simps] lemma source : (h.to_local_homeomorph f).source = set.univ := rfl
+@[simp, mfld_simps] lemma target : (h.to_local_homeomorph f).target = set.range f := image_univ
 
 end open_embedding
 
@@ -804,7 +765,7 @@ lemma continuous_at_iff
   continuous_at (g ∘ f) x ↔ continuous_at g (f x) :=
 begin
   haveI : nonempty α := ⟨x⟩,
-  convert ((hf.to_local_homeomorph.continuous_at_iff_continuous_at_comp_right) _).symm,
+  convert (((hf.to_local_homeomorph f).continuous_at_iff_continuous_at_comp_right) _).symm,
   { apply (local_homeomorph.left_inv _ _).symm,
     simp, },
   { simp, },
@@ -820,7 +781,7 @@ variables (s : opens α) [nonempty s]
 /-- The inclusion of an open subset `s` of a space `α` into `α` is a local homeomorphism from the
 subtype `s` to `α`. -/
 noncomputable def local_homeomorph_subtype_coe : local_homeomorph s α :=
-open_embedding.to_local_homeomorph (s.2.open_embedding_subtype_coe)
+open_embedding.to_local_homeomorph _ s.2.open_embedding_subtype_coe
 
 @[simp, mfld_simps] lemma local_homeomorph_subtype_coe_coe :
   (s.local_homeomorph_subtype_coe : s → α) = coe := rfl