From 0b00e53a2acc662aa91b93cb83087ebaae01a1c7 Mon Sep 17 00:00:00 2001
From: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Thu, 10 Nov 2022 09:01:25 +0000
Subject: [PATCH] chore(topology/fiber_bundle): move trivializations to a new
 file (#17463)

Split the file `topology.fiber_bundle` into two, `topology.fiber_bundle.trivialization` and `topology.fiber_bundle.basic`, the former treating (pre)trivializations and the latter treating fiber bundles and constructions for them (the core construction, the prebundle construction, etc).  Also move lemmas from `topology.vector_bundle.basic` which turned out not to invove the linear structure (cf [this discussion](https://github.com/leanprover-community/mathlib/pull/17359#discussion_r1015622110)) into `topology.fiber_bundle.trivialization`.
---
 src/analysis/complex/re_im_topology.lean      |   2 +-
 src/topology/covering.lean                    |   2 +-
 .../basic.lean}                               | 575 +-------------
 src/topology/fiber_bundle/trivialization.lean | 711 ++++++++++++++++++
 src/topology/vector_bundle/basic.lean         | 121 +--
 5 files changed, 717 insertions(+), 694 deletions(-)
 rename src/topology/{fiber_bundle.lean => fiber_bundle/basic.lean} (57%)
 create mode 100644 src/topology/fiber_bundle/trivialization.lean

diff --git a/src/analysis/complex/re_im_topology.lean b/src/analysis/complex/re_im_topology.lean
index 2fd080de7cd45..0928eaf6950eb 100644
--- a/src/analysis/complex/re_im_topology.lean
+++ b/src/analysis/complex/re_im_topology.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import analysis.complex.basic
-import topology.fiber_bundle
+import topology.fiber_bundle.basic
 
 /-!
 # Closure, interior, and frontier of preimages under `re` and `im`
diff --git a/src/topology/covering.lean b/src/topology/covering.lean
index 47f49f76770e6..08e11cf4d66a1 100644
--- a/src/topology/covering.lean
+++ b/src/topology/covering.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 -/
 import topology.is_locally_homeomorph
-import topology.fiber_bundle
+import topology.fiber_bundle.basic
 
 /-!
 # Covering Maps
diff --git a/src/topology/fiber_bundle.lean b/src/topology/fiber_bundle/basic.lean
similarity index 57%
rename from src/topology/fiber_bundle.lean
rename to src/topology/fiber_bundle/basic.lean
index 7ef528f6338f6..dc1c63e2d6ef5 100644
--- a/src/topology/fiber_bundle.lean
+++ b/src/topology/fiber_bundle/basic.lean
@@ -3,9 +3,7 @@ Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import data.bundle
-import topology.algebra.order.basic
-import topology.local_homeomorph
+import topology.fiber_bundle.trivialization
 
 /-!
 # Fiber bundles
@@ -29,9 +27,6 @@ fiber bundle from trivializations given as local equivalences with minimum addit
 
 ### Basic definitions
 
-* `trivialization F p` : structure extending local homeomorphisms, defining a local
-                  trivialization of a topological space `Z` with projection `p` and fiber `F`.
-
 * `is_topological_fiber_bundle F p` : Prop saying that the map `p` between topological spaces is a
                   fiber bundle with fiber `F`.
 
@@ -41,21 +36,9 @@ fiber bundle from trivializations given as local equivalences with minimum addit
 
 ### Operations on bundles
 
-We provide the following operations on `trivialization`s.
-
-* `trivialization.comap`: given a local trivialization `e` of a fiber bundle `p : Z → B`, a
-  continuous map `f : B' → B` and a point `b' : B'` such that `f b' ∈ e.base_set`,
-  `e.comap f hf b' hb'` is a trivialization of the pullback bundle. The pullback bundle
-  (a.k.a., the induced bundle) has total space `{(x, y) : B' × Z | f x = p y}`, and is given by
-  `λ ⟨(x, y), h⟩, x`.
-
 * `is_topological_fiber_bundle.comap`: if `p : Z → B` is a topological fiber bundle, then its
   pullback along a continuous map `f : B' → B` is a topological fiber bundle as well.
 
-* `trivialization.comp_homeomorph`: given a local trivialization `e` of a fiber bundle
-  `p : Z → B` and a homeomorphism `h : Z' ≃ₜ Z`, returns a local trivialization of the fiber bundle
-  `p ∘ h`.
-
 * `is_topological_fiber_bundle.comp_homeomorph`: if `p : Z → B` is a topological fiber bundle
   and `h : Z' ≃ₜ Z` is a homeomorphism, then `p ∘ h : Z' → B` is a topological fiber bundle with
   the same fiber.
@@ -77,8 +60,6 @@ Let `Z : topological_fiber_bundle_core ι B F`. Then we define
 * `Z.local_triv i`: for `i : ι`, bundle trivialization above the set `Z.base_set i`, which is an
                     open set in `B`.
 
-* `pretrivialization F proj` : trivialization as a local equivalence, mainly used when the
-                                      topology on the total space has not yet been defined.
 * `topological_fiber_prebundle F proj` : structure registering a cover of prebundle trivializations
   and requiring that the relative transition maps are local homeomorphisms.
 * `topological_fiber_prebundle.total_space_topology a` : natural topology of the total space, making
@@ -86,23 +67,6 @@ Let `Z : topological_fiber_bundle_core ι B F`. Then we define
 
 ## Implementation notes
 
-### Trivializations
-
-Previously, in mathlib, there was a structure `topological_vector_bundle.trivialization` which
-extended another structure `topological_fibre_bundle.trivialization` by a linearity hypothesis. As
-of PR #17359, we have changed this to a single structure `trivialization` (no namespace), together
-with a mixin class `trivialization.is_linear`.
-
-This permits all the *data* of a vector bundle to be held at the level of fibre bundles, so that the
-same trivializations can underlie an object's structure as (say) a vector bundle over `ℂ` and as a
-vector bundle over `ℝ`, as well as its structure simply as a fibre bundle.
-
-This might be a little surprising, given the general trend of the library to ever-increased
-bundling.  But in this case the typical motivation for more bundling does not apply: there is no
-algebraic or order structure on the whole type of linear (say) trivializations of a bundle.
-Indeed, since trivializations only have meaning on their base sets (taking junk values outside), the
-type of linear trivializations is not even particularly well-behaved.
-
 ### Core construction
 
 A topological fiber bundle with fiber `F` over a base `B` is a family of spaces isomorphic to `F`,
@@ -164,7 +128,7 @@ Or for the pullback of a `topological_fiber_bundle_core`, the indexing type will
 for the initial bundle.
 
 ## Tags
-Fiber bundle, topological bundle, local trivialization, structure group
+Fiber bundle, topological bundle, structure group
 -/
 
 variables {ι : Type*} {B : Type*} {F : Type*}
@@ -177,301 +141,8 @@ open_locale topological_space classical
 section topological_fiber_bundle
 
 variables (F) {Z : Type*} [topological_space B] [topological_space F] {proj : Z → B}
-
-/-- This structure contains the information left for a local trivialization (which is implemented
-below as `trivialization F proj`) if the total space has not been given a topology, but we
-have a topology on both the fiber and the base space. Through the construction
-`topological_fiber_prebundle F proj` it will be possible to promote a
-`pretrivialization F proj` to a `trivialization F proj`. -/
-@[ext, nolint has_nonempty_instance]
-structure pretrivialization (proj : Z → B) extends local_equiv Z (B × F) :=
-(open_target   : is_open target)
-(base_set      : set B)
-(open_base_set : is_open base_set)
-(source_eq     : source = proj ⁻¹' base_set)
-(target_eq     : target = base_set ×ˢ univ)
-(proj_to_fun   : ∀ p ∈ source, (to_fun p).1 = proj p)
-
-namespace pretrivialization
-
-instance : has_coe_to_fun (pretrivialization F proj) (λ _, Z → (B × F)) := ⟨λ e, e.to_fun⟩
-
-variables {F} (e : pretrivialization F proj) {x : Z}
-
-@[simp, mfld_simps] lemma coe_coe : ⇑e.to_local_equiv = e := rfl
-@[simp, mfld_simps] lemma coe_fst (ex : x ∈ e.source) : (e x).1 = proj x := e.proj_to_fun x ex
-lemma mem_source : x ∈ e.source ↔ proj x ∈ e.base_set := by rw [e.source_eq, mem_preimage]
-lemma coe_fst' (ex : proj x ∈ e.base_set) : (e x).1 = proj x := e.coe_fst (e.mem_source.2 ex)
-protected lemma eq_on : eq_on (prod.fst ∘ e) proj e.source := λ x hx, e.coe_fst hx
-lemma mk_proj_snd (ex : x ∈ e.source) : (proj x, (e x).2) = e x := prod.ext (e.coe_fst ex).symm rfl
-lemma mk_proj_snd' (ex : proj x ∈ e.base_set) : (proj x, (e x).2) = e x :=
-prod.ext (e.coe_fst' ex).symm rfl
-
-/-- Composition of inverse and coercion from the subtype of the target. -/
-def set_symm : e.target → Z := e.target.restrict e.to_local_equiv.symm
-
-lemma mem_target {x : B × F} : x ∈ e.target ↔ x.1 ∈ e.base_set :=
-by rw [e.target_eq, prod_univ, mem_preimage]
-
-lemma proj_symm_apply {x : B × F} (hx : x ∈ e.target) : proj (e.to_local_equiv.symm x) = x.1 :=
-begin
-  have := (e.coe_fst (e.to_local_equiv.map_target hx)).symm,
-  rwa [← e.coe_coe, e.to_local_equiv.right_inv hx] at this
-end
-
-lemma proj_symm_apply' {b : B} {x : F} (hx : b ∈ e.base_set) :
-  proj (e.to_local_equiv.symm (b, x)) = b :=
-e.proj_symm_apply (e.mem_target.2 hx)
-
-lemma proj_surj_on_base_set [nonempty F] : set.surj_on proj e.source e.base_set :=
-λ b hb, let ⟨y⟩ := ‹nonempty F› in ⟨e.to_local_equiv.symm (b, y),
-  e.to_local_equiv.map_target $ e.mem_target.2 hb, e.proj_symm_apply' hb⟩
-
-lemma apply_symm_apply {x : B × F} (hx : x ∈ e.target) : e (e.to_local_equiv.symm x) = x :=
-e.to_local_equiv.right_inv hx
-
-lemma apply_symm_apply' {b : B} {x : F} (hx : b ∈ e.base_set) :
-  e (e.to_local_equiv.symm (b, x)) = (b, x) :=
-e.apply_symm_apply (e.mem_target.2 hx)
-
-lemma symm_apply_apply {x : Z} (hx : x ∈ e.source) : e.to_local_equiv.symm (e x) = x :=
-e.to_local_equiv.left_inv hx
-
-@[simp, mfld_simps] lemma symm_apply_mk_proj {x : Z} (ex : x ∈ e.source) :
-  e.to_local_equiv.symm (proj x, (e x).2) = x :=
-by rw [← e.coe_fst ex, prod.mk.eta, ← e.coe_coe, e.to_local_equiv.left_inv ex]
-
-@[simp, mfld_simps] lemma preimage_symm_proj_base_set :
-  (e.to_local_equiv.symm ⁻¹' (proj ⁻¹' e.base_set)) ∩ e.target  = e.target :=
-begin
-  refine inter_eq_right_iff_subset.mpr (λ x hx, _),
-  simp only [mem_preimage, local_equiv.inv_fun_as_coe, e.proj_symm_apply hx],
-  exact e.mem_target.mp hx,
-end
-
-@[simp, mfld_simps] lemma preimage_symm_proj_inter (s : set B) :
-  (e.to_local_equiv.symm ⁻¹' (proj ⁻¹' s)) ∩ e.base_set ×ˢ univ = (s ∩ e.base_set) ×ˢ univ :=
-begin
-  ext ⟨x, y⟩,
-  suffices : x ∈ e.base_set → (proj (e.to_local_equiv.symm (x, y)) ∈ s ↔ x ∈ s),
-    by simpa only [prod_mk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ, and.congr_left_iff],
-  intro h,
-  rw [e.proj_symm_apply' h]
-end
-
-lemma target_inter_preimage_symm_source_eq (e f : pretrivialization F proj) :
-  f.target ∩ (f.to_local_equiv.symm) ⁻¹' e.source = (e.base_set ∩ f.base_set) ×ˢ univ :=
-by rw [inter_comm, f.target_eq, e.source_eq, f.preimage_symm_proj_inter]
-
-lemma trans_source (e f : pretrivialization F proj) :
-  (f.to_local_equiv.symm.trans e.to_local_equiv).source = (e.base_set ∩ f.base_set) ×ˢ univ :=
-by rw [local_equiv.trans_source, local_equiv.symm_source, e.target_inter_preimage_symm_source_eq]
-
-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]
-
-lemma symm_trans_source_eq (e e' : pretrivialization F proj) :
-  (e.to_local_equiv.symm.trans e'.to_local_equiv).source = (e.base_set ∩ e'.base_set) ×ˢ univ :=
-by rw [local_equiv.trans_source, e'.source_eq, local_equiv.symm_source, e.target_eq, inter_comm,
-  e.preimage_symm_proj_inter, inter_comm]
-
-lemma symm_trans_target_eq (e e' : pretrivialization F proj) :
-  (e.to_local_equiv.symm.trans e'.to_local_equiv).target = (e.base_set ∩ e'.base_set) ×ˢ univ :=
-by rw [← local_equiv.symm_source, symm_trans_symm, symm_trans_source_eq, inter_comm]
-
-end pretrivialization
-
 variable [topological_space Z]
 
-/--
-A structure extending local homeomorphisms, defining a local trivialization of a projection
-`proj : Z → B` with fiber `F`, as a local homeomorphism between `Z` and `B × F` defined between two
-sets of the form `proj ⁻¹' base_set` and `base_set × F`, acting trivially on the first coordinate.
--/
-@[ext, nolint has_nonempty_instance]
-structure trivialization (proj : Z → B)
-  extends local_homeomorph Z (B × F) :=
-(base_set      : set B)
-(open_base_set : is_open base_set)
-(source_eq     : source = proj ⁻¹' base_set)
-(target_eq     : target = base_set ×ˢ univ)
-(proj_to_fun   : ∀ p ∈ source, (to_local_homeomorph p).1 = proj p)
-
-namespace trivialization
-
-variables {F} (e : trivialization F proj) {x : Z}
-
-/-- Natural identification as a `pretrivialization`. -/
-def to_pretrivialization : pretrivialization F proj := { ..e }
-
-instance : has_coe_to_fun (trivialization F proj) (λ _, Z → B × F) := ⟨λ e, e.to_fun⟩
-instance : has_coe (trivialization F proj) (pretrivialization F proj) :=
-⟨to_pretrivialization⟩
-
-lemma to_pretrivialization_injective :
-  function.injective (λ e : trivialization F proj, e.to_pretrivialization) :=
-by { intros e e', rw [pretrivialization.ext_iff, trivialization.ext_iff,
-  ← local_homeomorph.to_local_equiv_injective.eq_iff], exact id }
-
-@[simp, mfld_simps] lemma coe_coe : ⇑e.to_local_homeomorph = e := rfl
-@[simp, mfld_simps] lemma coe_fst (ex : x ∈ e.source) : (e x).1 = proj x := e.proj_to_fun x ex
-protected lemma eq_on : eq_on (prod.fst ∘ e) proj e.source := λ x hx, e.coe_fst hx
-lemma mem_source : x ∈ e.source ↔ proj x ∈ e.base_set := by rw [e.source_eq, mem_preimage]
-lemma coe_fst' (ex : proj x ∈ e.base_set) : (e x).1 = proj x := e.coe_fst (e.mem_source.2 ex)
-lemma mk_proj_snd (ex : x ∈ e.source) : (proj x, (e x).2) = e x := prod.ext (e.coe_fst ex).symm rfl
-lemma mk_proj_snd' (ex : proj x ∈ e.base_set) : (proj x, (e x).2) = e x :=
-prod.ext (e.coe_fst' ex).symm rfl
-
-lemma source_inter_preimage_target_inter (s : set (B × F)) :
-  e.source ∩ (e ⁻¹' (e.target ∩ s)) = e.source ∩ (e ⁻¹' s) :=
-e.to_local_homeomorph.source_inter_preimage_target_inter s
-
-@[simp, mfld_simps] lemma coe_mk (e : local_homeomorph Z (B × F)) (i j k l m) (x : Z) :
-  (trivialization.mk e i j k l m : trivialization F proj) x = e x := rfl
-
-lemma mem_target {x : B × F} : x ∈ e.target ↔ x.1 ∈ e.base_set :=
-e.to_pretrivialization.mem_target
-
-lemma map_target {x : B × F} (hx : x ∈ e.target) : e.to_local_homeomorph.symm x ∈ e.source :=
-e.to_local_homeomorph.map_target hx
-
-lemma proj_symm_apply {x : B × F} (hx : x ∈ e.target) : proj (e.to_local_homeomorph.symm x) = x.1 :=
-e.to_pretrivialization.proj_symm_apply hx
-
-lemma proj_symm_apply' {b : B} {x : F}
-  (hx : b ∈ e.base_set) : proj (e.to_local_homeomorph.symm (b, x)) = b :=
-e.to_pretrivialization.proj_symm_apply' hx
-
-lemma proj_surj_on_base_set [nonempty F] : set.surj_on proj e.source e.base_set :=
-e.to_pretrivialization.proj_surj_on_base_set
-
-lemma apply_symm_apply {x : B × F} (hx : x ∈ e.target) : e (e.to_local_homeomorph.symm x) = x :=
-e.to_local_homeomorph.right_inv hx
-
-lemma apply_symm_apply'
-  {b : B} {x : F} (hx : b ∈ e.base_set) : e (e.to_local_homeomorph.symm (b, x)) = (b, x) :=
-e.to_pretrivialization.apply_symm_apply' hx
-
-@[simp, mfld_simps] lemma symm_apply_mk_proj (ex : x ∈ e.source) :
-  e.to_local_homeomorph.symm (proj x, (e x).2) = x :=
-e.to_pretrivialization.symm_apply_mk_proj ex
-
-lemma symm_trans_source_eq (e e' : trivialization F proj) :
-  (e.to_local_equiv.symm.trans e'.to_local_equiv).source = (e.base_set ∩ e'.base_set) ×ˢ univ :=
-pretrivialization.symm_trans_source_eq e.to_pretrivialization e'
-
-lemma symm_trans_target_eq (e e' : trivialization F proj) :
-  (e.to_local_equiv.symm.trans e'.to_local_equiv).target = (e.base_set ∩ e'.base_set) ×ˢ univ :=
-pretrivialization.symm_trans_target_eq e.to_pretrivialization e'
-
-lemma coe_fst_eventually_eq_proj (ex : x ∈ e.source) : prod.fst ∘ e =ᶠ[𝓝 x] proj  :=
-mem_nhds_iff.2 ⟨e.source, λ y hy, e.coe_fst hy, e.open_source, ex⟩
-
-lemma coe_fst_eventually_eq_proj' (ex : proj x ∈ e.base_set) : prod.fst ∘ e =ᶠ[𝓝 x] proj :=
-e.coe_fst_eventually_eq_proj (e.mem_source.2 ex)
-
-lemma map_proj_nhds (ex : x ∈ e.source) : map proj (𝓝 x) = 𝓝 (proj x) :=
-by rw [← e.coe_fst ex, ← map_congr (e.coe_fst_eventually_eq_proj ex), ← map_map, ← e.coe_coe,
-  e.to_local_homeomorph.map_nhds_eq ex, map_fst_nhds]
-
-lemma preimage_subset_source {s : set B} (hb : s ⊆ e.base_set) : proj ⁻¹' s ⊆ e.source :=
-λ p hp, e.mem_source.mpr (hb hp)
-
-lemma image_preimage_eq_prod_univ {s : set B} (hb : s ⊆ e.base_set) :
-  e '' (proj ⁻¹' s) = s ×ˢ univ :=
-subset.antisymm (image_subset_iff.mpr (λ p hp,
-  ⟨(e.proj_to_fun p (e.preimage_subset_source hb hp)).symm ▸ hp, trivial⟩)) (λ p hp,
-  let hp' : p ∈ e.target := e.mem_target.mpr (hb hp.1) in
-  ⟨e.inv_fun p, mem_preimage.mpr ((e.proj_symm_apply hp').symm ▸ hp.1), e.apply_symm_apply hp'⟩)
-
-/-- The preimage of a subset of the base set is homeomorphic to the product with the fiber. -/
-def preimage_homeomorph {s : set B} (hb : s ⊆ e.base_set) : proj ⁻¹' s ≃ₜ s × F :=
-(e.to_local_homeomorph.homeomorph_of_image_subset_source (e.preimage_subset_source hb)
-  (e.image_preimage_eq_prod_univ hb)).trans
-  ((homeomorph.set.prod s univ).trans ((homeomorph.refl s).prod_congr (homeomorph.set.univ F)))
-
-@[simp] lemma preimage_homeomorph_apply {s : set B} (hb : s ⊆ e.base_set) (p : proj ⁻¹' s) :
-  e.preimage_homeomorph hb p = (⟨proj p, p.2⟩, (e p).2) :=
-prod.ext (subtype.ext (e.proj_to_fun p (e.mem_source.mpr (hb p.2)))) rfl
-
-@[simp] lemma preimage_homeomorph_symm_apply {s : set B} (hb : s ⊆ e.base_set) (p : s × F) :
-  (e.preimage_homeomorph hb).symm p = ⟨e.symm (p.1, p.2), ((e.preimage_homeomorph hb).symm p).2⟩ :=
-rfl
-
-/-- The source is homeomorphic to the product of the base set with the fiber. -/
-def source_homeomorph_base_set_prod : e.source ≃ₜ e.base_set × F :=
-(homeomorph.set_congr e.source_eq).trans (e.preimage_homeomorph subset_rfl)
-
-@[simp] lemma source_homeomorph_base_set_prod_apply (p : e.source) :
-  e.source_homeomorph_base_set_prod p = (⟨proj p, e.mem_source.mp p.2⟩, (e p).2) :=
-e.preimage_homeomorph_apply subset_rfl ⟨p, e.mem_source.mp p.2⟩
-
-@[simp] lemma source_homeomorph_base_set_prod_symm_apply (p : e.base_set × F) :
-  e.source_homeomorph_base_set_prod.symm p =
-    ⟨e.symm (p.1, p.2), (e.source_homeomorph_base_set_prod.symm p).2⟩ :=
-rfl
-
-/-- Each fiber of a trivialization is homeomorphic to the specified fiber. -/
-def preimage_singleton_homeomorph {b : B} (hb : b ∈ e.base_set) : proj ⁻¹' {b} ≃ₜ F :=
-(e.preimage_homeomorph (set.singleton_subset_iff.mpr hb)).trans (((homeomorph.homeomorph_of_unique
-  ({b} : set B) punit).prod_congr (homeomorph.refl F)).trans (homeomorph.punit_prod F))
-
-@[simp] lemma preimage_singleton_homeomorph_apply {b : B} (hb : b ∈ e.base_set)
-  (p : proj ⁻¹' {b}) : e.preimage_singleton_homeomorph hb p = (e p).2 :=
-rfl
-
-@[simp] lemma preimage_singleton_homeomorph_symm_apply {b : B} (hb : b ∈ e.base_set) (p : F) :
-  (e.preimage_singleton_homeomorph hb).symm p =
-    ⟨e.symm (b, p), by rw [mem_preimage, e.proj_symm_apply' hb, mem_singleton_iff]⟩ :=
-rfl
-
-/-- In the domain of a bundle trivialization, the projection is continuous-/
-lemma continuous_at_proj (ex : x ∈ e.source) : continuous_at proj x :=
-(e.map_proj_nhds ex).le
-
-/-- Composition of a `trivialization` and a `homeomorph`. -/
-def comp_homeomorph {Z' : Type*} [topological_space Z'] (h : Z' ≃ₜ Z) :
-  trivialization F (proj ∘ h) :=
-{ to_local_homeomorph := h.to_local_homeomorph.trans e.to_local_homeomorph,
-  base_set := e.base_set,
-  open_base_set := e.open_base_set,
-  source_eq := by simp [e.source_eq, preimage_preimage],
-  target_eq := by simp [e.target_eq],
-  proj_to_fun := λ p hp,
-    have hp : h p ∈ e.source, by simpa using hp,
-    by simp [hp] }
-
-/-- Read off the continuity of a function `f : Z → X` at `z : Z` by transferring via a
-trivialization of `Z` containing `z`. -/
-lemma continuous_at_of_comp_right {X : Type*} [topological_space X] {f : Z → X} {z : Z}
-  (e : trivialization F proj) (he : proj z ∈ e.base_set)
-  (hf : continuous_at (f ∘ e.to_local_equiv.symm) (e z)) :
-  continuous_at f z :=
-begin
-  have hez : z ∈ e.to_local_equiv.symm.target,
-  { rw [local_equiv.symm_target, e.mem_source],
-    exact he },
-  rwa [e.to_local_homeomorph.symm.continuous_at_iff_continuous_at_comp_right hez,
-   local_homeomorph.symm_symm]
-end
-
-/-- Read off the continuity of a function `f : X → Z` at `x : X` by transferring via a
-trivialization of `Z` containing `f x`. -/
-lemma continuous_at_of_comp_left {X : Type*} [topological_space X] {f : X → Z} {x : X}
-  (e : trivialization F proj) (hf_proj : continuous_at (proj ∘ f) x) (he : proj (f x) ∈ e.base_set)
-  (hf : continuous_at (e ∘ f) x) :
-  continuous_at f x :=
-begin
-  rw e.to_local_homeomorph.continuous_at_iff_continuous_at_comp_left,
-  { exact hf },
-  rw [e.source_eq, ← preimage_comp],
-  exact hf_proj.preimage_mem_nhds (e.open_base_set.mem_nhds he),
-end
-
-end trivialization
-
 /-- A topological fiber bundle with fiber `F` over a base `B` is a space projecting on `B`
 for which the fibers are all homeomorphic to `F`, such that the local situation around each point
 is a direct product. -/
@@ -544,152 +215,12 @@ lemma is_topological_fiber_bundle.comp_homeomorph {Z' : Type*} [topological_spac
 λ x, let ⟨e, he⟩ := e x in
 ⟨e.comp_homeomorph h, by simpa [trivialization.comp_homeomorph] using he⟩
 
-namespace trivialization
-
-/-- If `e` is a `trivialization` of `proj : Z → B` with fiber `F` and `h` is a homeomorphism
-`F ≃ₜ F'`, then `e.trans_fiber_homeomorph h` is the trivialization of `proj` with the fiber `F'`
-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 $ (homeomorph.refl _).prod_congr h,
-  base_set := e.base_set,
-  open_base_set := e.open_base_set,
-  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) :
-  e.trans_fiber_homeomorph h x = ((e x).1, h (e x).2) :=
-rfl
-
-/-- Coordinate transformation in the fiber induced by a pair of bundle trivializations. See also
-`trivialization.coord_change_homeomorph` for a version bundled as `F ≃ₜ F`. -/
-def coord_change (e₁ e₂ : trivialization F proj) (b : B) (x : F) : F :=
-(e₂ $ e₁.to_local_homeomorph.symm (b, x)).2
-
-lemma mk_coord_change
-  (e₁ e₂ : trivialization F proj) {b : B}
-  (h₁ : b ∈ e₁.base_set) (h₂ : b ∈ e₂.base_set) (x : F) :
-  (b, e₁.coord_change e₂ b x) = e₂ (e₁.to_local_homeomorph.symm (b, x)) :=
-begin
-  refine prod.ext _ rfl,
-  rw [e₂.coe_fst', ← e₁.coe_fst', e₁.apply_symm_apply' h₁],
-  { rwa [e₁.proj_symm_apply' h₁] },
-  { rwa [e₁.proj_symm_apply' h₁] }
-end
-
-lemma coord_change_apply_snd
-  (e₁ e₂ : trivialization F proj) {p : Z}
-  (h : proj p ∈ e₁.base_set) :
-  e₁.coord_change e₂ (proj p) (e₁ p).snd = (e₂ p).snd :=
-by rw [coord_change, e₁.symm_apply_mk_proj (e₁.mem_source.2 h)]
-
-lemma coord_change_same_apply
-  (e : trivialization F proj) {b : B} (h : b ∈ e.base_set) (x : F) :
-  e.coord_change e b x = x :=
-by rw [coord_change, e.apply_symm_apply' h]
-
-lemma coord_change_same
-  (e : trivialization F proj) {b : B} (h : b ∈ e.base_set) :
-  e.coord_change e b = id :=
-funext $ e.coord_change_same_apply h
-
-lemma coord_change_coord_change
-  (e₁ e₂ e₃ : trivialization F proj) {b : B}
-  (h₁ : b ∈ e₁.base_set) (h₂ : b ∈ e₂.base_set) (x : F) :
-  e₂.coord_change e₃ b (e₁.coord_change e₂ b x) = e₁.coord_change e₃ b x :=
-begin
-  rw [coord_change, e₁.mk_coord_change _ h₁ h₂, ← e₂.coe_coe,
-    e₂.to_local_homeomorph.left_inv, coord_change],
-  rwa [e₂.mem_source, e₁.proj_symm_apply' h₁]
-end
-
-lemma continuous_coord_change (e₁ e₂ : trivialization F proj) {b : B}
-  (h₁ : b ∈ e₁.base_set) (h₂ : b ∈ e₂.base_set) :
-  continuous (e₁.coord_change e₂ b) :=
-begin
-  refine continuous_snd.comp (e₂.to_local_homeomorph.continuous_on.comp_continuous
-    (e₁.to_local_homeomorph.continuous_on_symm.comp_continuous _ _) _),
-  { exact continuous_const.prod_mk continuous_id },
-  { exact λ x, e₁.mem_target.2 h₁ },
-  { intro x,
-    rwa [e₂.mem_source, e₁.proj_symm_apply' h₁] }
-end
-
-/-- Coordinate transformation in the fiber induced by a pair of bundle trivializations,
-as a homeomorphism. -/
-def coord_change_homeomorph
-  (e₁ e₂ : trivialization F proj) {b : B} (h₁ : b ∈ e₁.base_set) (h₂ : b ∈ e₂.base_set) :
-  F ≃ₜ F :=
-{ to_fun := e₁.coord_change e₂ b,
-  inv_fun := e₂.coord_change e₁ b,
-  left_inv := λ x, by simp only [*, coord_change_coord_change, coord_change_same_apply],
-  right_inv := λ x, by simp only [*, coord_change_coord_change, coord_change_same_apply],
-  continuous_to_fun := e₁.continuous_coord_change e₂ h₁ h₂,
-  continuous_inv_fun := e₂.continuous_coord_change e₁ h₂ h₁ }
-
-@[simp] lemma coord_change_homeomorph_coe
-  (e₁ e₂ : trivialization F proj) {b : B} (h₁ : b ∈ e₁.base_set) (h₂ : b ∈ e₂.base_set) :
-  ⇑(e₁.coord_change_homeomorph e₂ h₁ h₂) = e₁.coord_change e₂ b :=
-rfl
-
-end trivialization
-
 section comap
 
 open_locale classical
 
 variables {B' : Type*} [topological_space B']
 
-/-- Given a bundle trivialization of `proj : Z → B` and a continuous map `f : B' → B`,
-construct a bundle trivialization of `φ : {p : B' × Z | f p.1 = proj p.2} → B'`
-given by `φ x = (x : B' × Z).1`. -/
-noncomputable def trivialization.comap
-  (e : trivialization F proj) (f : B' → B) (hf : continuous f)
-  (b' : B') (hb' : f b' ∈ e.base_set) :
-  trivialization F (λ x : {p : B' × Z | f p.1 = proj p.2}, (x : B' × Z).1) :=
-{ to_fun := λ p, ((p : B' × Z).1, (e (p : B' × Z).2).2),
-  inv_fun := λ p, if h : f p.1 ∈ e.base_set
-    then ⟨⟨p.1, e.to_local_homeomorph.symm (f p.1, p.2)⟩, by simp [e.proj_symm_apply' h]⟩
-    else ⟨⟨b', e.to_local_homeomorph.symm (f b', p.2)⟩, by simp [e.proj_symm_apply' hb']⟩,
-  source := {p | f (p : B' × Z).1 ∈ e.base_set},
-  target := {p | f p.1 ∈ e.base_set},
-  map_source' := λ p hp, hp,
-  map_target' := λ p (hp : f p.1 ∈ e.base_set), by simp [hp],
-  left_inv' :=
-    begin
-      rintro ⟨⟨b, x⟩, hbx⟩ hb,
-      dsimp at *,
-      have hx : x ∈ e.source, from e.mem_source.2 (hbx ▸ hb),
-      ext; simp *
-    end,
-  right_inv' := λ p (hp : f p.1 ∈ e.base_set), by simp [*, e.apply_symm_apply'],
-  open_source := e.open_base_set.preimage (hf.comp $ continuous_fst.comp continuous_subtype_coe),
-  open_target := e.open_base_set.preimage (hf.comp continuous_fst),
-  continuous_to_fun := ((continuous_fst.comp continuous_subtype_coe).continuous_on).prod $
-    continuous_snd.comp_continuous_on $ e.continuous_to_fun.comp
-      (continuous_snd.comp continuous_subtype_coe).continuous_on $
-      by { rintro ⟨⟨b, x⟩, (hbx : f b = proj x)⟩ (hb : f b ∈ e.base_set),
-           rw hbx at hb,
-           exact e.mem_source.2 hb },
-  continuous_inv_fun :=
-    begin
-      rw [embedding_subtype_coe.continuous_on_iff],
-      suffices : continuous_on (λ p : B' × F, (p.1, e.to_local_homeomorph.symm (f p.1, p.2)))
-        {p : B' × F | f p.1 ∈ e.base_set},
-      { refine this.congr (λ p (hp : f p.1 ∈ e.base_set), _),
-        simp [hp] },
-      { refine continuous_on_fst.prod (e.to_local_homeomorph.symm.continuous_on.comp _ _),
-        { exact ((hf.comp continuous_fst).prod_mk continuous_snd).continuous_on },
-        { exact λ p hp, e.mem_target.2 hp } }
-    end,
-  base_set := f ⁻¹' e.base_set,
-  source_eq := rfl,
-  target_eq := by { ext, simp },
-  open_base_set := e.open_base_set.preimage hf,
-  proj_to_fun := λ _ _, rfl }
-
 /-- If `proj : Z → B` is a topological fiber bundle with fiber `F` and `f : B' → B` is a continuous
 map, then the pullback bundle (a.k.a. induced bundle) is the topological bundle with the total space
 `{(x, y) : B' × Z | f x = proj y}` given by `λ ⟨(x, y), h⟩, x`. -/
@@ -700,105 +231,9 @@ lemma is_topological_fiber_bundle.comap (h : is_topological_fiber_bundle F proj)
 
 end comap
 
-namespace trivialization
-
-lemma is_image_preimage_prod (e : trivialization F proj) (s : set B) :
-  e.to_local_homeomorph.is_image (proj ⁻¹' s) (s ×ˢ univ) :=
-λ x hx, by simp [e.coe_fst', hx]
-
-/-- Restrict a `trivialization` to an open set in the base. `-/
-def restr_open (e : trivialization F proj) (s : set B)
-  (hs : is_open s) : trivialization F proj :=
-{ to_local_homeomorph := ((e.is_image_preimage_prod s).symm.restr
-    (is_open.inter e.open_target (hs.prod is_open_univ))).symm,
-  base_set := e.base_set ∩ s,
-  open_base_set := is_open.inter e.open_base_set hs,
-  source_eq := by simp [e.source_eq],
-  target_eq := by simp [e.target_eq, prod_univ],
-  proj_to_fun := λ p hp, e.proj_to_fun p hp.1 }
-
-section piecewise
-
-lemma frontier_preimage (e : trivialization F proj) (s : set B) :
-  e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.base_set ∩ frontier s) :=
-by rw [← (e.is_image_preimage_prod s).frontier.preimage_eq, frontier_prod_univ_eq,
-  (e.is_image_preimage_prod _).preimage_eq, e.source_eq, preimage_inter]
-
-/-- Given two bundle trivializations `e`, `e'` of `proj : Z → B` and a set `s : set B` such that
-the base sets of `e` and `e'` intersect `frontier s` on the same set and `e p = e' p` whenever
-`proj p ∈ e.base_set ∩ frontier s`, `e.piecewise e' s Hs Heq` is the bundle trivialization over
-`set.ite s e.base_set e'.base_set` that is equal to `e` on `proj ⁻¹ s` and is equal to `e'`
-otherwise. -/
-noncomputable def piecewise (e e' : trivialization F proj) (s : set B)
-  (Hs : e.base_set ∩ frontier s = e'.base_set ∩ frontier s)
-  (Heq : eq_on e e' $ proj ⁻¹' (e.base_set ∩ frontier s)) :
-  trivialization F proj :=
-{ to_local_homeomorph := e.to_local_homeomorph.piecewise e'.to_local_homeomorph
-    (proj ⁻¹' s) (s ×ˢ univ) (e.is_image_preimage_prod s) (e'.is_image_preimage_prod s)
-    (by rw [e.frontier_preimage, e'.frontier_preimage, Hs])
-    (by rwa e.frontier_preimage),
-  base_set := s.ite e.base_set e'.base_set,
-  open_base_set := e.open_base_set.ite e'.open_base_set Hs,
-  source_eq := by simp [e.source_eq, e'.source_eq],
-  target_eq := by simp [e.target_eq, e'.target_eq, prod_univ],
-  proj_to_fun := by rintro p (⟨he, hs⟩|⟨he, hs⟩); simp * }
-
-/-- Given two bundle trivializations `e`, `e'` of a topological fiber bundle `proj : Z → B`
-over a linearly ordered base `B` and a point `a ∈ e.base_set ∩ e'.base_set` such that
-`e` equals `e'` on `proj ⁻¹' {a}`, `e.piecewise_le_of_eq e' a He He' Heq` is the bundle
-trivialization over `set.ite (Iic a) e.base_set e'.base_set` that is equal to `e` on points `p`
-such that `proj p ≤ a` and is equal to `e'` otherwise. -/
-noncomputable def piecewise_le_of_eq [linear_order B] [order_topology B]
-  (e e' : trivialization F proj) (a : B) (He : a ∈ e.base_set) (He' : a ∈ e'.base_set)
-  (Heq : ∀ p, proj p = a → e p = e' p) :
-  trivialization F proj :=
-e.piecewise e' (Iic a)
-  (set.ext $ λ x, and.congr_left_iff.2 $ λ hx,
-    by simp [He, He', mem_singleton_iff.1 (frontier_Iic_subset _ hx)])
-  (λ p hp, Heq p $ frontier_Iic_subset _ hp.2)
-
-/-- Given two bundle trivializations `e`, `e'` of a topological fiber bundle `proj : Z → B` over a
-linearly ordered base `B` and a point `a ∈ e.base_set ∩ e'.base_set`, `e.piecewise_le e' a He He'`
-is the bundle trivialization over `set.ite (Iic a) e.base_set e'.base_set` that is equal to `e` on
-points `p` such that `proj p ≤ a` and is equal to `((e' p).1, h (e' p).2)` otherwise, where
-`h = `e'.coord_change_homeomorph e _ _` is the homeomorphism of the fiber such that
-`h (e' p).2 = (e p).2` whenever `e p = a`. -/
-noncomputable def piecewise_le [linear_order B] [order_topology B]
-  (e e' : trivialization F proj) (a : B) (He : a ∈ e.base_set) (He' : a ∈ e'.base_set) :
-  trivialization F proj :=
-e.piecewise_le_of_eq (e'.trans_fiber_homeomorph (e'.coord_change_homeomorph e He' He))
-  a He He' $ by { unfreezingI {rintro p rfl },
-    ext1,
-    { simp [e.coe_fst', e'.coe_fst', *] },
-    { simp [e'.coord_change_apply_snd, *] } }
-
-/-- Given two bundle trivializations `e`, `e'` over disjoint sets, `e.disjoint_union e' H` is the
-bundle trivialization over the union of the base sets that agrees with `e` and `e'` over their
-base sets. -/
-noncomputable def disjoint_union (e e' : trivialization F proj)
-  (H : disjoint e.base_set e'.base_set) :
-  trivialization F proj :=
-{ to_local_homeomorph := e.to_local_homeomorph.disjoint_union e'.to_local_homeomorph
-    (λ x hx, by { rw [e.source_eq, e'.source_eq] at hx, exact H hx })
-    (λ x hx, by { rw [e.target_eq, e'.target_eq] at hx, exact H ⟨hx.1.1, hx.2.1⟩ }),
-  base_set := e.base_set ∪ e'.base_set,
-  open_base_set := is_open.union e.open_base_set e'.open_base_set,
-  source_eq := congr_arg2 (∪) e.source_eq e'.source_eq,
-  target_eq := (congr_arg2 (∪) e.target_eq e'.target_eq).trans union_prod.symm,
-  proj_to_fun :=
-    begin
-      rintro p (hp|hp'),
-      { show (e.source.piecewise e e' p).1 = proj p,
-        rw [piecewise_eq_of_mem, e.coe_fst]; exact hp },
-      { show (e.source.piecewise e e' p).1 = proj p,
-        rw [piecewise_eq_of_not_mem, e'.coe_fst hp'],
-        simp only [e.source_eq, e'.source_eq] at hp' ⊢,
-        exact λ h, H ⟨h, hp'⟩ }
-    end }
-
 /-- If `h` is a topological fiber bundle over a conditionally complete linear order,
 then it is trivial over any closed interval. -/
-lemma _root_.is_topological_fiber_bundle.exists_trivialization_Icc_subset
+lemma is_topological_fiber_bundle.exists_trivialization_Icc_subset
   [conditionally_complete_linear_order B] [order_topology B]
   (h : is_topological_fiber_bundle F proj) (a b : B) :
   ∃ e : trivialization F proj, Icc a b ⊆ e.base_set :=
@@ -860,10 +295,6 @@ begin
     exact ⟨d', ⟨hd'c, hdd'.le.trans hdcb.2⟩, ec, (Icc_subset_Ico_right hdd').trans had⟩ }
 end
 
-end piecewise
-
-end trivialization
-
 end topological_fiber_bundle
 
 /-! ### Constructing topological fiber bundles -/
diff --git a/src/topology/fiber_bundle/trivialization.lean b/src/topology/fiber_bundle/trivialization.lean
new file mode 100644
index 0000000000000..dde58207b3a37
--- /dev/null
+++ b/src/topology/fiber_bundle/trivialization.lean
@@ -0,0 +1,711 @@
+/-
+Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sébastien Gouëzel
+-/
+import data.bundle
+import topology.algebra.order.basic
+import topology.local_homeomorph
+
+/-!
+# Trivializations
+
+## Main definitions
+
+### Basic definitions
+
+* `trivialization F p` : structure extending local homeomorphisms, defining a local
+                  trivialization of a topological space `Z` with projection `p` and fiber `F`.
+
+* `pretrivialization F proj` : trivialization as a local equivalence, mainly used when the
+                                      topology on the total space has not yet been defined.
+
+### Operations on bundles
+
+We provide the following operations on `trivialization`s.
+
+* `trivialization.comap`: given a local trivialization `e` of a fiber bundle `p : Z → B`, a
+  continuous map `f : B' → B` and a point `b' : B'` such that `f b' ∈ e.base_set`,
+  `e.comap f hf b' hb'` is a trivialization of the pullback bundle. The pullback bundle
+  (a.k.a., the induced bundle) has total space `{(x, y) : B' × Z | f x = p y}`, and is given by
+  `λ ⟨(x, y), h⟩, x`.
+
+* `trivialization.comp_homeomorph`: given a local trivialization `e` of a fiber bundle
+  `p : Z → B` and a homeomorphism `h : Z' ≃ₜ Z`, returns a local trivialization of the fiber bundle
+  `p ∘ h`.
+
+## Implementation notes
+
+Previously, in mathlib, there was a structure `topological_vector_bundle.trivialization` which
+extended another structure `topological_fibre_bundle.trivialization` by a linearity hypothesis. As
+of PR #17359, we have changed this to a single structure `trivialization` (no namespace), together
+with a mixin class `trivialization.is_linear`.
+
+This permits all the *data* of a vector bundle to be held at the level of fibre bundles, so that the
+same trivializations can underlie an object's structure as (say) a vector bundle over `ℂ` and as a
+vector bundle over `ℝ`, as well as its structure simply as a fibre bundle.
+
+This might be a little surprising, given the general trend of the library to ever-increased
+bundling.  But in this case the typical motivation for more bundling does not apply: there is no
+algebraic or order structure on the whole type of linear (say) trivializations of a bundle.
+Indeed, since trivializations only have meaning on their base sets (taking junk values outside), the
+type of linear trivializations is not even particularly well-behaved.
+
+-/
+
+open topological_space filter set bundle
+open_locale topological_space classical bundle
+
+variables {ι : Type*} {B : Type*} {F : Type*} {E : B → Type*}
+variables (F) {Z : Type*} [topological_space B] [topological_space F] {proj : Z → B}
+
+/-- This structure contains the information left for a local trivialization (which is implemented
+below as `trivialization F proj`) if the total space has not been given a topology, but we
+have a topology on both the fiber and the base space. Through the construction
+`topological_fiber_prebundle F proj` it will be possible to promote a
+`pretrivialization F proj` to a `trivialization F proj`. -/
+@[ext, nolint has_nonempty_instance]
+structure pretrivialization (proj : Z → B) extends local_equiv Z (B × F) :=
+(open_target   : is_open target)
+(base_set      : set B)
+(open_base_set : is_open base_set)
+(source_eq     : source = proj ⁻¹' base_set)
+(target_eq     : target = base_set ×ˢ univ)
+(proj_to_fun   : ∀ p ∈ source, (to_fun p).1 = proj p)
+
+namespace pretrivialization
+
+instance : has_coe_to_fun (pretrivialization F proj) (λ _, Z → (B × F)) := ⟨λ e, e.to_fun⟩
+
+variables {F} (e : pretrivialization F proj) {x : Z}
+
+@[simp, mfld_simps] lemma coe_coe : ⇑e.to_local_equiv = e := rfl
+@[simp, mfld_simps] lemma coe_fst (ex : x ∈ e.source) : (e x).1 = proj x := e.proj_to_fun x ex
+lemma mem_source : x ∈ e.source ↔ proj x ∈ e.base_set := by rw [e.source_eq, mem_preimage]
+lemma coe_fst' (ex : proj x ∈ e.base_set) : (e x).1 = proj x := e.coe_fst (e.mem_source.2 ex)
+protected lemma eq_on : eq_on (prod.fst ∘ e) proj e.source := λ x hx, e.coe_fst hx
+lemma mk_proj_snd (ex : x ∈ e.source) : (proj x, (e x).2) = e x := prod.ext (e.coe_fst ex).symm rfl
+lemma mk_proj_snd' (ex : proj x ∈ e.base_set) : (proj x, (e x).2) = e x :=
+prod.ext (e.coe_fst' ex).symm rfl
+
+/-- Composition of inverse and coercion from the subtype of the target. -/
+def set_symm : e.target → Z := e.target.restrict e.to_local_equiv.symm
+
+lemma mem_target {x : B × F} : x ∈ e.target ↔ x.1 ∈ e.base_set :=
+by rw [e.target_eq, prod_univ, mem_preimage]
+
+lemma proj_symm_apply {x : B × F} (hx : x ∈ e.target) : proj (e.to_local_equiv.symm x) = x.1 :=
+begin
+  have := (e.coe_fst (e.to_local_equiv.map_target hx)).symm,
+  rwa [← e.coe_coe, e.to_local_equiv.right_inv hx] at this
+end
+
+lemma proj_symm_apply' {b : B} {x : F} (hx : b ∈ e.base_set) :
+  proj (e.to_local_equiv.symm (b, x)) = b :=
+e.proj_symm_apply (e.mem_target.2 hx)
+
+lemma proj_surj_on_base_set [nonempty F] : set.surj_on proj e.source e.base_set :=
+λ b hb, let ⟨y⟩ := ‹nonempty F› in ⟨e.to_local_equiv.symm (b, y),
+  e.to_local_equiv.map_target $ e.mem_target.2 hb, e.proj_symm_apply' hb⟩
+
+lemma apply_symm_apply {x : B × F} (hx : x ∈ e.target) : e (e.to_local_equiv.symm x) = x :=
+e.to_local_equiv.right_inv hx
+
+lemma apply_symm_apply' {b : B} {x : F} (hx : b ∈ e.base_set) :
+  e (e.to_local_equiv.symm (b, x)) = (b, x) :=
+e.apply_symm_apply (e.mem_target.2 hx)
+
+lemma symm_apply_apply {x : Z} (hx : x ∈ e.source) : e.to_local_equiv.symm (e x) = x :=
+e.to_local_equiv.left_inv hx
+
+@[simp, mfld_simps] lemma symm_apply_mk_proj {x : Z} (ex : x ∈ e.source) :
+  e.to_local_equiv.symm (proj x, (e x).2) = x :=
+by rw [← e.coe_fst ex, prod.mk.eta, ← e.coe_coe, e.to_local_equiv.left_inv ex]
+
+@[simp, mfld_simps] lemma preimage_symm_proj_base_set :
+  (e.to_local_equiv.symm ⁻¹' (proj ⁻¹' e.base_set)) ∩ e.target  = e.target :=
+begin
+  refine inter_eq_right_iff_subset.mpr (λ x hx, _),
+  simp only [mem_preimage, local_equiv.inv_fun_as_coe, e.proj_symm_apply hx],
+  exact e.mem_target.mp hx,
+end
+
+@[simp, mfld_simps] lemma preimage_symm_proj_inter (s : set B) :
+  (e.to_local_equiv.symm ⁻¹' (proj ⁻¹' s)) ∩ e.base_set ×ˢ univ = (s ∩ e.base_set) ×ˢ univ :=
+begin
+  ext ⟨x, y⟩,
+  suffices : x ∈ e.base_set → (proj (e.to_local_equiv.symm (x, y)) ∈ s ↔ x ∈ s),
+    by simpa only [prod_mk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ, and.congr_left_iff],
+  intro h,
+  rw [e.proj_symm_apply' h]
+end
+
+lemma target_inter_preimage_symm_source_eq (e f : pretrivialization F proj) :
+  f.target ∩ (f.to_local_equiv.symm) ⁻¹' e.source = (e.base_set ∩ f.base_set) ×ˢ univ :=
+by rw [inter_comm, f.target_eq, e.source_eq, f.preimage_symm_proj_inter]
+
+lemma trans_source (e f : pretrivialization F proj) :
+  (f.to_local_equiv.symm.trans e.to_local_equiv).source = (e.base_set ∩ f.base_set) ×ˢ univ :=
+by rw [local_equiv.trans_source, local_equiv.symm_source, e.target_inter_preimage_symm_source_eq]
+
+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]
+
+lemma symm_trans_source_eq (e e' : pretrivialization F proj) :
+  (e.to_local_equiv.symm.trans e'.to_local_equiv).source = (e.base_set ∩ e'.base_set) ×ˢ univ :=
+by rw [local_equiv.trans_source, e'.source_eq, local_equiv.symm_source, e.target_eq, inter_comm,
+  e.preimage_symm_proj_inter, inter_comm]
+
+lemma symm_trans_target_eq (e e' : pretrivialization F proj) :
+  (e.to_local_equiv.symm.trans e'.to_local_equiv).target = (e.base_set ∩ e'.base_set) ×ˢ univ :=
+by rw [← local_equiv.symm_source, symm_trans_symm, symm_trans_source_eq, inter_comm]
+
+variables {B F} (e' : pretrivialization F (π E)) {x' : total_space E} {b : B} {y : E b}
+
+lemma coe_mem_source : ↑y ∈ e'.source ↔ b ∈ e'.base_set := e'.mem_source
+
+@[simp, mfld_simps] lemma coe_coe_fst (hb : b ∈ e'.base_set) : (e' y).1 = b :=
+e'.coe_fst (e'.mem_source.2 hb)
+
+lemma mk_mem_target {x : B} {y : F} : (x, y) ∈ e'.target ↔ x ∈ e'.base_set :=
+e'.mem_target
+
+lemma symm_coe_proj {x : B} {y : F} (e' : pretrivialization F (π E)) (h : x ∈ e'.base_set) :
+  (e'.to_local_equiv.symm (x, y)).1 = x :=
+e'.proj_symm_apply' h
+
+section has_zero
+variables [∀ x, has_zero (E x)]
+
+/-- A fiberwise inverse to `e`. This is the function `F → E b` that induces a local inverse
+`B × F → total_space E` of `e` on `e.base_set`. It is defined to be `0` outside `e.base_set`. -/
+protected noncomputable def symm (e : pretrivialization F (π E)) (b : B) (y : F) : E b :=
+if hb : b ∈ e.base_set
+then cast (congr_arg E (e.proj_symm_apply' hb)) (e.to_local_equiv.symm (b, y)).2
+else 0
+
+lemma symm_apply (e : pretrivialization F (π E)) {b : B} (hb : b ∈ e.base_set) (y : F) :
+  e.symm b y = cast (congr_arg E (e.symm_coe_proj hb)) (e.to_local_equiv.symm (b, y)).2 :=
+dif_pos hb
+
+lemma symm_apply_of_not_mem (e : pretrivialization F (π E)) {b : B} (hb : b ∉ e.base_set) (y : F) :
+  e.symm b y = 0 :=
+dif_neg hb
+
+lemma coe_symm_of_not_mem (e : pretrivialization F (π E)) {b : B} (hb : b ∉ e.base_set) :
+  (e.symm b : F → E b) = 0 :=
+funext $ λ y, dif_neg hb
+
+lemma mk_symm (e : pretrivialization F (π E)) {b : B} (hb : b ∈ e.base_set) (y : F) :
+  total_space_mk b (e.symm b y) = e.to_local_equiv.symm (b, y) :=
+by rw [e.symm_apply hb, total_space.mk_cast, total_space.eta]
+
+lemma symm_proj_apply (e : pretrivialization F (π E)) (z : total_space E)
+  (hz : z.proj ∈ e.base_set) : e.symm z.proj (e z).2 = z.2 :=
+by rw [e.symm_apply hz, cast_eq_iff_heq, e.mk_proj_snd' hz,
+  e.symm_apply_apply (e.mem_source.mpr hz)]
+
+lemma symm_apply_apply_mk (e : pretrivialization F (π E)) {b : B} (hb : b ∈ e.base_set) (y : E b) :
+  e.symm b (e (total_space_mk b y)).2 = y :=
+e.symm_proj_apply (total_space_mk b y) hb
+
+lemma apply_mk_symm (e : pretrivialization F (π E)) {b : B} (hb : b ∈ e.base_set) (y : F) :
+  e (total_space_mk b (e.symm b y)) = (b, y) :=
+by rw [e.mk_symm hb, e.apply_symm_apply (e.mk_mem_target.mpr hb)]
+
+end has_zero
+
+end pretrivialization
+
+variables [topological_space Z] [topological_space (total_space E)]
+
+/--
+A structure extending local homeomorphisms, defining a local trivialization of a projection
+`proj : Z → B` with fiber `F`, as a local homeomorphism between `Z` and `B × F` defined between two
+sets of the form `proj ⁻¹' base_set` and `base_set × F`, acting trivially on the first coordinate.
+-/
+@[ext, nolint has_nonempty_instance]
+structure trivialization (proj : Z → B)
+  extends local_homeomorph Z (B × F) :=
+(base_set      : set B)
+(open_base_set : is_open base_set)
+(source_eq     : source = proj ⁻¹' base_set)
+(target_eq     : target = base_set ×ˢ univ)
+(proj_to_fun   : ∀ p ∈ source, (to_local_homeomorph p).1 = proj p)
+
+namespace trivialization
+
+variables {F} (e : trivialization F proj) {x : Z}
+
+/-- Natural identification as a `pretrivialization`. -/
+def to_pretrivialization : pretrivialization F proj := { ..e }
+
+instance : has_coe_to_fun (trivialization F proj) (λ _, Z → B × F) := ⟨λ e, e.to_fun⟩
+instance : has_coe (trivialization F proj) (pretrivialization F proj) :=
+⟨to_pretrivialization⟩
+
+lemma to_pretrivialization_injective :
+  function.injective (λ e : trivialization F proj, e.to_pretrivialization) :=
+by { intros e e', rw [pretrivialization.ext_iff, trivialization.ext_iff,
+  ← local_homeomorph.to_local_equiv_injective.eq_iff], exact id }
+
+@[simp, mfld_simps] lemma coe_coe : ⇑e.to_local_homeomorph = e := rfl
+@[simp, mfld_simps] lemma coe_fst (ex : x ∈ e.source) : (e x).1 = proj x := e.proj_to_fun x ex
+protected lemma eq_on : eq_on (prod.fst ∘ e) proj e.source := λ x hx, e.coe_fst hx
+lemma mem_source : x ∈ e.source ↔ proj x ∈ e.base_set := by rw [e.source_eq, mem_preimage]
+lemma coe_fst' (ex : proj x ∈ e.base_set) : (e x).1 = proj x := e.coe_fst (e.mem_source.2 ex)
+lemma mk_proj_snd (ex : x ∈ e.source) : (proj x, (e x).2) = e x := prod.ext (e.coe_fst ex).symm rfl
+lemma mk_proj_snd' (ex : proj x ∈ e.base_set) : (proj x, (e x).2) = e x :=
+prod.ext (e.coe_fst' ex).symm rfl
+
+lemma source_inter_preimage_target_inter (s : set (B × F)) :
+  e.source ∩ (e ⁻¹' (e.target ∩ s)) = e.source ∩ (e ⁻¹' s) :=
+e.to_local_homeomorph.source_inter_preimage_target_inter s
+
+@[simp, mfld_simps] lemma coe_mk (e : local_homeomorph Z (B × F)) (i j k l m) (x : Z) :
+  (trivialization.mk e i j k l m : trivialization F proj) x = e x := rfl
+
+lemma mem_target {x : B × F} : x ∈ e.target ↔ x.1 ∈ e.base_set :=
+e.to_pretrivialization.mem_target
+
+lemma map_target {x : B × F} (hx : x ∈ e.target) : e.to_local_homeomorph.symm x ∈ e.source :=
+e.to_local_homeomorph.map_target hx
+
+lemma proj_symm_apply {x : B × F} (hx : x ∈ e.target) : proj (e.to_local_homeomorph.symm x) = x.1 :=
+e.to_pretrivialization.proj_symm_apply hx
+
+lemma proj_symm_apply' {b : B} {x : F}
+  (hx : b ∈ e.base_set) : proj (e.to_local_homeomorph.symm (b, x)) = b :=
+e.to_pretrivialization.proj_symm_apply' hx
+
+lemma proj_surj_on_base_set [nonempty F] : set.surj_on proj e.source e.base_set :=
+e.to_pretrivialization.proj_surj_on_base_set
+
+lemma apply_symm_apply {x : B × F} (hx : x ∈ e.target) : e (e.to_local_homeomorph.symm x) = x :=
+e.to_local_homeomorph.right_inv hx
+
+lemma apply_symm_apply'
+  {b : B} {x : F} (hx : b ∈ e.base_set) : e (e.to_local_homeomorph.symm (b, x)) = (b, x) :=
+e.to_pretrivialization.apply_symm_apply' hx
+
+@[simp, mfld_simps] lemma symm_apply_mk_proj (ex : x ∈ e.source) :
+  e.to_local_homeomorph.symm (proj x, (e x).2) = x :=
+e.to_pretrivialization.symm_apply_mk_proj ex
+
+lemma symm_trans_source_eq (e e' : trivialization F proj) :
+  (e.to_local_equiv.symm.trans e'.to_local_equiv).source = (e.base_set ∩ e'.base_set) ×ˢ univ :=
+pretrivialization.symm_trans_source_eq e.to_pretrivialization e'
+
+lemma symm_trans_target_eq (e e' : trivialization F proj) :
+  (e.to_local_equiv.symm.trans e'.to_local_equiv).target = (e.base_set ∩ e'.base_set) ×ˢ univ :=
+pretrivialization.symm_trans_target_eq e.to_pretrivialization e'
+
+lemma coe_fst_eventually_eq_proj (ex : x ∈ e.source) : prod.fst ∘ e =ᶠ[𝓝 x] proj  :=
+mem_nhds_iff.2 ⟨e.source, λ y hy, e.coe_fst hy, e.open_source, ex⟩
+
+lemma coe_fst_eventually_eq_proj' (ex : proj x ∈ e.base_set) : prod.fst ∘ e =ᶠ[𝓝 x] proj :=
+e.coe_fst_eventually_eq_proj (e.mem_source.2 ex)
+
+lemma map_proj_nhds (ex : x ∈ e.source) : map proj (𝓝 x) = 𝓝 (proj x) :=
+by rw [← e.coe_fst ex, ← map_congr (e.coe_fst_eventually_eq_proj ex), ← map_map, ← e.coe_coe,
+  e.to_local_homeomorph.map_nhds_eq ex, map_fst_nhds]
+
+lemma preimage_subset_source {s : set B} (hb : s ⊆ e.base_set) : proj ⁻¹' s ⊆ e.source :=
+λ p hp, e.mem_source.mpr (hb hp)
+
+lemma image_preimage_eq_prod_univ {s : set B} (hb : s ⊆ e.base_set) :
+  e '' (proj ⁻¹' s) = s ×ˢ univ :=
+subset.antisymm (image_subset_iff.mpr (λ p hp,
+  ⟨(e.proj_to_fun p (e.preimage_subset_source hb hp)).symm ▸ hp, trivial⟩)) (λ p hp,
+  let hp' : p ∈ e.target := e.mem_target.mpr (hb hp.1) in
+  ⟨e.inv_fun p, mem_preimage.mpr ((e.proj_symm_apply hp').symm ▸ hp.1), e.apply_symm_apply hp'⟩)
+
+/-- The preimage of a subset of the base set is homeomorphic to the product with the fiber. -/
+def preimage_homeomorph {s : set B} (hb : s ⊆ e.base_set) : proj ⁻¹' s ≃ₜ s × F :=
+(e.to_local_homeomorph.homeomorph_of_image_subset_source (e.preimage_subset_source hb)
+  (e.image_preimage_eq_prod_univ hb)).trans
+  ((homeomorph.set.prod s univ).trans ((homeomorph.refl s).prod_congr (homeomorph.set.univ F)))
+
+@[simp] lemma preimage_homeomorph_apply {s : set B} (hb : s ⊆ e.base_set) (p : proj ⁻¹' s) :
+  e.preimage_homeomorph hb p = (⟨proj p, p.2⟩, (e p).2) :=
+prod.ext (subtype.ext (e.proj_to_fun p (e.mem_source.mpr (hb p.2)))) rfl
+
+@[simp] lemma preimage_homeomorph_symm_apply {s : set B} (hb : s ⊆ e.base_set) (p : s × F) :
+  (e.preimage_homeomorph hb).symm p = ⟨e.symm (p.1, p.2), ((e.preimage_homeomorph hb).symm p).2⟩ :=
+rfl
+
+/-- The source is homeomorphic to the product of the base set with the fiber. -/
+def source_homeomorph_base_set_prod : e.source ≃ₜ e.base_set × F :=
+(homeomorph.set_congr e.source_eq).trans (e.preimage_homeomorph subset_rfl)
+
+@[simp] lemma source_homeomorph_base_set_prod_apply (p : e.source) :
+  e.source_homeomorph_base_set_prod p = (⟨proj p, e.mem_source.mp p.2⟩, (e p).2) :=
+e.preimage_homeomorph_apply subset_rfl ⟨p, e.mem_source.mp p.2⟩
+
+@[simp] lemma source_homeomorph_base_set_prod_symm_apply (p : e.base_set × F) :
+  e.source_homeomorph_base_set_prod.symm p =
+    ⟨e.symm (p.1, p.2), (e.source_homeomorph_base_set_prod.symm p).2⟩ :=
+rfl
+
+/-- Each fiber of a trivialization is homeomorphic to the specified fiber. -/
+def preimage_singleton_homeomorph {b : B} (hb : b ∈ e.base_set) : proj ⁻¹' {b} ≃ₜ F :=
+(e.preimage_homeomorph (set.singleton_subset_iff.mpr hb)).trans (((homeomorph.homeomorph_of_unique
+  ({b} : set B) punit).prod_congr (homeomorph.refl F)).trans (homeomorph.punit_prod F))
+
+@[simp] lemma preimage_singleton_homeomorph_apply {b : B} (hb : b ∈ e.base_set)
+  (p : proj ⁻¹' {b}) : e.preimage_singleton_homeomorph hb p = (e p).2 :=
+rfl
+
+@[simp] lemma preimage_singleton_homeomorph_symm_apply {b : B} (hb : b ∈ e.base_set) (p : F) :
+  (e.preimage_singleton_homeomorph hb).symm p =
+    ⟨e.symm (b, p), by rw [mem_preimage, e.proj_symm_apply' hb, mem_singleton_iff]⟩ :=
+rfl
+
+/-- In the domain of a bundle trivialization, the projection is continuous-/
+lemma continuous_at_proj (ex : x ∈ e.source) : continuous_at proj x :=
+(e.map_proj_nhds ex).le
+
+/-- Composition of a `trivialization` and a `homeomorph`. -/
+protected def comp_homeomorph {Z' : Type*} [topological_space Z'] (h : Z' ≃ₜ Z) :
+  trivialization F (proj ∘ h) :=
+{ to_local_homeomorph := h.to_local_homeomorph.trans e.to_local_homeomorph,
+  base_set := e.base_set,
+  open_base_set := e.open_base_set,
+  source_eq := by simp [e.source_eq, preimage_preimage],
+  target_eq := by simp [e.target_eq],
+  proj_to_fun := λ p hp,
+    have hp : h p ∈ e.source, by simpa using hp,
+    by simp [hp] }
+
+/-- Read off the continuity of a function `f : Z → X` at `z : Z` by transferring via a
+trivialization of `Z` containing `z`. -/
+lemma continuous_at_of_comp_right {X : Type*} [topological_space X] {f : Z → X} {z : Z}
+  (e : trivialization F proj) (he : proj z ∈ e.base_set)
+  (hf : continuous_at (f ∘ e.to_local_equiv.symm) (e z)) :
+  continuous_at f z :=
+begin
+  have hez : z ∈ e.to_local_equiv.symm.target,
+  { rw [local_equiv.symm_target, e.mem_source],
+    exact he },
+  rwa [e.to_local_homeomorph.symm.continuous_at_iff_continuous_at_comp_right hez,
+   local_homeomorph.symm_symm]
+end
+
+/-- Read off the continuity of a function `f : X → Z` at `x : X` by transferring via a
+trivialization of `Z` containing `f x`. -/
+lemma continuous_at_of_comp_left {X : Type*} [topological_space X] {f : X → Z} {x : X}
+  (e : trivialization F proj) (hf_proj : continuous_at (proj ∘ f) x) (he : proj (f x) ∈ e.base_set)
+  (hf : continuous_at (e ∘ f) x) :
+  continuous_at f x :=
+begin
+  rw e.to_local_homeomorph.continuous_at_iff_continuous_at_comp_left,
+  { exact hf },
+  rw [e.source_eq, ← preimage_comp],
+  exact hf_proj.preimage_mem_nhds (e.open_base_set.mem_nhds he),
+end
+
+variables {E} (e' : trivialization F (π E)) {x' : total_space E} {b : B} {y : E b}
+
+protected lemma continuous_on : continuous_on e' e'.source := e'.continuous_to_fun
+
+lemma coe_mem_source : ↑y ∈ e'.source ↔ b ∈ e'.base_set := e'.mem_source
+
+lemma open_target : is_open e'.target :=
+by { rw e'.target_eq, exact e'.open_base_set.prod is_open_univ }
+
+@[simp, mfld_simps] lemma coe_coe_fst (hb : b ∈ e'.base_set) : (e' y).1 = b :=
+e'.coe_fst (e'.mem_source.2 hb)
+
+lemma mk_mem_target {y : F} : (b, y) ∈ e'.target ↔ b ∈ e'.base_set :=
+e'.to_pretrivialization.mem_target
+
+lemma symm_apply_apply {x : total_space E} (hx : x ∈ e'.source) :
+  e'.to_local_homeomorph.symm (e' x) = x :=
+e'.to_local_equiv.left_inv hx
+
+@[simp, mfld_simps] lemma symm_coe_proj {x : B} {y : F}
+  (e : trivialization F (π E)) (h : x ∈ e.base_set) :
+  (e.to_local_homeomorph.symm (x, y)).1 = x := e.proj_symm_apply' h
+
+section has_zero
+variables [∀ x, has_zero (E x)]
+
+/-- A fiberwise inverse to `e'`. The function `F → E x` that induces a local inverse
+`B × F → total_space E` of `e'` on `e'.base_set`. It is defined to be `0` outside `e'.base_set`. -/
+protected noncomputable def symm (e : trivialization F (π E)) (b : B) (y : F) : E b :=
+e.to_pretrivialization.symm b y
+
+lemma symm_apply (e : trivialization F (π E)) {b : B} (hb : b ∈ e.base_set) (y : F) :
+  e.symm b y = cast (congr_arg E (e.symm_coe_proj hb)) (e.to_local_homeomorph.symm (b, y)).2 :=
+dif_pos hb
+
+lemma symm_apply_of_not_mem (e : trivialization F (π E)) {b : B} (hb : b ∉ e.base_set) (y : F) :
+  e.symm b y = 0 :=
+dif_neg hb
+
+lemma mk_symm (e : trivialization F (π E)) {b : B} (hb : b ∈ e.base_set) (y : F) :
+  total_space_mk b (e.symm b y) = e.to_local_homeomorph.symm (b, y) :=
+e.to_pretrivialization.mk_symm hb y
+
+lemma symm_proj_apply (e : trivialization F (π E)) (z : total_space E)
+  (hz : z.proj ∈ e.base_set) : e.symm z.proj (e z).2 = z.2 :=
+e.to_pretrivialization.symm_proj_apply z hz
+
+lemma symm_apply_apply_mk (e : trivialization F (π E)) {b : B} (hb : b ∈ e.base_set) (y : E b) :
+  e.symm b (e (total_space_mk b y)).2 = y :=
+e.symm_proj_apply (total_space_mk b y) hb
+
+lemma apply_mk_symm (e : trivialization F (π E)) {b : B} (hb : b ∈ e.base_set) (y : F) :
+  e (total_space_mk b (e.symm b y)) = (b, y) :=
+e.to_pretrivialization.apply_mk_symm hb y
+
+lemma continuous_on_symm (e : trivialization F (π E)) :
+  continuous_on (λ z : B × F, total_space_mk z.1 (e.symm z.1 z.2)) (e.base_set ×ˢ univ) :=
+begin
+  have : ∀ (z : B × F) (hz : z ∈ e.base_set ×ˢ (univ : set F)),
+    total_space_mk z.1 (e.symm z.1 z.2) = e.to_local_homeomorph.symm z,
+  { rintro x ⟨hx : x.1 ∈ e.base_set, _⟩, simp_rw [e.mk_symm hx, prod.mk.eta] },
+  refine continuous_on.congr _ this,
+  rw [← e.target_eq],
+  exact e.to_local_homeomorph.continuous_on_symm
+end
+
+end has_zero
+
+/-- If `e` is a `trivialization` of `proj : Z → B` with fiber `F` and `h` is a homeomorphism
+`F ≃ₜ F'`, then `e.trans_fiber_homeomorph h` is the trivialization of `proj` with the fiber `F'`
+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 $ (homeomorph.refl _).prod_congr h,
+  base_set := e.base_set,
+  open_base_set := e.open_base_set,
+  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) :
+  e.trans_fiber_homeomorph h x = ((e x).1, h (e x).2) :=
+rfl
+
+/-- Coordinate transformation in the fiber induced by a pair of bundle trivializations. See also
+`trivialization.coord_change_homeomorph` for a version bundled as `F ≃ₜ F`. -/
+def coord_change (e₁ e₂ : trivialization F proj) (b : B) (x : F) : F :=
+(e₂ $ e₁.to_local_homeomorph.symm (b, x)).2
+
+lemma mk_coord_change
+  (e₁ e₂ : trivialization F proj) {b : B}
+  (h₁ : b ∈ e₁.base_set) (h₂ : b ∈ e₂.base_set) (x : F) :
+  (b, e₁.coord_change e₂ b x) = e₂ (e₁.to_local_homeomorph.symm (b, x)) :=
+begin
+  refine prod.ext _ rfl,
+  rw [e₂.coe_fst', ← e₁.coe_fst', e₁.apply_symm_apply' h₁],
+  { rwa [e₁.proj_symm_apply' h₁] },
+  { rwa [e₁.proj_symm_apply' h₁] }
+end
+
+lemma coord_change_apply_snd
+  (e₁ e₂ : trivialization F proj) {p : Z}
+  (h : proj p ∈ e₁.base_set) :
+  e₁.coord_change e₂ (proj p) (e₁ p).snd = (e₂ p).snd :=
+by rw [coord_change, e₁.symm_apply_mk_proj (e₁.mem_source.2 h)]
+
+lemma coord_change_same_apply
+  (e : trivialization F proj) {b : B} (h : b ∈ e.base_set) (x : F) :
+  e.coord_change e b x = x :=
+by rw [coord_change, e.apply_symm_apply' h]
+
+lemma coord_change_same
+  (e : trivialization F proj) {b : B} (h : b ∈ e.base_set) :
+  e.coord_change e b = id :=
+funext $ e.coord_change_same_apply h
+
+lemma coord_change_coord_change
+  (e₁ e₂ e₃ : trivialization F proj) {b : B}
+  (h₁ : b ∈ e₁.base_set) (h₂ : b ∈ e₂.base_set) (x : F) :
+  e₂.coord_change e₃ b (e₁.coord_change e₂ b x) = e₁.coord_change e₃ b x :=
+begin
+  rw [coord_change, e₁.mk_coord_change _ h₁ h₂, ← e₂.coe_coe,
+    e₂.to_local_homeomorph.left_inv, coord_change],
+  rwa [e₂.mem_source, e₁.proj_symm_apply' h₁]
+end
+
+lemma continuous_coord_change (e₁ e₂ : trivialization F proj) {b : B}
+  (h₁ : b ∈ e₁.base_set) (h₂ : b ∈ e₂.base_set) :
+  continuous (e₁.coord_change e₂ b) :=
+begin
+  refine continuous_snd.comp (e₂.to_local_homeomorph.continuous_on.comp_continuous
+    (e₁.to_local_homeomorph.continuous_on_symm.comp_continuous _ _) _),
+  { exact continuous_const.prod_mk continuous_id },
+  { exact λ x, e₁.mem_target.2 h₁ },
+  { intro x,
+    rwa [e₂.mem_source, e₁.proj_symm_apply' h₁] }
+end
+
+/-- Coordinate transformation in the fiber induced by a pair of bundle trivializations,
+as a homeomorphism. -/
+protected def coord_change_homeomorph
+  (e₁ e₂ : trivialization F proj) {b : B} (h₁ : b ∈ e₁.base_set) (h₂ : b ∈ e₂.base_set) :
+  F ≃ₜ F :=
+{ to_fun := e₁.coord_change e₂ b,
+  inv_fun := e₂.coord_change e₁ b,
+  left_inv := λ x, by simp only [*, coord_change_coord_change, coord_change_same_apply],
+  right_inv := λ x, by simp only [*, coord_change_coord_change, coord_change_same_apply],
+  continuous_to_fun := e₁.continuous_coord_change e₂ h₁ h₂,
+  continuous_inv_fun := e₂.continuous_coord_change e₁ h₂ h₁ }
+
+@[simp] lemma coord_change_homeomorph_coe
+  (e₁ e₂ : trivialization F proj) {b : B} (h₁ : b ∈ e₁.base_set) (h₂ : b ∈ e₂.base_set) :
+  ⇑(e₁.coord_change_homeomorph e₂ h₁ h₂) = e₁.coord_change e₂ b :=
+rfl
+
+variables {F} {B' : Type*} [topological_space B']
+
+/-- Given a bundle trivialization of `proj : Z → B` and a continuous map `f : B' → B`,
+construct a bundle trivialization of `φ : {p : B' × Z | f p.1 = proj p.2} → B'`
+given by `φ x = (x : B' × Z).1`. -/
+protected noncomputable def comap
+  (e : trivialization F proj) (f : B' → B) (hf : continuous f)
+  (b' : B') (hb' : f b' ∈ e.base_set) :
+  trivialization F (λ x : {p : B' × Z | f p.1 = proj p.2}, (x : B' × Z).1) :=
+{ to_fun := λ p, ((p : B' × Z).1, (e (p : B' × Z).2).2),
+  inv_fun := λ p, if h : f p.1 ∈ e.base_set
+    then ⟨⟨p.1, e.to_local_homeomorph.symm (f p.1, p.2)⟩, by simp [e.proj_symm_apply' h]⟩
+    else ⟨⟨b', e.to_local_homeomorph.symm (f b', p.2)⟩, by simp [e.proj_symm_apply' hb']⟩,
+  source := {p | f (p : B' × Z).1 ∈ e.base_set},
+  target := {p | f p.1 ∈ e.base_set},
+  map_source' := λ p hp, hp,
+  map_target' := λ p (hp : f p.1 ∈ e.base_set), by simp [hp],
+  left_inv' :=
+    begin
+      rintro ⟨⟨b, x⟩, hbx⟩ hb,
+      dsimp at *,
+      have hx : x ∈ e.source, from e.mem_source.2 (hbx ▸ hb),
+      ext; simp *
+    end,
+  right_inv' := λ p (hp : f p.1 ∈ e.base_set), by simp [*, e.apply_symm_apply'],
+  open_source := e.open_base_set.preimage (hf.comp $ continuous_fst.comp continuous_subtype_coe),
+  open_target := e.open_base_set.preimage (hf.comp continuous_fst),
+  continuous_to_fun := ((continuous_fst.comp continuous_subtype_coe).continuous_on).prod $
+    continuous_snd.comp_continuous_on $ e.continuous_to_fun.comp
+      (continuous_snd.comp continuous_subtype_coe).continuous_on $
+      by { rintro ⟨⟨b, x⟩, (hbx : f b = proj x)⟩ (hb : f b ∈ e.base_set),
+           rw hbx at hb,
+           exact e.mem_source.2 hb },
+  continuous_inv_fun :=
+    begin
+      rw [embedding_subtype_coe.continuous_on_iff],
+      suffices : continuous_on (λ p : B' × F, (p.1, e.to_local_homeomorph.symm (f p.1, p.2)))
+        {p : B' × F | f p.1 ∈ e.base_set},
+      { refine this.congr (λ p (hp : f p.1 ∈ e.base_set), _),
+        simp [hp] },
+      { refine continuous_on_fst.prod (e.to_local_homeomorph.symm.continuous_on.comp _ _),
+        { exact ((hf.comp continuous_fst).prod_mk continuous_snd).continuous_on },
+        { exact λ p hp, e.mem_target.2 hp } }
+    end,
+  base_set := f ⁻¹' e.base_set,
+  source_eq := rfl,
+  target_eq := by { ext, simp },
+  open_base_set := e.open_base_set.preimage hf,
+  proj_to_fun := λ _ _, rfl }
+
+lemma is_image_preimage_prod (e : trivialization F proj) (s : set B) :
+  e.to_local_homeomorph.is_image (proj ⁻¹' s) (s ×ˢ univ) :=
+λ x hx, by simp [e.coe_fst', hx]
+
+/-- Restrict a `trivialization` to an open set in the base. `-/
+protected def restr_open (e : trivialization F proj) (s : set B)
+  (hs : is_open s) : trivialization F proj :=
+{ to_local_homeomorph := ((e.is_image_preimage_prod s).symm.restr
+    (is_open.inter e.open_target (hs.prod is_open_univ))).symm,
+  base_set := e.base_set ∩ s,
+  open_base_set := is_open.inter e.open_base_set hs,
+  source_eq := by simp [e.source_eq],
+  target_eq := by simp [e.target_eq, prod_univ],
+  proj_to_fun := λ p hp, e.proj_to_fun p hp.1 }
+
+section piecewise
+
+lemma frontier_preimage (e : trivialization F proj) (s : set B) :
+  e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.base_set ∩ frontier s) :=
+by rw [← (e.is_image_preimage_prod s).frontier.preimage_eq, frontier_prod_univ_eq,
+  (e.is_image_preimage_prod _).preimage_eq, e.source_eq, preimage_inter]
+
+/-- Given two bundle trivializations `e`, `e'` of `proj : Z → B` and a set `s : set B` such that
+the base sets of `e` and `e'` intersect `frontier s` on the same set and `e p = e' p` whenever
+`proj p ∈ e.base_set ∩ frontier s`, `e.piecewise e' s Hs Heq` is the bundle trivialization over
+`set.ite s e.base_set e'.base_set` that is equal to `e` on `proj ⁻¹ s` and is equal to `e'`
+otherwise. -/
+noncomputable def piecewise (e e' : trivialization F proj) (s : set B)
+  (Hs : e.base_set ∩ frontier s = e'.base_set ∩ frontier s)
+  (Heq : eq_on e e' $ proj ⁻¹' (e.base_set ∩ frontier s)) :
+  trivialization F proj :=
+{ to_local_homeomorph := e.to_local_homeomorph.piecewise e'.to_local_homeomorph
+    (proj ⁻¹' s) (s ×ˢ univ) (e.is_image_preimage_prod s) (e'.is_image_preimage_prod s)
+    (by rw [e.frontier_preimage, e'.frontier_preimage, Hs])
+    (by rwa e.frontier_preimage),
+  base_set := s.ite e.base_set e'.base_set,
+  open_base_set := e.open_base_set.ite e'.open_base_set Hs,
+  source_eq := by simp [e.source_eq, e'.source_eq],
+  target_eq := by simp [e.target_eq, e'.target_eq, prod_univ],
+  proj_to_fun := by rintro p (⟨he, hs⟩|⟨he, hs⟩); simp * }
+
+/-- Given two bundle trivializations `e`, `e'` of a topological fiber bundle `proj : Z → B`
+over a linearly ordered base `B` and a point `a ∈ e.base_set ∩ e'.base_set` such that
+`e` equals `e'` on `proj ⁻¹' {a}`, `e.piecewise_le_of_eq e' a He He' Heq` is the bundle
+trivialization over `set.ite (Iic a) e.base_set e'.base_set` that is equal to `e` on points `p`
+such that `proj p ≤ a` and is equal to `e'` otherwise. -/
+noncomputable def piecewise_le_of_eq [linear_order B] [order_topology B]
+  (e e' : trivialization F proj) (a : B) (He : a ∈ e.base_set) (He' : a ∈ e'.base_set)
+  (Heq : ∀ p, proj p = a → e p = e' p) :
+  trivialization F proj :=
+e.piecewise e' (Iic a)
+  (set.ext $ λ x, and.congr_left_iff.2 $ λ hx,
+    by simp [He, He', mem_singleton_iff.1 (frontier_Iic_subset _ hx)])
+  (λ p hp, Heq p $ frontier_Iic_subset _ hp.2)
+
+/-- Given two bundle trivializations `e`, `e'` of a topological fiber bundle `proj : Z → B` over a
+linearly ordered base `B` and a point `a ∈ e.base_set ∩ e'.base_set`, `e.piecewise_le e' a He He'`
+is the bundle trivialization over `set.ite (Iic a) e.base_set e'.base_set` that is equal to `e` on
+points `p` such that `proj p ≤ a` and is equal to `((e' p).1, h (e' p).2)` otherwise, where
+`h = `e'.coord_change_homeomorph e _ _` is the homeomorphism of the fiber such that
+`h (e' p).2 = (e p).2` whenever `e p = a`. -/
+noncomputable def piecewise_le [linear_order B] [order_topology B]
+  (e e' : trivialization F proj) (a : B) (He : a ∈ e.base_set) (He' : a ∈ e'.base_set) :
+  trivialization F proj :=
+e.piecewise_le_of_eq (e'.trans_fiber_homeomorph (e'.coord_change_homeomorph e He' He))
+  a He He' $ by { unfreezingI {rintro p rfl },
+    ext1,
+    { simp [e.coe_fst', e'.coe_fst', *] },
+    { simp [e'.coord_change_apply_snd, *] } }
+
+/-- Given two bundle trivializations `e`, `e'` over disjoint sets, `e.disjoint_union e' H` is the
+bundle trivialization over the union of the base sets that agrees with `e` and `e'` over their
+base sets. -/
+noncomputable def disjoint_union (e e' : trivialization F proj)
+  (H : disjoint e.base_set e'.base_set) :
+  trivialization F proj :=
+{ to_local_homeomorph := e.to_local_homeomorph.disjoint_union e'.to_local_homeomorph
+    (λ x hx, by { rw [e.source_eq, e'.source_eq] at hx, exact H hx })
+    (λ x hx, by { rw [e.target_eq, e'.target_eq] at hx, exact H ⟨hx.1.1, hx.2.1⟩ }),
+  base_set := e.base_set ∪ e'.base_set,
+  open_base_set := is_open.union e.open_base_set e'.open_base_set,
+  source_eq := congr_arg2 (∪) e.source_eq e'.source_eq,
+  target_eq := (congr_arg2 (∪) e.target_eq e'.target_eq).trans union_prod.symm,
+  proj_to_fun :=
+    begin
+      rintro p (hp|hp'),
+      { show (e.source.piecewise e e' p).1 = proj p,
+        rw [piecewise_eq_of_mem, e.coe_fst]; exact hp },
+      { show (e.source.piecewise e e' p).1 = proj p,
+        rw [piecewise_eq_of_not_mem, e'.coe_fst hp'],
+        simp only [e.source_eq, e'.source_eq] at hp' ⊢,
+        exact λ h, H ⟨h, hp'⟩ }
+    end }
+
+end piecewise
+
+end trivialization
diff --git a/src/topology/vector_bundle/basic.lean b/src/topology/vector_bundle/basic.lean
index a0e6693ced58d..a991754e88e12 100644
--- a/src/topology/vector_bundle/basic.lean
+++ b/src/topology/vector_bundle/basic.lean
@@ -5,7 +5,7 @@ Authors: Nicolò Cavalleri, Sebastien Gouezel, Heather Macbeth, Patrick Massot,
 -/
 
 import analysis.normed_space.bounded_linear_maps
-import topology.fiber_bundle
+import topology.fiber_bundle.basic
 
 /-!
 # Topological vector bundles
@@ -69,59 +69,6 @@ lemma linear [add_comm_monoid F] [module R F] [∀ x, add_comm_monoid (E x)] [
   is_linear_map R (λ x : E b, (e (total_space_mk b x)).2) :=
 pretrivialization.is_linear.linear b hb
 
-lemma coe_mem_source : ↑y ∈ e.source ↔ b ∈ e.base_set := e.mem_source
-
-@[simp, mfld_simps] lemma coe_coe_fst (hb : b ∈ e.base_set) : (e y).1 = b :=
-e.coe_fst (e.mem_source.2 hb)
-
-lemma mk_mem_target {x : B} {y : F} : (x, y) ∈ e.target ↔ x ∈ e.base_set :=
-e.mem_target
-
-lemma symm_coe_proj {x : B} {y : F} (e : pretrivialization F (π E)) (h : x ∈ e.base_set) :
-  (e.to_local_equiv.symm (x, y)).1 = x :=
-e.proj_symm_apply' h
-
-section has_zero
-variables [∀ x, has_zero (E x)]
-
-/-- A fiberwise inverse to `e`. This is the function `F → E b` that induces a local inverse
-`B × F → total_space E` of `e` on `e.base_set`. It is defined to be `0` outside `e.base_set`. -/
-protected def symm (e : pretrivialization F (π E)) (b : B) (y : F) : E b :=
-if hb : b ∈ e.base_set
-then cast (congr_arg E (e.proj_symm_apply' hb)) (e.to_local_equiv.symm (b, y)).2
-else 0
-
-lemma symm_apply (e : pretrivialization F (π E)) {b : B} (hb : b ∈ e.base_set) (y : F) :
-  e.symm b y = cast (congr_arg E (e.symm_coe_proj hb)) (e.to_local_equiv.symm (b, y)).2 :=
-dif_pos hb
-
-lemma symm_apply_of_not_mem (e : pretrivialization F (π E)) {b : B} (hb : b ∉ e.base_set) (y : F) :
-  e.symm b y = 0 :=
-dif_neg hb
-
-lemma coe_symm_of_not_mem (e : pretrivialization F (π E)) {b : B} (hb : b ∉ e.base_set) :
-  (e.symm b : F → E b) = 0 :=
-funext $ λ y, dif_neg hb
-
-lemma mk_symm (e : pretrivialization F (π E)) {b : B} (hb : b ∈ e.base_set) (y : F) :
-  total_space_mk b (e.symm b y) = e.to_local_equiv.symm (b, y) :=
-by rw [e.symm_apply hb, total_space.mk_cast, total_space.eta]
-
-lemma symm_proj_apply (e : pretrivialization F (π E)) (z : total_space E)
-  (hz : z.proj ∈ e.base_set) : e.symm z.proj (e z).2 = z.2 :=
-by rw [e.symm_apply hz, cast_eq_iff_heq, e.mk_proj_snd' hz,
-  e.symm_apply_apply (e.mem_source.mpr hz)]
-
-lemma symm_apply_apply_mk (e : pretrivialization F (π E)) {b : B} (hb : b ∈ e.base_set) (y : E b) :
-  e.symm b (e (total_space_mk b y)).2 = y :=
-e.symm_proj_apply (total_space_mk b y) hb
-
-lemma apply_mk_symm (e : pretrivialization F (π E)) {b : B} (hb : b ∈ e.base_set) (y : F) :
-  e (total_space_mk b (e.symm b y)) = (b, y) :=
-by rw [e.mk_symm hb, e.apply_symm_apply (e.mk_mem_target.mpr hb)]
-
-end has_zero
-
 variables [add_comm_monoid F] [module R F] [∀ x, add_comm_monoid (E x)] [∀ x, module R (E x)]
 
 /-- A fiberwise linear inverse to `e`. -/
@@ -215,72 +162,6 @@ instance to_pretrivialization.is_linear [add_comm_monoid F] [module R F]
   e.to_pretrivialization.is_linear R :=
 { ..(‹_› : e.is_linear R) }
 
-protected lemma continuous_on : continuous_on e e.source := e.continuous_to_fun
-
-lemma coe_mem_source : ↑y ∈ e.source ↔ b ∈ e.base_set := e.mem_source
-
-lemma open_target : is_open e.target :=
-by { rw e.target_eq, exact e.open_base_set.prod is_open_univ }
-
-@[simp, mfld_simps] lemma coe_coe_fst (hb : b ∈ e.base_set) : (e y).1 = b :=
-e.coe_fst (e.mem_source.2 hb)
-
-lemma mk_mem_target {y : F} : (b, y) ∈ e.target ↔ b ∈ e.base_set :=
-e.to_pretrivialization.mem_target
-
-lemma symm_apply_apply {x : total_space E} (hx : x ∈ e.source) :
-  e.to_local_homeomorph.symm (e x) = x :=
-e.to_local_equiv.left_inv hx
-
-@[simp, mfld_simps] lemma symm_coe_proj {x : B} {y : F}
-  (e : trivialization F (π E)) (h : x ∈ e.base_set) :
-  (e.to_local_homeomorph.symm (x, y)).1 = x := e.proj_symm_apply' h
-
-section has_zero
-variables [∀ x, has_zero (E x)]
-
-/-- A fiberwise inverse to `e`. The function `F → E x` that induces a local inverse
-  `B × F → total_space E` of `e` on `e.base_set`. It is defined to be `0` outside `e.base_set`. -/
-protected def symm (e : trivialization F (π E)) (b : B) (y : F) : E b :=
-e.to_pretrivialization.symm b y
-
-lemma symm_apply (e : trivialization F (π E)) {b : B} (hb : b ∈ e.base_set) (y : F) :
-  e.symm b y = cast (congr_arg E (e.symm_coe_proj hb)) (e.to_local_homeomorph.symm (b, y)).2 :=
-dif_pos hb
-
-lemma symm_apply_of_not_mem (e : trivialization F (π E)) {b : B} (hb : b ∉ e.base_set) (y : F) :
-  e.symm b y = 0 :=
-dif_neg hb
-
-lemma mk_symm (e : trivialization F (π E)) {b : B} (hb : b ∈ e.base_set) (y : F) :
-  total_space_mk b (e.symm b y) = e.to_local_homeomorph.symm (b, y) :=
-e.to_pretrivialization.mk_symm hb y
-
-lemma symm_proj_apply (e : trivialization F (π E)) (z : total_space E)
-  (hz : z.proj ∈ e.base_set) : e.symm z.proj (e z).2 = z.2 :=
-e.to_pretrivialization.symm_proj_apply z hz
-
-lemma symm_apply_apply_mk (e : trivialization F (π E)) {b : B} (hb : b ∈ e.base_set) (y : E b) :
-  e.symm b (e (total_space_mk b y)).2 = y :=
-e.symm_proj_apply (total_space_mk b y) hb
-
-lemma apply_mk_symm (e : trivialization F (π E)) {b : B} (hb : b ∈ e.base_set) (y : F) :
-  e (total_space_mk b (e.symm b y)) = (b, y) :=
-e.to_pretrivialization.apply_mk_symm hb y
-
-lemma continuous_on_symm (e : trivialization F (π E)) :
-  continuous_on (λ z : B × F, total_space_mk z.1 (e.symm z.1 z.2)) (e.base_set ×ˢ univ) :=
-begin
-  have : ∀ (z : B × F) (hz : z ∈ e.base_set ×ˢ (univ : set F)),
-    total_space_mk z.1 (e.symm z.1 z.2) = e.to_local_homeomorph.symm z,
-  { rintro x ⟨hx : x.1 ∈ e.base_set, _⟩, simp_rw [e.mk_symm hx, prod.mk.eta] },
-  refine continuous_on.congr _ this,
-  rw [← e.target_eq],
-  exact e.to_local_homeomorph.continuous_on_symm
-end
-
-end has_zero
-
 variables [add_comm_monoid F] [module R F] [∀ x, add_comm_monoid (E x)] [∀ x, module R (E x)]
 
 /-- A trivialization for a topological vector bundle defines linear equivalences between the