refactor(data/equiv/local_equiv): use dot notation for eq_on_source (…

…#2830)

Also reuse more lemmas from `data/set/function`.

src/data/equiv/local_equiv.lean

@@ -120,15 +120,23 @@ instance : has_coe_to_fun (local_equiv α β) := ⟨_, local_equiv.to_fun⟩
 @[simp] 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] 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] 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] 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
+
 /-- Associating to a local_equiv an equiv between the source and the target -/
 protected def to_equiv : equiv (e.source) (e.target) :=
 { to_fun    := λ x, ⟨e x, e.map_source x.mem⟩,
@@ -142,8 +150,7 @@ protected def to_equiv : equiv (e.source) (e.target) :=
 
 /-- 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 ⟨λ x, e.left_inv, λ x, e.right_inv⟩
-(λ x, e.map_source) (λ x, e.map_target)
+inv_on.bij_on ⟨e.left_inv_on, e.right_inv_on⟩ e.maps_to e.symm_maps_to
 
 lemma image_eq_target_inter_inv_preimage {s : set α} (h : s ⊆ e.source) :
   e '' s = e.target ∩ e.symm ⁻¹' s :=
@@ -352,94 +359,77 @@ local_equiv.ext (λx, rfl) (λx, rfl) $ by { simp [trans_source, inter_comm], rw
 /-- `eq_on_source e e'` means that `e` and `e'` have the same source, and coincide there. Then `e`
 and `e'` should really be considered the same local equiv. -/
 def eq_on_source (e e' : local_equiv α β) : Prop :=
-e.source = e'.source ∧ (∀x ∈ e.source, e x = e' x)
+e.source = e'.source ∧ (e.source.eq_on e e')
 
 /-- `eq_on_source` is an equivalence relation -/
 instance eq_on_source_setoid : setoid (local_equiv α β) :=
 { r     := eq_on_source,
   iseqv := ⟨
     λe, by simp [eq_on_source],
-    λe e' h, by { simp [eq_on_source, h.1.symm], exact λx hx, (h.2 x hx).symm },
-    λe e' e'' h h', ⟨by rwa [← h'.1, ← h.1], λx hx, by { rw [← h'.2 x, h.2 x hx], rwa ← h.1 }⟩⟩ }
+    λe e' h, by { simp [eq_on_source, h.1.symm], exact λx hx, (h.2 hx).symm },
+    λe e' e'' h h', ⟨by rwa [← h'.1, ← h.1], λx hx, by { rw [← h'.2, h.2 hx], rwa ← h.1 }⟩⟩ }
 
 lemma eq_on_source_refl : e ≈ e := setoid.refl _
 
