feat(topology/local_homeomorph): define helper definition (#14360)

* Define `homeomorph.trans_local_homeomorph` and `local_homeomorph.trans_homeomorph`. They are equal to `local_homeomorph.trans`, but with better definitional behavior for `source` and `target`.
* Define similar operations for `local_equiv`.
* Use this to improve the definitional behavior of [`topological_fiber_bundle.trivialization.trans_fiber_homeomorph`](https://leanprover-community.github.io/mathlib_docs/find/topological_fiber_bundle.trivialization.trans_fiber_homeomorph)
* Also use `@[simps]` to generate a couple of extra simp-lemmas.

src/logic/equiv/local_equiv.lean

@@ -131,17 +131,6 @@ structure local_equiv (α : Type*) (β : Type*) :=
 (left_inv'   : ∀{x}, x ∈ source → inv_fun (to_fun x) = x)
 (right_inv'  : ∀{x}, x ∈ target → to_fun (inv_fun x) = x)
 
-/-- Associating a local_equiv to an equiv-/
-def equiv.to_local_equiv (e : α ≃ β) : local_equiv α β :=
-{ to_fun      := e,
-  inv_fun     := e.symm,
-  source      := univ,
-  target      := univ,
-  map_source' := λx hx, mem_univ _,
-  map_target' := λy hy, mem_univ _,
-  left_inv'   := λx hx, e.left_inv x,
-  right_inv'  := λx hx, e.right_inv x }
-
 namespace local_equiv
 
 variables (e : local_equiv α β) (e' : local_equiv β γ)
@@ -150,9 +139,6 @@ instance [inhabited α] [inhabited β] : inhabited (local_equiv α β) :=
 ⟨⟨const α default, const β default, ∅, ∅, maps_to_empty _ _, maps_to_empty _ _,
   eq_on_empty _ _, eq_on_empty _ _⟩⟩
 
-instance inhabited_of_empty [is_empty α] [is_empty β] : inhabited (local_equiv α β) :=
-⟨((equiv.equiv_empty α).trans (equiv.equiv_empty β).symm).to_local_equiv⟩
-
 /-- The inverse of a local equiv -/
 protected def symm : local_equiv β α :=
 { to_fun     := e.inv_fun,
@@ -202,8 +188,23 @@ 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 a local_equiv to an equiv-/
+@[simps (mfld_cfg)] def _root_.equiv.to_local_equiv (e : α ≃ β) : local_equiv α β :=
+{ to_fun      := e,
+  inv_fun     := e.symm,
+  source      := univ,
+  target      := univ,
+  map_source' := λx hx, mem_univ _,
+  map_target' := λy hy, mem_univ _,
+  left_inv'   := λx hx, e.left_inv x,
+  right_inv'  := λx hx, e.right_inv x }
+
+instance inhabited_of_empty [is_empty α] [is_empty β] : inhabited (local_equiv α β) :=
+⟨((equiv.equiv_empty α).trans (equiv.equiv_empty β).symm).to_local_equiv⟩
+
 /-- Create a copy of a `local_equiv` providing better definitional equalities. -/
-@[simps] def copy (e : local_equiv α β) (f : α → β) (hf : ⇑e = f) (g : β → α) (hg : ⇑e.symm = g)
+@[simps {fully_applied := ff}]
+def copy (e : local_equiv α β) (f : α → β) (hf : ⇑e = f) (g : β → α) (hg : ⇑e.symm = g)
   (s : set α) (hs : e.source = s) (t : set β) (ht : e.target = t) :
   local_equiv α β :=
 { to_fun := f,
@@ -268,7 +269,7 @@ lemma symm_maps_to (h : e.is_image s t) : maps_to e.symm (e.target ∩ t) (e.sou
 h.symm.maps_to
 
 /-- Restrict a `local_equiv` to a pair of corresponding sets. -/
-@[simps] def restr (h : e.is_image s t) : local_equiv α β :=
+@[simps {fully_applied := ff}] def restr (h : e.is_image s t) : local_equiv α β :=
 { to_fun := e,
   inv_fun := e.symm,
   source := e.source ∩ s,
@@ -530,6 +531,25 @@ lemma restr_trans (s : set α) :
   (e.restr s).trans e' = (e.trans e').restr s :=
 local_equiv.ext (λx, rfl) (λx, rfl) $ by { simp [trans_source, inter_comm], rwa inter_assoc }
 
+/-- Postcompose a local equivalence with an equivalence.
+We modify the source and target to have better definitional behavior. -/
+@[simps] def trans_equiv (e' : β ≃ γ) : local_equiv α γ :=
+(e.trans e'.to_local_equiv).copy _ rfl _ rfl e.source (inter_univ _) (e'.symm ⁻¹' e.target)
+  (univ_inter _)
+
+lemma trans_equiv_eq_trans (e' : β ≃ γ) : e.trans_equiv e' = e.trans e'.to_local_equiv :=
+copy_eq_self _ _ _ _ _ _ _ _ _
+
+/-- Precompose a local equivalence with an equivalence.
+We modify the source and target to have better definitional behavior. -/
+@[simps] def _root_.equiv.trans_local_equiv (e : α ≃ β) : local_equiv α γ :=
+(e.to_local_equiv.trans e').copy _ rfl _ rfl (e ⁻¹' e'.source) (univ_inter _) e'.target
+  (inter_univ _)
+
+lemma _root_.equiv.trans_local_equiv_eq_trans (e : α ≃ β) :
+  e.trans_local_equiv e' = e.to_local_equiv.trans e' :=
+copy_eq_self _ _ _ _ _ _ _ _ _
+
 /-- `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 :=
@@ -669,7 +689,7 @@ end prod
 sends `e.source ∩ s` to `e.target ∩ t` using `e` and `e'.source \ s` to `e'.target \ t` using `e'`,
 and similarly for the inverse function. The definition assumes `e.is_image s t` and
 `e'.is_image s t`. -/
-@[simps] def piecewise (e e' : local_equiv α β) (s : set α) (t : set β)
+@[simps {fully_applied := ff}] def piecewise (e e' : local_equiv α β) (s : set α) (t : set β)
   [∀ x, decidable (x ∈ s)] [∀ y, decidable (y ∈ t)] (H : e.is_image s t) (H' : e'.is_image s t) :
   local_equiv α β :=
 { to_fun := s.piecewise e e',
@@ -690,7 +710,8 @@ rfl
 /-- Combine two `local_equiv`s with disjoint sources and disjoint targets. We reuse
 `local_equiv.piecewise`, then override `source` and `target` to ensure better definitional
 equalities. -/
-@[simps] def disjoint_union (e e' : local_equiv α β) (hs : disjoint e.source e'.source)
+@[simps {fully_applied := ff}]
+def disjoint_union (e e' : local_equiv α β) (hs : disjoint e.source e'.source)
   (ht : disjoint e.target e'.target) [∀ x, decidable (x ∈ e.source)]
   [∀ y, decidable (y ∈ e.target)] :
   local_equiv α β :=
@@ -710,7 +731,7 @@ section pi
 variables {ι : Type*} {αi βi : ι → Type*} (ei : Π i, local_equiv (αi i) (βi i))
 
 /-- The product of a family of local equivs, as a local equiv on the pi type. -/
-@[simps source target] protected def pi : local_equiv (Π i, αi i) (Π i, βi i) :=
+@[simps (mfld_cfg)] protected def pi : local_equiv (Π i, αi i) (Π i, βi i) :=
 { to_fun := λ f i, ei i (f i),
   inv_fun := λ f i, (ei i).symm (f i),
   source := pi univ (λ i, (ei i).source),
@@ -720,12 +741,6 @@ variables {ι : Type*} {αi βi : ι → Type*} (ei : Π i, local_equiv (αi i)
   left_inv' := λ f hf, funext $ λ i, (ei i).left_inv (hf i trivial),
   right_inv' := λ f hf, funext $ λ i, (ei i).right_inv (hf i trivial) }
 
-attribute [mfld_simps] pi_source pi_target
-
-@[simp, mfld_simps] lemma pi_coe : ⇑(local_equiv.pi ei) = λ (f : Π i, αi i) i, ei i (f i) := rfl
-@[simp, mfld_simps] lemma pi_symm :
-  (local_equiv.pi ei).symm = local_equiv.pi (λ i, (ei i).symm) := rfl
-
 end pi
 
 end local_equiv
@@ -735,8 +750,8 @@ namespace set
 -- All arguments are explicit to avoid missing information in the pretty printer output
 /-- A bijection between two sets `s : set α` and `t : set β` provides a local equivalence
 between `α` and `β`. -/
-@[simps] noncomputable def bij_on.to_local_equiv [nonempty α] (f : α → β) (s : set α) (t : set β)
-  (hf : bij_on f s t) :
+@[simps {fully_applied := ff}] noncomputable def bij_on.to_local_equiv [nonempty α] (f : α → β)
+  (s : set α) (t : set β) (hf : bij_on f s t) :
   local_equiv α β :=
 { to_fun := f,
   inv_fun := inv_fun_on f s,
@@ -758,12 +773,8 @@ end set
 namespace equiv
 /- equivs give rise to local_equiv. We set up simp lemmas to reduce most properties of the local
 equiv to that of the equiv. -/
-variables (e : equiv α β) (e' : equiv β γ)
+variables (e : α ≃ β) (e' : β ≃ γ)
 
-@[simp, mfld_simps] lemma to_local_equiv_coe : (e.to_local_equiv : α → β) = e := rfl
-@[simp, mfld_simps] lemma to_local_equiv_symm_coe : (e.to_local_equiv.symm : β → α) = e.symm := rfl
-@[simp, mfld_simps] lemma to_local_equiv_source : e.to_local_equiv.source = univ := rfl
-@[simp, mfld_simps] lemma to_local_equiv_target : e.to_local_equiv.target = univ := rfl
 @[simp, mfld_simps] lemma refl_to_local_equiv :
   (equiv.refl α).to_local_equiv = local_equiv.refl α := rfl
 @[simp, mfld_simps] lemma symm_to_local_equiv : e.symm.to_local_equiv = e.to_local_equiv.symm := rfl

src/topology/fiber_bundle.lean

@@ -243,7 +243,7 @@ end
 lemma symm_trans_symm (e e' : pretrivialization F proj) :
   (e.to_local_equiv.symm.trans e'.to_local_equiv).symm =
   e'.to_local_equiv.symm.trans e.to_local_equiv :=
-by rw [local_equiv.trans_symm_eq_symm_trans_symm,local_equiv.symm_symm]
+by rw [local_equiv.trans_symm_eq_symm_trans_symm, local_equiv.symm_symm]
 
 lemma symm_trans_source_eq (e e' : pretrivialization F proj) :
   (e.to_local_equiv.symm.trans e'.to_local_equiv).source =
@@ -447,13 +447,12 @@ namespace topological_fiber_bundle.trivialization
 that sends `p : Z` to `((e p).1, h (e p).2)`. -/
 def trans_fiber_homeomorph {F' : Type*} [topological_space F']
   (e : trivialization F proj) (h : F ≃ₜ F') : trivialization F' proj :=
-{ to_local_homeomorph := e.to_local_homeomorph.trans
-    ((homeomorph.refl _).prod_congr h).to_local_homeomorph,
+{ to_local_homeomorph := e.to_local_homeomorph.trans_homeomorph $ (homeomorph.refl _).prod_congr h,
   base_set := e.base_set,
   open_base_set := e.open_base_set,
-  source_eq := by simp [e.source_eq],
-  target_eq := by { ext, simp [e.target_eq] },
-  proj_to_fun := λ p hp, have p ∈ e.source, by simpa using hp, by simp [this] }
+  source_eq := e.source_eq,
+  target_eq := by simp [e.target_eq, prod_univ, preimage_preimage],
+  proj_to_fun := e.proj_to_fun }
 
 @[simp] lemma trans_fiber_homeomorph_apply {F' : Type*} [topological_space F']
   (e : trivialization F proj) (h : F ≃ₜ F') (x : Z) :
@@ -741,7 +740,7 @@ begin
     (mem_nhds_within_Ici_iff_exists_mem_Ioc_Ico_subset hlt).1
       (mem_nhds_within_of_mem_nhds $ is_open.mem_nhds ec.open_base_set (hec ⟨hc.1, le_rfl⟩)),
   have had : Ico a d ⊆ ec.base_set,
-    from subset.trans Ico_subset_Icc_union_Ico (union_subset hec hd),
+    from Ico_subset_Icc_union_Ico.trans (union_subset hec hd),
   by_cases he : disjoint (Iio d) (Ioi c),
   { /- If `(c, d) = ∅`, then let `ed` be a trivialization of `proj` over a neighborhood of `d`.
     Then the disjoint union of `ec` restricted to `(-∞, d)` and `ed` restricted to `(c, ∞)` is
@@ -755,7 +754,7 @@ begin
   { /- If `(c, d)` is nonempty, then take `d' ∈ (c, d)`. Since the base set of `ec` includes
     `[a, d)`, it includes `[a, d'] ⊆ [a, d)` as well. -/
     rw [disjoint_left] at he, push_neg at he, rcases he with ⟨d', hdd' : d' < d, hd'c⟩,
-    exact ⟨d', ⟨hd'c, hdd'.le.trans hdcb.2⟩, ec, subset.trans (Icc_subset_Ico_right hdd') had⟩ }
+    exact ⟨d', ⟨hd'c, hdd'.le.trans hdcb.2⟩, ec, (Icc_subset_Ico_right hdd').trans had⟩ }
 end
 
 end piecewise

src/topology/homeomorph.lean

@@ -49,8 +49,6 @@ instance : has_coe_to_fun (α ≃ₜ β) (λ _, α → β) := ⟨λe, e.to_equiv
   ((homeomorph.mk a b c) : α → β) = a :=
 rfl
 
-@[simp] lemma coe_to_equiv (h : α ≃ₜ β) : ⇑h.to_equiv = h := rfl
-
 /-- Inverse of a homeomorphism. -/
 protected def symm (h : α ≃ₜ β) : β ≃ₜ α :=
 { continuous_to_fun  := h.continuous_inv_fun,
@@ -66,6 +64,9 @@ def simps.symm_apply (h : α ≃ₜ β) : β → α := h.symm
 initialize_simps_projections homeomorph
   (to_equiv_to_fun → apply, to_equiv_inv_fun → symm_apply, -to_equiv)
 
+@[simp] lemma coe_to_equiv (h : α ≃ₜ β) : ⇑h.to_equiv = h := rfl
+@[simp] lemma coe_symm_to_equiv (h : α ≃ₜ β) : ⇑h.to_equiv.symm = h.symm := rfl
+
 lemma to_equiv_injective : function.injective (to_equiv : α ≃ₜ β → α ≃ β)
 | ⟨e, h₁, h₂⟩ ⟨e', h₁', h₂'⟩ rfl := rfl
 

src/topology/local_homeomorph.lean

@@ -57,15 +57,6 @@ structure local_homeomorph (α : Type*) (β : Type*) [topological_space α] [top
 (continuous_to_fun  : continuous_on to_fun source)
 (continuous_inv_fun : continuous_on inv_fun target)
 
-/-- A homeomorphism induces a local homeomorphism on the whole space -/
-def homeomorph.to_local_homeomorph (e : α ≃ₜ β) :
-  local_homeomorph α β :=
-{ open_source        := is_open_univ,
-  open_target        := is_open_univ,
-  continuous_to_fun  := by { erw ← continuous_iff_continuous_on_univ, exact e.continuous_to_fun },
-  continuous_inv_fun := by { erw ← continuous_iff_continuous_on_univ, exact e.continuous_inv_fun },
-  ..e.to_equiv.to_local_equiv }
-
 namespace local_homeomorph
 
 variables (e : local_homeomorph α β) (e' : local_homeomorph β γ)
@@ -100,6 +91,9 @@ lemma continuous_on_symm : continuous_on e.symm e.target := e.continuous_inv_fun
 @[simp, mfld_simps] lemma mk_coe_symm (e : local_equiv α β) (a b c d) :
   ((local_homeomorph.mk e a b c d).symm : β → α) = e.symm := rfl
 
+lemma to_local_equiv_injective : injective (to_local_equiv : local_homeomorph α β → local_equiv α β)
+| ⟨e, h₁, h₂, h₃, h₄⟩ ⟨e', h₁', h₂', h₃', h₄'⟩ rfl := rfl
+
 /- Register a few simp lemmas to make sure that `simp` puts the application of a local
 homeomorphism in its normal form, i.e., in terms of its coercion to a function. -/
 
@@ -132,6 +126,16 @@ 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
 
+/-- A homeomorphism induces a local homeomorphism on the whole space -/
+@[simps {simp_rhs := tt, .. mfld_cfg}]
+def _root_.homeomorph.to_local_homeomorph (e : α ≃ₜ β) :
+  local_homeomorph α β :=
+{ open_source        := is_open_univ,
+  open_target        := is_open_univ,
+  continuous_to_fun  := by { erw ← continuous_iff_continuous_on_univ, exact e.continuous_to_fun },
+  continuous_inv_fun := by { erw ← continuous_iff_continuous_on_univ, exact e.continuous_inv_fun },
+  ..e.to_equiv.to_local_equiv }
+
 /-- Replace `to_local_equiv` field to provide better definitional equalities. -/
 def replace_equiv (e : local_homeomorph α β) (e' : local_equiv α β) (h : e.to_local_equiv = e') :
   local_homeomorph α β :=
@@ -556,12 +560,12 @@ protected def trans' (h : e.target = e'.source) : local_homeomorph α γ :=
 { open_source       := e.open_source,
   open_target       := e'.open_target,
   continuous_to_fun := begin
-    apply continuous_on.comp e'.continuous_to_fun e.continuous_to_fun,
+    apply e'.continuous_to_fun.comp e.continuous_to_fun,
     rw ← h,
     exact e.to_local_equiv.source_subset_preimage_target
   end,
   continuous_inv_fun := begin
-    apply continuous_on.comp e.continuous_inv_fun e'.continuous_inv_fun,
+    apply e.continuous_inv_fun.comp e'.continuous_inv_fun,
     rw h,
     exact e'.to_local_equiv.target_subset_preimage_source
   end,
@@ -646,6 +650,33 @@ lemma restr_trans (s : set α) :
   (e.restr s).trans e' = (e.trans e').restr s :=
 eq_of_local_equiv_eq $ local_equiv.restr_trans e.to_local_equiv e'.to_local_equiv (interior s)
 
+/-- Postcompose a local homeomorphism with an homeomorphism.
+We modify the source and target to have better definitional behavior. -/
+@[simps {fully_applied := ff}]
+def trans_homeomorph (e' : β ≃ₜ γ) : local_homeomorph α γ :=
+{ to_local_equiv := e.to_local_equiv.trans_equiv e'.to_equiv,
+  open_source := e.open_source,
+  open_target := e.open_target.preimage e'.symm.continuous,
+  continuous_to_fun := e'.continuous.comp_continuous_on e.continuous_on,
+  continuous_inv_fun := e.symm.continuous_on.comp e'.symm.continuous.continuous_on (λ x h, h) }
+
+lemma trans_equiv_eq_trans (e' : β ≃ₜ γ) : e.trans_homeomorph e' = e.trans e'.to_local_homeomorph :=
+to_local_equiv_injective $ local_equiv.trans_equiv_eq_trans _ _
+
+/-- Precompose a local homeomorphism with an homeomorphism.
+We modify the source and target to have better definitional behavior. -/
+@[simps {fully_applied := ff}]
+def _root_.homeomorph.trans_local_homeomorph (e : α ≃ₜ β) : local_homeomorph α γ :=
+{ to_local_equiv := e.to_equiv.trans_local_equiv e'.to_local_equiv,
+  open_source := e'.open_source.preimage e.continuous,
+  open_target := e'.open_target,
+  continuous_to_fun := e'.continuous_on.comp e.continuous.continuous_on (λ x h, h),
+  continuous_inv_fun := e.symm.continuous.comp_continuous_on e'.symm.continuous_on }
+
+lemma _root_.homeomorph.trans_local_homeomorph_eq_trans (e : α ≃ₜ β) :
+  e.trans_local_homeomorph e' = e.to_local_homeomorph.trans e' :=
+to_local_equiv_injective $ equiv.trans_local_equiv_eq_trans _ _
+
 /-- `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 :=
@@ -939,10 +970,6 @@ variables (e : α ≃ₜ β) (e' : β ≃ₜ γ)
 /- Register as simp lemmas that the fields of a local homeomorphism built from a homeomorphism
 correspond to the fields of the original homeomorphism. -/
 
-attribute [simps apply source target {simp_rhs := tt, .. mfld_cfg}] to_local_homeomorph
-
-@[simp, mfld_simps] lemma to_local_homeomorph_coe_symm :
-  (e.to_local_homeomorph.symm : β → α) = e.symm := rfl
 @[simp, mfld_simps] lemma refl_to_local_homeomorph :
   (homeomorph.refl α).to_local_homeomorph = local_homeomorph.refl α := rfl
 @[simp, mfld_simps] lemma symm_to_local_homeomorph :