-/-- If two local equivs are equivalent, so are their inverses -/
-lemma eq_on_source_symm {e e' : local_equiv α β} (h : e ≈ e') : e.symm ≈ e'.symm :=
-begin
-  have T : e.target = e'.target,
-  { have : set.bij_on e' e.source e.target := e.bij_on_source.congr h.2,
-    have A : e' '' e.source = e.target := this.image_eq,
-    rw [h.1, e'.bij_on_source.image_eq] at A,
-    exact A.symm },
-  refine ⟨T, λx hx, _⟩,
-  have xt : x ∈ e.target := hx,
-  rw T at xt,
-  have e's : e'.symm x ∈ e.source, by { rw h.1, apply e'.map_target xt },
-  have A : e (e.symm x) = x := e.right_inv hx,
-  have B : e (e'.symm x) = x,
-    by { rw h.2, exact e'.right_inv xt, exact e's },
-  apply e.bij_on_source.inj_on (e.map_target hx) e's,
-  rw [A, B]
-end
-
 /-- Two equivalent local equivs have the same source -/
-lemma source_eq_of_eq_on_source {e e' : local_equiv α β} (h : e ≈ e') : e.source = e'.source :=
+lemma eq_on_source.source_eq {e e' : local_equiv α β} (h : e ≈ e') : e.source = e'.source :=
 h.1
 
+/-- Two equivalent local equivs coincide on the source -/
+lemma eq_on_source.eq_on {e e' : local_equiv α β} (h : e ≈ e') : e.source.eq_on e e' :=
+h.2
+
 /-- Two equivalent local equivs have the same target -/
-lemma target_eq_of_eq_on_source {e e' : local_equiv α β} (h : e ≈ e') : e.target = e'.target :=
-(eq_on_source_symm h).1
+lemma eq_on_source.target_eq {e e' : local_equiv α β} (h : e ≈ e') : e.target = e'.target :=
+by simp only [← image_source_eq_target, ← h.source_eq, h.2.image_eq]
 
-/-- Two equivalent local equivs coincide on the source -/
-lemma apply_eq_of_eq_on_source {e e' : local_equiv α β} (h : e ≈ e') {x : α} (hx : x ∈ e.source) :
-  e x = e' x :=
-h.2 x hx
+/-- If two local equivs are equivalent, so are their inverses. -/
+lemma eq_on_source.symm' {e e' : local_equiv α β} (h : e ≈ e') : e.symm ≈ e'.symm :=
+begin
+  refine ⟨h.target_eq, eq_on_of_left_inv_on_of_right_inv_on e.left_inv_on _ _⟩;
+    simp only [symm_source, h.target_eq, h.source_eq, e'.symm_maps_to],
+  exact e'.right_inv_on.congr_right e'.symm_maps_to (h.source_eq ▸ h.eq_on.symm),
+end
 
 /-- Two equivalent local equivs have coinciding inverses on the target -/
-lemma inv_apply_eq_of_eq_on_source {e e' : local_equiv α β} (h : e ≈ e') {x : β} (hx : x ∈ e.target) :
-  e.symm x = e'.symm x :=
-(eq_on_source_symm h).2 x hx
+lemma eq_on_source.symm_eq_on {e e' : local_equiv α β} (h : e ≈ e') :
+  eq_on e.symm e'.symm e.target :=
+h.symm'.eq_on
 
 /-- Composition of local equivs respects equivalence -/
-lemma eq_on_source_trans {e e' : local_equiv α β} {f f' : local_equiv β γ}
+lemma eq_on_source.trans' {e e' : local_equiv α β} {f f' : local_equiv β γ}
   (he : e ≈ e') (hf : f ≈ f') : e.trans f ≈ e'.trans f' :=
 begin
   split,
-  { have : e.target = e'.target := (eq_on_source_symm he).1,
-    rw [trans_source'', trans_source'', ← this, ← hf.1],
-    exact eq_on.image_eq (λx hx, (eq_on_source_symm he).2 x hx.1) },
+  { rw [trans_source'', trans_source'', ← he.target_eq, ← hf.1],
+    exact (he.symm'.eq_on.mono $ inter_subset_left _ _).image_eq },
   { assume x hx,
     rw trans_source at hx,
-    simp [(he.2 x hx.1).symm, hf.2 _ hx.2] }
+    simp [(he.2 hx.1).symm, hf.2 hx.2] }
 end
 
 /-- Restriction of local equivs respects equivalence -/
-lemma eq_on_source_restr {e e' : local_equiv α β} (he : e ≈ e') (s : set α) :
+lemma eq_on_source.restr {e e' : local_equiv α β} (he : e ≈ e') (s : set α) :
   e.restr s ≈ e'.restr s :=
 begin
   split,
   { simp [he.1] },
   { assume x hx,
     simp only [mem_inter_eq, restr_source] at hx,
-    exact he.2 x hx.1 }
+    exact he.2 hx.1 }
 end
 
 /-- Preimages are respected by equivalence -/
-lemma eq_on_source_preimage {e e' : local_equiv α β} (he : e ≈ e') (s : set β) :
+lemma eq_on_source.source_inter_preimage_eq {e e' : local_equiv α β} (he : e ≈ e') (s : set β) :
   e.source ∩ e ⁻¹' s = e'.source ∩ e' ⁻¹' s :=
 begin
   ext x,
   simp only [mem_inter_eq, mem_preimage],
   split,
   { assume hx,
-    rwa [apply_eq_of_eq_on_source (setoid.symm he), source_eq_of_eq_on_source (setoid.symm he)],
-    rw source_eq_of_eq_on_source he at hx,
-    exact hx.1 },
+    rwa [← he.2 hx.1, ← he.source_eq] },
   { assume hx,
-    rwa [apply_eq_of_eq_on_source he, source_eq_of_eq_on_source he],
-    rw source_eq_of_eq_on_source (setoid.symm he) at hx,
-    exact hx.1 },
+    rwa [← (setoid.symm he).2 hx.1, he.source_eq] }
 end
 
 /-- Composition of a local equiv and its inverse is equivalent to the restriction of the identity
@@ -465,10 +455,10 @@ lemma eq_of_eq_on_source_univ (e e' : local_equiv α β) (h : e ≈ e')
   (s : e.source = univ) (t : e.target = univ) : e = e' :=
 begin
   apply local_equiv.ext (λx, _) (λx, _) h.1,
-  { apply h.2 x,
+  { apply h.2,
     rw s,
     exact mem_univ _ },
-  { apply (eq_on_source_symm h).2 x,
+  { apply h.symm'.2,
     rw [symm_source, t],
     exact mem_univ _ }
 end

src/data/set/function.lean

@@ -335,12 +335,11 @@ theorem inj_on.right_inv_on_of_left_inv_on (hf : inj_on f s) (hf' : left_inv_on
   right_inv_on f f' s :=
 λ x h, hf (h₂ $ h₁ h) h (hf' (h₁ h))
 
-theorem eq_on_of_left_inv_of_right_inv (h₁ : left_inv_on f₁' f s) (h₂ : right_inv_on f₂' f t)
+theorem eq_on_of_left_inv_on_of_right_inv_on (h₁ : left_inv_on f₁' f s) (h₂ : right_inv_on f₂' f t)
   (h : maps_to f₂' t s) : eq_on f₁' f₂' t :=
 λ y hy,
-calc
-  f₁' y = (f₁' ∘ f ∘ f₂') y : congr_arg f₁' (h₂ hy).symm
-  ...  = f₂' y              : h₁ (h hy)
+calc f₁' y = (f₁' ∘ f ∘ f₂') y : congr_arg f₁' (h₂ hy).symm
+      ...  = f₂' y              : h₁ (h hy)
 
 theorem surj_on.left_inv_on_of_right_inv_on (hf : surj_on f s t) (hf' : right_inv_on f f' s) :
   left_inv_on f f' t :=

src/geometry/manifold/manifold.lean

@@ -23,20 +23,21 @@ notion of structure groupoid, i.e., a set of local homeomorphisms stable under c
 inverse, to which the change of coordinates should belong.
 
 ## Main definitions
-* `structure_groupoid H`   : a subset of local homeomorphisms of `H` stable under composition, inverse
-                             and restriction (ex: local diffeos)
+* `structure_groupoid H`   : a subset of local homeomorphisms of `H` stable under composition,
+                             inverse and restriction (ex: local diffeos)
 * `pregroupoid H`          : a subset of local homeomorphisms of `H` stable under composition and
                              restriction, but not inverse (ex: smooth maps)
-* `groupoid_of_pregroupoid`: construct a groupoid from a pregroupoid, by requiring that a map and its
-                             inverse both belong to the pregroupoid (ex: construct diffeos from smooth
-                             maps)
+* `groupoid_of_pregroupoid`: construct a groupoid from a pregroupoid, by requiring that a map and
+                             its inverse both belong to the pregroupoid (ex: construct diffeos from
+                             smooth maps)
 * `continuous_groupoid H`  : the groupoid of all local homeomorphisms of `H`
 
 * `manifold H M`           : manifold structure on `M` modelled on `H`, given by an atlas of local
-                             homeomorphisms from `M` to `H` whose sources cover `M`. This is a type class.
-* `has_groupoid M G`       : when `G` is a structure groupoid on `H` and `M` is a manifold modelled on
-                             `H`, require that all coordinate changes belong to `G`. This is a type
-                             class
+                             homeomorphisms from `M` to `H` whose sources cover `M`. This is a type
+                             class.
+* `has_groupoid M G`       : when `G` is a structure groupoid on `H` and `M` is a manifold modelled
+                             on `H`, require that all coordinate changes belong to `G`. This is
+                             a type class
 * `atlas H M`              : when `M` is a manifold modelled on `H`, the atlas of this manifold
                              structure, i.e., the set of charts
 * `structomorph G M M'`    : the set of diffeomorphisms between the manifolds `M` and `M'` for the
@@ -183,7 +184,7 @@ def id_groupoid (H : Type u) [topological_space H] : structure_groupoid H :=
       rwa ← this },
     { right,
       change (e.to_local_equiv).source = ∅ at he,
-      rwa [set.mem_set_of_eq, source_eq_of_eq_on_source he'e] }
+      rwa [set.mem_set_of_eq, he'e.source_eq] }
   end }
 
 /-- Every structure groupoid contains the identity groupoid -/
@@ -250,7 +251,7 @@ def pregroupoid.groupoid (PG : pregroupoid H) : structure_groupoid H :=
     split,
     { apply PG.congr e'.open_source ee'.2,
       simp only [ee'.1, he.1] },
-    { have A := eq_on_source_symm ee',
+    { have A := ee'.symm',
       apply PG.congr e'.symm.open_source A.2,
       convert he.2,
       rw A.1,
@@ -275,7 +276,7 @@ lemma mem_pregroupoid_of_eq_on_source (PG : pregroupoid H) {e e' : local_homeomo
   PG.property e' e'.source :=
 begin
   rw ← he'.1,
-  exact PG.congr e.open_source (λx hx, (he'.2 x hx).symm) he,
+  exact PG.congr e.open_source he'.eq_on.symm he,
 end
 
 /-- The pregroupoid of all local maps on a topological space H -/
@@ -532,12 +533,12 @@ def structomorph.trans (e : structomorph G M M') (e' : structomorph G M' M'') :
     have : F₁ ≈ F₂ := calc
       F₁ ≈ c.symm ≫ₕ f₁ ≫ₕ (g ≫ₕ g.symm) ≫ₕ f₂ ≫ₕ c' : by simp [F₁, trans_assoc]
       ... ≈ c.symm ≫ₕ f₁ ≫ₕ (of_set g.source g.open_source) ≫ₕ f₂ ≫ₕ c' :
-        by simp [eq_on_source_trans, trans_self_symm g]
+        by simp [eq_on_source.trans', trans_self_symm g]
       ... ≈ ((c.symm ≫ₕ f₁) ≫ₕ (of_set g.source g.open_source)) ≫ₕ (f₂ ≫ₕ c') :
         by simp [trans_assoc]
       ... ≈ ((c.symm ≫ₕ f₁).restr s) ≫ₕ (f₂ ≫ₕ c') : by simp [s, trans_of_set']
       ... ≈ ((c.symm ≫ₕ f₁) ≫ₕ (f₂ ≫ₕ c')).restr s : by simp [restr_trans]
-      ... ≈ (c.symm ≫ₕ (f₁ ≫ₕ f₂) ≫ₕ c').restr s : by simp [eq_on_source_restr, trans_assoc]
+      ... ≈ (c.symm ≫ₕ (f₁ ≫ₕ f₂) ≫ₕ c').restr s : by simp [eq_on_source.restr, trans_assoc]
       ... ≈ F₂ : by simp [F₂, feq],
     have : F₂ ∈ G := G.eq_on_source F₁ F₂ A (setoid.symm this),
     exact this

src/topology/local_homeomorph.lean

@@ -394,11 +394,11 @@ eq_of_local_equiv_eq $ local_equiv.restr_trans e.to_local_equiv e'.to_local_equi
 /-- `eq_on_source e e'` means that `e` and `e'` have the same source, and coincide there. They
 should really be considered the same local equiv. -/
 def eq_on_source (e e' : local_homeomorph α β) : Prop :=
-e.source = e'.source ∧ (∀x ∈ e.source, e x = e' x)
+e.source = e'.source ∧ (eq_on e e' e.source)
 
 lemma eq_on_source_iff (e e' : local_homeomorph α β) :
 eq_on_source e e' ↔ local_equiv.eq_on_source e.to_local_equiv e'.to_local_equiv :=
-by refl
+iff.rfl
 
 /-- `eq_on_source` is an equivalence relation -/
 instance : setoid (local_homeomorph α β) :=
@@ -412,42 +412,36 @@ instance : setoid (local_homeomorph α β) :=
 lemma eq_on_source_refl : e ≈ e := setoid.refl _
 
 /-- If two local homeomorphisms are equivalent, so are their inverses -/
-lemma eq_on_source_symm {e e' : local_homeomorph α β} (h : e ≈ e') : e.symm ≈ e'.symm :=
-local_equiv.eq_on_source_symm h
+lemma eq_on_source.symm' {e e' : local_homeomorph α β} (h : e ≈ e') : e.symm ≈ e'.symm :=
+local_equiv.eq_on_source.symm' h
 
 /-- Two equivalent local homeomorphisms have the same source -/
-lemma source_eq_of_eq_on_source {e e' : local_homeomorph α β} (h : e ≈ e') : e.source = e'.source :=
+lemma eq_on_source.source_eq {e e' : local_homeomorph α β} (h : e ≈ e') : e.source = e'.source :=
 h.1
 
 /-- Two equivalent local homeomorphisms have the same target -/
-lemma target_eq_of_eq_on_source {e e' : local_homeomorph α β} (h : e ≈ e') : e.target = e'.target :=
-(eq_on_source_symm h).1
+lemma eq_on_source.target_eq {e e' : local_homeomorph α β} (h : e ≈ e') : e.target = e'.target :=
+h.symm'.1
 
 /-- Two equivalent local homeomorphisms have coinciding `to_fun` on the source -/
-lemma apply_eq_of_eq_on_source {e e' : local_homeomorph α β} (h : e ≈ e')
-  {x : α} (hx : x ∈ e.source) : e x = e' x :=
-h.2 x hx
+lemma eq_on_source.eq_on {e e' : local_homeomorph α β} (h : e ≈ e') :
+  eq_on e e' e.source :=
+h.2
 
 /-- Two equivalent local homeomorphisms have coinciding `inv_fun` on the target -/
-lemma inv_apply_eq_of_eq_on_source {e e' : local_homeomorph α β} (h : e ≈ e')
-  {x : β} (hx : x ∈ e.target) : e.symm x = e'.symm x :=
-(eq_on_source_symm h).2 x hx
+lemma eq_on_source.symm_eq_on_target {e e' : local_homeomorph α β} (h : e ≈ e') :
+  eq_on e.symm e'.symm e.target :=
+h.symm'.2
 
 /-- Composition of local homeomorphisms respects equivalence -/
-lemma eq_on_source_trans {e e' : local_homeomorph α β} {f f' : local_homeomorph β γ}
+lemma eq_on_source.trans' {e e' : local_homeomorph α β} {f f' : local_homeomorph β γ}
   (he : e ≈ e') (hf : f ≈ f') : e.trans f ≈ e'.trans f' :=
-begin
-  change local_equiv.eq_on_source (e.trans f).to_local_equiv (e'.trans f').to_local_equiv,
-  simp only [trans_to_local_equiv],
-  apply local_equiv.eq_on_source_trans,
-  exact he,
-  exact hf
-end
+local_equiv.eq_on_source.trans' he hf
 
 /-- Restriction of local homeomorphisms respects equivalence -/
-lemma eq_on_source_restr {e e' : local_homeomorph α β} (he : e ≈ e') (s : set α) :
+lemma eq_on_source.restr {e e' : local_homeomorph α β} (he : e ≈ e') (s : set α) :
   e.restr s ≈ e'.restr s :=
-local_equiv.eq_on_source_restr he _
+local_equiv.eq_on_source.restr he _
 
 /-- Composition of a local homeomorphism and its inverse is equivalent to the restriction of the
 identity to the source -/