diff --git a/src/data/bundle.lean b/src/data/bundle.lean
new file mode 100644
index 0000000000000..7eaad1912e26d
--- /dev/null
+++ b/src/data/bundle.lean
@@ -0,0 +1,81 @@
+/-
+Copyright © 2021 Nicolò Cavalleri. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nicolò Cavalleri
+-/
+
+import tactic.basic
+import algebra.module.basic
+
+/-!
+# Bundle
+Basic data structure to implement fiber bundles, vector bundles (maybe fibrations?), etc. This file
+should contain all possible results that do not involve any topology.
+We provide a type synonym of `Σ x, E x` as `bundle.total_space E`, to be able to endow it with
+a topology which is not the disjoint union topology `sigma.topological_space`. In general, the
+constructions of fiber bundles we will make will be of this form.
+
+## References
+- https://en.wikipedia.org/wiki/Bundle_(mathematics)
+-/
+
+namespace bundle
+
+variables {B : Type*} (E : B → Type*)
+
+/--
+`total_space E` is the total space of the bundle `Σ x, E x`. This type synonym is used to avoid
+conflicts with general sigma types.
+-/
+def total_space := Σ x, E x
+
+instance [inhabited B] [inhabited (E (default B))] :
+  inhabited (total_space E) := ⟨⟨default B, default (E (default B))⟩⟩
+
+/-- `bundle.proj E` is the canonical projection `total_space E → B` on the base space. -/
+@[simp] def proj : total_space E → B := sigma.fst
+
+/-- Constructor for the total space of a `topological_fiber_bundle_core`. -/
+@[simp, reducible] def total_space_mk (E : B → Type*) (b : B) (a : E b) :
+  bundle.total_space E := ⟨b, a⟩
+
+instance {x : B} : has_coe_t (E x) (total_space E) := ⟨sigma.mk x⟩
+
+@[simp] lemma coe_fst (x : B) (v : E x) : (v : total_space E).fst = x := rfl
+
+lemma to_total_space_coe {x : B} (v : E x) : (v : total_space E) = ⟨x, v⟩ := rfl
+
+/-- `bundle.trivial B F` is the trivial bundle over `B` of fiber `F`. -/
+def trivial (B : Type*) (F : Type*) : B → Type* := function.const B F
+
+instance {F : Type*} [inhabited F] {b : B} : inhabited (bundle.trivial B F b) := ⟨(default F : F)⟩
+
+/-- The trivial bundle, unlike other bundles, has a canonical projection on the fiber. -/
+def trivial.proj_snd (B : Type*) (F : Type*) : (total_space (bundle.trivial B F)) → F := sigma.snd
+
+section fiber_structures
+
+variable [∀ x, add_comm_monoid (E x)]
+
+@[simp] lemma coe_snd_map_apply (x : B) (v w : E x) :
+  (↑(v + w) : total_space E).snd = (v : total_space E).snd + (w : total_space E).snd := rfl
+
+variables (R : Type*) [semiring R] [∀ x, module R (E x)]
+
+@[simp] lemma coe_snd_map_smul (x : B) (r : R) (v : E x) :
+  (↑(r • v) : total_space E).snd = r • (v : total_space E).snd := rfl
+
+end fiber_structures
+
+section trivial_instances
+local attribute [reducible] bundle.trivial
+
+variables {F : Type*} {R : Type*} [semiring R] (b : B)
+
+instance [add_comm_monoid F] : add_comm_monoid (bundle.trivial B F b) := ‹add_comm_monoid F›
+instance [add_comm_group F] : add_comm_group (bundle.trivial B F b) := ‹add_comm_group F›
+instance [add_comm_monoid F] [module R F] : module R (bundle.trivial B F b) := ‹module R F›
+
+end trivial_instances
+
+end bundle
diff --git a/src/geometry/manifold/basic_smooth_bundle.lean b/src/geometry/manifold/basic_smooth_bundle.lean
index 9b515116da7ee..ce922f9d2254a 100644
--- a/src/geometry/manifold/basic_smooth_bundle.lean
+++ b/src/geometry/manifold/basic_smooth_bundle.lean
@@ -106,7 +106,6 @@ structure basic_smooth_bundle_core {𝕜 : Type*} [nondiscrete_normed_field 𝕜
   times_cont_diff_on 𝕜 ∞ (λp : E × F, coord_change i j (I.symm p.1) p.2)
   ((I '' (i.1.symm.trans j.1).source).prod (univ : set F)))
 
-
 /-- The trivial basic smooth bundle core, in which all the changes of coordinates are the
 identity. -/
 def trivial_basic_smooth_bundle_core {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
@@ -169,12 +168,12 @@ def to_topological_fiber_bundle_core : topological_fiber_bundle_core (atlas H M)
   end }
 
 @[simp, mfld_simps] lemma base_set (i : atlas H M) :
-  (Z.to_topological_fiber_bundle_core.local_triv_ext i).base_set = i.1.source := rfl
+  (Z.to_topological_fiber_bundle_core.local_triv i).base_set = i.1.source := rfl
 
 /-- Local chart for the total space of a basic smooth bundle -/
 def chart {e : local_homeomorph M H} (he : e ∈ atlas H M) :
   local_homeomorph (Z.to_topological_fiber_bundle_core.total_space) (model_prod H F) :=
-(Z.to_topological_fiber_bundle_core.local_triv ⟨e, he⟩).trans
+(Z.to_topological_fiber_bundle_core.local_triv ⟨e, he⟩).to_local_homeomorph.trans
   (local_homeomorph.prod e (local_homeomorph.refl F))
 
 @[simp, mfld_simps] lemma chart_source (e : local_homeomorph M H) (he : e ∈ atlas H M) :
@@ -481,7 +480,7 @@ tangent bundle gives a second component in the tangent space. -/
 def tangent_bundle := Σ (x : M), tangent_space I x
 
 /-- The projection from the tangent bundle of a smooth manifold to the manifold. As the tangent
-bundle is represented internally as a product type, the notation `p.1` also works for the projection
+bundle is represented internally as a sigma type, the notation `p.1` also works for the projection
 of the point `p`. -/
 def tangent_bundle.proj : tangent_bundle I M → M :=
 λ p, p.1
diff --git a/src/topology/continuous_on.lean b/src/topology/continuous_on.lean
index 6803fb0a04f77..de17a427ced36 100644
--- a/src/topology/continuous_on.lean
+++ b/src/topology/continuous_on.lean
@@ -658,6 +658,11 @@ lemma continuous_within_at.comp' {g : β → γ} {f : α → β} {s : set α} {t
   continuous_within_at (g ∘ f) (s ∩ f⁻¹' t) x :=
 hg.comp (hf.mono (inter_subset_left _ _)) (inter_subset_right _ _)
 
+lemma continuous_at.comp_continuous_within_at {g : β → γ} {f : α → β} {s : set α} {x : α}
+  (hg : continuous_at g (f x)) (hf : continuous_within_at f s x) :
+  continuous_within_at (g ∘ f) s x :=
+hg.continuous_within_at.comp hf subset_preimage_univ
+
 lemma continuous_on.comp {g : β → γ} {f : α → β} {s : set α} {t : set β}
   (hg : continuous_on g t) (hf : continuous_on f s) (h : s ⊆ f ⁻¹' t) :
   continuous_on (g ∘ f) s :=
@@ -1004,3 +1009,16 @@ continuous_snd.continuous_on
 lemma continuous_within_at_snd {s : set (α × β)} {p : α × β} :
   continuous_within_at prod.snd s p :=
 continuous_snd.continuous_within_at
+
+lemma continuous_within_at.fst {f : α → β × γ} {s : set α} {a : α}
+  (h : continuous_within_at f s a) : continuous_within_at (λ x, (f x).fst) s a :=
+continuous_at_fst.comp_continuous_within_at h
+
+lemma continuous_within_at.snd {f : α → β × γ} {s : set α} {a : α}
+  (h : continuous_within_at f s a) : continuous_within_at (λ x, (f x).snd) s a :=
+continuous_at_snd.comp_continuous_within_at h
+
+lemma continuous_within_at_prod_iff {f : α → β × γ} {s : set α} {x : α} :
+  continuous_within_at f s x ↔ continuous_within_at (prod.fst ∘ f) s x ∧
+  continuous_within_at (prod.snd ∘ f) s x :=
+⟨λ h, ⟨h.fst, h.snd⟩, by { rintro ⟨h1, h2⟩, convert h1.prod h2, ext, refl, refl }⟩
diff --git a/src/topology/topological_fiber_bundle.lean b/src/topology/topological_fiber_bundle.lean
index 1fc8fe4a27871..2ff6f1944a57b 100644
--- a/src/topology/topological_fiber_bundle.lean
+++ b/src/topology/topological_fiber_bundle.lean
@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 import topology.local_homeomorph
 import topology.algebra.ordered.basic
+import data.bundle
 
 /-!
 # Fiber bundles
@@ -73,10 +74,11 @@ Let `Z : topological_fiber_bundle_core ι B F`. Then we define
   twisted topology coming from the fiber bundle structure. It is (reducibly) the same as
   `bundle.total_space Z.fiber`.
 * `Z.proj`        : projection from `Z.total_space` to `B`. It is continuous.
-* `Z.local_triv i`: for `i : ι`, a local homeomorphism from `Z.total_space` to `B × F`, that
-  realizes a trivialization above the set `Z.base_set i`, which is an open set in `B`.
+* `Z.local_triv i`: for `i : ι`, bundle trivialization above the set `Z.base_set i`, which is an
+                    open set in `B`.
 
-* `prebundle_trivialization F proj` : trivialization as a local equivalence.
+* `prebundle_trivialization 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
@@ -143,7 +145,7 @@ Or for the pullback of a `topological_fiber_bundle_core`, the indexing type will
 for the initial bundle.
 
 ## Tags
-Fiber bundle, topological bundle, vector bundle, local trivialization, structure group
+Fiber bundle, topological bundle, local trivialization, structure group
 -/
 
 variables {ι : Type*} {B : Type*} {F : Type*}
@@ -273,6 +275,10 @@ lemma mk_proj_snd (ex : x ∈ e.source) : (proj x, (e x).2) = e x := prod.ext (e
 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) :
   (bundle_trivialization.mk e i j k l m : bundle_trivialization F proj) x = e x := rfl
 
@@ -717,44 +723,10 @@ end topological_fiber_bundle
 /-! ### Constructing topological fiber bundles -/
 
 namespace bundle
-/- We provide a type synonym of `Σ x, E x` as `bundle.total_space E`, to be able to endow it with
-a topology which is not the disjoint union topology. In general, the constructions of fiber bundles
-we will make will be of this form. -/
 
 variable (E : B → Type*)
 
-/--
-`total_space E` is the total space of the bundle `Σ x, E x`. This type synonym is used to avoid
-conflicts with general sigma types.
--/
-def total_space := Σ x, E x
-
-instance [inhabited B] [inhabited (E (default B))] :
-  inhabited (total_space E) := ⟨⟨default B, default (E (default B))⟩⟩
-
-/-- `bundle.proj E` is the canonical projection `total_space E → B` on the base space. -/
-@[simp, mfld_simps] def proj : total_space E → B :=
-λ (y : total_space E), y.1
-
-/-- Constructor for the total space of a `topological_fiber_bundle_core`. -/
-@[simp, mfld_simps, reducible] def total_space_mk (E : B → Type*) (b : B) (a : E b) :
-  bundle.total_space E := ⟨b, a⟩
-
-instance {x : B} : has_coe_t (E x) (total_space E) := ⟨λ y, (⟨x, y⟩ : total_space E)⟩
-
-@[simp, mfld_simps] lemma coe_fst (x : B) (v : E x) : (v : total_space E).fst = x := rfl
-
-lemma to_total_space_coe {x : B} (v : E x) : (v : total_space E) = ⟨x, v⟩ := rfl
-
-/-- `bundle.trivial B F` is the trivial bundle over `B` of fiber `F`. -/
-@[nolint unused_arguments]
-def trivial (B : Type*) (F : Type*) : B → Type* := λ x, F
-
-instance [inhabited F] {b : B} : inhabited (bundle.trivial B F b) :=
-⟨(default F : F)⟩
-
-/-- The trivial bundle, unlike other bundles, has a canonical projection on the fiber. -/
-def trivial.proj_snd (B : Type*) (F : Type*) : (total_space (bundle.trivial B F)) → F := sigma.snd
+attribute [mfld_simps] proj total_space_mk coe_fst coe_snd_map_apply coe_snd_map_smul
 
 instance [I : topological_space F] : ∀ x : B, topological_space (trivial B F x) := λ x, I
 
@@ -763,22 +735,12 @@ instance [t₁ : topological_space B] [t₂ : topological_space F] :
 topological_space.induced (proj (trivial B F)) t₁ ⊓
   topological_space.induced (trivial.proj_snd B F) t₂
 
-variable [∀ x, add_comm_monoid (E x)]
-
-@[simp, mfld_simps] lemma coe_snd_map_apply (x : B) (v w : E x) :
-  (↑(v + w) : total_space E).snd = (v : total_space E).snd + (w : total_space E).snd := rfl
-
-variables (R : Type*) [semiring R] [∀ x, module R (E x)]
-
-@[simp, mfld_simps] lemma coe_snd_map_smul (x : B) (r : R) (v : E x) :
-  (↑(r • v) : total_space E).snd = r • (v : total_space E).snd := rfl
-
 end bundle
 
 /-- Core data defining a locally trivial topological bundle with fiber `F` over a topological
 space `B`. Note that "bundle" is used in its mathematical sense. This is the (computer science)
 bundled version, i.e., all the relevant data is contained in the following structure. A family of
-local trivializations is indexed by a type ι, on open subsets `base_set i` for each `i : ι`.
+local trivializations is indexed by a type `ι`, on open subsets `base_set i` for each `i : ι`.
 Trivialization changes from `i` to `j` are given by continuous maps `coord_change i j` from
 `base_set i ∩ base_set j` to the set of homeomorphisms of `F`, but we express them as maps
 `B → F → F` and require continuity on `(base_set i ∩ base_set j) × F` to avoid the topology on the
@@ -787,14 +749,14 @@ space of continuous maps on `F`. -/
 structure topological_fiber_bundle_core (ι : Type*) (B : Type*) [topological_space B]
   (F : Type*) [topological_space F] :=
 (base_set          : ι → set B)
-(is_open_base_set  : ∀i, is_open (base_set i))
+(is_open_base_set  : ∀ i, is_open (base_set i))
 (index_at          : B → ι)
-(mem_base_set_at   : ∀x, x ∈ base_set (index_at x))
+(mem_base_set_at   : ∀ x, x ∈ base_set (index_at x))
 (coord_change      : ι → ι → B → F → F)
-(coord_change_self : ∀i, ∀ x ∈ base_set i, ∀v, coord_change i i x v = v)
-(coord_change_continuous : ∀i j, continuous_on (λp : B × F, coord_change i j p.1 p.2)
+(coord_change_self : ∀ i, ∀ x ∈ base_set i, ∀ v, coord_change i i x v = v)
+(coord_change_continuous : ∀ i j, continuous_on (λp : B × F, coord_change i j p.1 p.2)
                                                (set.prod ((base_set i) ∩ (base_set j)) univ))
-(coord_change_comp : ∀i j k, ∀x ∈ (base_set i) ∩ (base_set j) ∩ (base_set k), ∀v,
+(coord_change_comp : ∀ i j k, ∀ x ∈ (base_set i) ∩ (base_set j) ∩ (base_set k), ∀ v,
   (coord_change j k x) (coord_change i j x v) = coord_change i k x v)
 
 namespace topological_fiber_bundle_core
@@ -816,8 +778,12 @@ typeclass inference -/
 @[nolint unused_arguments has_inhabited_instance]
 def fiber (x : B) := F
 
-instance topological_space_fiber (x : B) : topological_space (Z.fiber x) :=
-by { dsimp [fiber], apply_instance }
+section fiber_instances
+local attribute [reducible] fiber
+
+instance topological_space_fiber (x : B) : topological_space (Z.fiber x) := by apply_instance
+
+end fiber_instances
 
 /-- The total space of the topological fiber bundle, as a convenience function for dot notation.
 It is by definition equal to `bundle.total_space Z.fiber`, a.k.a. `Σ x, Z.fiber x` but with a
@@ -871,7 +837,7 @@ The local trivialization will ultimately be a local homeomorphism. For now, we o
 local equiv version, denoted with a prime. In further developments, avoid this auxiliary version,
 and use `Z.local_triv` instead.
 -/
-def local_triv' (i : ι) : local_equiv Z.total_space (B × F) :=
+def local_triv_as_local_equiv (i : ι) : local_equiv Z.total_space (B × F) :=
 { source      := Z.proj ⁻¹' (Z.base_set i),
   target      := set.prod (Z.base_set i) univ,
   inv_fun     := λp, ⟨p.1, Z.coord_change i (Z.index_at p.1) p.1 p.2⟩,
@@ -883,7 +849,7 @@ def local_triv' (i : ι) : local_equiv Z.total_space (B × F) :=
   left_inv'   := begin
     rintros ⟨x, v⟩ hx,
     change x ∈ Z.base_set i at hx,
-    dsimp,
+    dsimp only,
     rw [Z.coord_change_comp, Z.coord_change_self],
     { exact Z.mem_base_set_at _ },
     { simp only [hx, mem_inter_eq, and_self, mem_base_set_at] }
@@ -893,37 +859,33 @@ def local_triv' (i : ι) : local_equiv Z.total_space (B × F) :=
     simp only [prod_mk_mem_set_prod_eq, and_true, mem_univ] at hx,
     rw [Z.coord_change_comp, Z.coord_change_self],
     { exact hx },
-    { simp only [hx, mem_inter_eq, and_self, mem_base_set_at]}
+    { simp only [hx, mem_inter_eq, and_self, mem_base_set_at] }
   end }
 
 variable (i : ι)
 
-lemma mem_local_triv'_source (p : Z.total_space) :
-  p ∈ (Z.local_triv' i).source ↔ p.1 ∈ Z.base_set i :=
+lemma mem_local_triv_as_local_equiv_source (p : Z.total_space) :
+  p ∈ (Z.local_triv_as_local_equiv i).source ↔ p.1 ∈ Z.base_set i :=
 iff.rfl
 
-lemma mem_local_triv'_target (p : B × F) : p ∈ (Z.local_triv' i).target ↔ p.1 ∈ Z.base_set i :=
-by { erw [mem_prod], simp }
-
-lemma local_triv'_apply (p : Z.total_space) :
-  (Z.local_triv' i) p = ⟨p.1, Z.coord_change (Z.index_at p.1) i p.1 p.2⟩ := rfl
+lemma mem_local_triv_as_local_equiv_target (p : B × F) :
+  p ∈ (Z.local_triv_as_local_equiv i).target ↔ p.1 ∈ Z.base_set i :=
+by { erw [mem_prod], simp only [and_true, mem_univ] }
 
-lemma local_triv'_symm_apply (p : B × F) :
-  (Z.local_triv' i).symm p = ⟨p.1, Z.coord_change i (Z.index_at p.1) p.1 p.2⟩ := rfl
+lemma local_triv_as_local_equiv_apply (p : Z.total_space) :
+  (Z.local_triv_as_local_equiv i) p = ⟨p.1, Z.coord_change (Z.index_at p.1) i p.1 p.2⟩ := rfl
 
 /-- The composition of two local trivializations is the trivialization change Z.triv_change i j. -/
-lemma local_triv'_trans (i j : ι) :
-  (Z.local_triv' i).symm.trans (Z.local_triv' j) ≈ (Z.triv_change i j).to_local_equiv :=
+lemma local_triv_as_local_equiv_trans (i j : ι) :
+  (Z.local_triv_as_local_equiv i).symm.trans
+    (Z.local_triv_as_local_equiv j) ≈ (Z.triv_change i j).to_local_equiv :=
 begin
   split,
-  { ext x,
-    erw [mem_prod],
-    simp only [mem_local_triv'_source, mem_local_triv'_target, local_triv'_symm_apply]
-      with mfld_simps, },
+  { ext x, simp only [mem_local_triv_as_local_equiv_target] with mfld_simps, refl, },
   { rintros ⟨x, v⟩ hx,
-    simp only [triv_change, local_triv', local_equiv.symm, true_and, prod_mk_mem_set_prod_eq,
-      local_equiv.trans_source, mem_inter_eq, and_true, mem_univ, prod.mk.inj_iff, mem_preimage,
-      proj, local_equiv.coe_mk, eq_self_iff_true, local_equiv.coe_trans, bundle.proj] at hx ⊢,
+    simp only [triv_change, local_triv_as_local_equiv, local_equiv.symm, true_and, prod.mk.inj_iff,
+      prod_mk_mem_set_prod_eq, local_equiv.trans_source, mem_inter_eq, and_true, mem_preimage, proj,
+      mem_univ, local_equiv.coe_mk, eq_self_iff_true, local_equiv.coe_trans, bundle.proj] at hx ⊢,
     simp only [Z.coord_change_comp, hx, mem_inter_eq, and_self, mem_base_set_at], }
 end
 
@@ -933,27 +895,30 @@ variable (ι)
 that all the local trivialization are continuous. -/
 instance to_topological_space : topological_space (bundle.total_space Z.fiber) :=
 topological_space.generate_from $ ⋃ (i : ι) (s : set (B × F)) (s_open : is_open s),
-  {(Z.local_triv' i).source ∩ (Z.local_triv' i) ⁻¹' s}
+  {(Z.local_triv_as_local_equiv i).source ∩ (Z.local_triv_as_local_equiv i) ⁻¹' s}
 
 variable {ι}
 
-lemma open_source' (i : ι) : is_open (Z.local_triv' i).source :=
+lemma open_source' (i : ι) : is_open (Z.local_triv_as_local_equiv i).source :=
 begin
   apply topological_space.generate_open.basic,
   simp only [exists_prop, mem_Union, mem_singleton_iff],
   refine ⟨i, set.prod (Z.base_set i) univ, (Z.is_open_base_set i).prod is_open_univ, _⟩,
   ext p,
-  simp only [local_triv'_apply, prod_mk_mem_set_prod_eq, mem_local_triv'_source, mem_inter_eq,
-    and_true, mem_univ, mem_preimage, and_self]
+  simp only [local_triv_as_local_equiv_apply, prod_mk_mem_set_prod_eq, mem_inter_eq, and_self,
+    mem_local_triv_as_local_equiv_source, and_true, mem_univ, mem_preimage],
 end
 
-lemma open_target' (i : ι) : is_open (Z.local_triv' i).target :=
-(Z.is_open_base_set i).prod is_open_univ
-
-/-- Local trivialization of a topological bundle created from core, as a local homeomorphism. -/
-def local_triv (i : ι) : local_homeomorph Z.total_space (B × F) :=
-{ open_source := Z.open_source' i,
-  open_target := Z.open_target' i,
+/-- Extended version of the local trivialization of a fiber bundle constructed from core,
+registering additionally in its type that it is a local bundle trivialization. -/
+def local_triv (i : ι) : bundle_trivialization F Z.proj :=
+{ base_set      := Z.base_set i,
+  open_base_set := Z.is_open_base_set i,
+  source_eq     := rfl,
+  target_eq     := rfl,
+  proj_to_fun   := λ p hp, by { simp only with mfld_simps, refl },
+  open_source := Z.open_source' i,
+  open_target := (Z.is_open_base_set i).prod is_open_univ,
   continuous_to_fun := begin
     rw continuous_on_open_iff (Z.open_source' i),
     assume s s_open,
@@ -962,69 +927,30 @@ def local_triv (i : ι) : local_homeomorph Z.total_space (B × F) :=
     exact ⟨i, s, s_open, rfl⟩
   end,
   continuous_inv_fun := begin
-    apply continuous_on_open_of_generate_from (Z.open_target' i),
+    apply continuous_on_open_of_generate_from ((Z.is_open_base_set i).prod is_open_univ),
     assume t ht,
     simp only [exists_prop, mem_Union, mem_singleton_iff] at ht,
-    obtain ⟨j, s, s_open, ts⟩ : ∃ j s,
-      is_open s ∧ t = (local_triv' Z j).source ∩ (local_triv' Z j) ⁻¹' s := ht,
+    obtain ⟨j, s, s_open, ts⟩ : ∃ j s, is_open s ∧ t =
+      (local_triv_as_local_equiv Z j).source ∩ (local_triv_as_local_equiv Z j) ⁻¹' s := ht,
     rw ts,
     simp only [local_equiv.right_inv, preimage_inter, local_equiv.left_inv],
-    let e := Z.local_triv' i,
-    let e' := Z.local_triv' j,
+    let e := Z.local_triv_as_local_equiv i,
+    let e' := Z.local_triv_as_local_equiv j,
     let f := e.symm.trans e',
     have : is_open (f.source ∩ f ⁻¹' s),
-    { rw [(Z.local_triv'_trans i j).source_inter_preimage_eq],
+    { rw [(Z.local_triv_as_local_equiv_trans i j).source_inter_preimage_eq],
       exact (continuous_on_open_iff (Z.triv_change i j).open_source).1
         ((Z.triv_change i j).continuous_on) _ s_open },
     convert this using 1,
     dsimp [local_equiv.trans_source],
-    rw [← preimage_comp, inter_assoc]
+    rw [← preimage_comp, inter_assoc],
+    refl,
   end,
-  to_local_equiv := Z.local_triv' i }
-
-@[simp, mfld_simps] lemma local_triv'_coe : ⇑(Z.local_triv' i) = Z.local_triv i := rfl
-
-@[simp, mfld_simps] lemma local_triv'_source :
-  (Z.local_triv' i).source = (Z.local_triv i).source := rfl
-
-@[simp, mfld_simps] lemma local_triv'_target :
-  (Z.local_triv' i).target = (Z.local_triv i).target := rfl
-
-/- We will now state again the basic properties of the local trivializations, but without primes,
-i.e., for the local homeomorphism instead of the local equiv. -/
-
-lemma mem_local_triv_source (p : Z.total_space) :
-  p ∈ (Z.local_triv i).source ↔ p.1 ∈ Z.base_set i :=
-iff.rfl
-
-lemma mem_local_triv_target (p : B × F) : p ∈ (Z.local_triv i).target ↔ p.1 ∈ Z.base_set i :=
-by { erw [mem_prod], simp }
-
-lemma local_triv_apply (p : Z.total_space) :
-  (Z.local_triv i) p = ⟨p.1, Z.coord_change (Z.index_at p.1) i p.1 p.2⟩ := rfl
-
-lemma local_triv_symm_fst (p : B × F) :
-  (Z.local_triv i).symm p = ⟨p.1, Z.coord_change i (Z.index_at p.1) p.1 p.2⟩ := rfl
-
-/-- The composition of two local trivializations is the trivialization change Z.triv_change i j. -/
-lemma local_triv_trans (i j : ι) :
-  (Z.local_triv i).symm.trans (Z.local_triv j) ≈ Z.triv_change i j :=
-Z.local_triv'_trans i j
-
-/-- Extended version of the local trivialization of a fiber bundle constructed from core,
-registering additionally in its type that it is a local bundle trivialization. -/
-def local_triv_ext (i : ι) : bundle_trivialization F Z.proj :=
-{ base_set      := Z.base_set i,
-  open_base_set := Z.is_open_base_set i,
-  source_eq     := rfl,
-  target_eq     := rfl,
-  proj_to_fun   := λp hp, by simp only [local_triv_symm_fst, local_triv_apply,
-                              mem_local_triv_target, mem_local_triv_source] with mfld_simps,
-  to_local_homeomorph := Z.local_triv i }
+  to_local_equiv := Z.local_triv_as_local_equiv i }
 
 /-- A topological fiber bundle constructed from core is indeed a topological fiber bundle. -/
 protected theorem is_topological_fiber_bundle : is_topological_fiber_bundle F Z.proj :=
-λx, ⟨Z.local_triv_ext (Z.index_at x), Z.mem_base_set_at x⟩
+λx, ⟨Z.local_triv (Z.index_at x), Z.mem_base_set_at x⟩
 
 /-- The projection on the base of a topological bundle created from core is continuous -/
 lemma continuous_proj : continuous Z.proj :=
@@ -1036,11 +962,11 @@ Z.is_topological_fiber_bundle.is_open_map_proj
 
 /-- Preferred local trivialization of a fiber bundle constructed from core, at a given point, as
 a bundle trivialization -/
-def local_triv_at_ext (b : B) : bundle_trivialization F Z.proj :=
-Z.local_triv_ext (Z.index_at b)
+def local_triv_at (b : B) : bundle_trivialization F Z.proj :=
+Z.local_triv (Z.index_at b)
 
-@[simp, mfld_simps] lemma local_triv_at_ext_def (b : B) :
-  Z.local_triv_ext (Z.index_at b) = Z.local_triv_at_ext b := rfl
+@[simp, mfld_simps] lemma local_triv_at_def (b : B) :
+  Z.local_triv (Z.index_at b) = Z.local_triv_at b := rfl
 
 /-- If an element of `F` is invariant under all coordinate changes, then one can define a
 corresponding section of the fiber bundle, which is continuous. This applies in particular to the
@@ -1053,7 +979,7 @@ begin
   apply continuous_iff_continuous_at.2 (λ x, _),
   have A : Z.base_set (Z.index_at x) ∈ 𝓝 x :=
     is_open.mem_nhds (Z.is_open_base_set (Z.index_at x)) (Z.mem_base_set_at x),
-  apply ((Z.local_triv (Z.index_at x)).continuous_at_iff_continuous_at_comp_left _).2,
+  apply ((Z.local_triv_at x).to_local_homeomorph.continuous_at_iff_continuous_at_comp_left _).2,
   { simp only [(∘)] with mfld_simps,
     apply continuous_at_id.prod,
     have : continuous_on (λ (y : B), v) (Z.base_set (Z.index_at x)) := continuous_on_const,
@@ -1063,43 +989,41 @@ begin
   { exact A }
 end
 
-@[simp, mfld_simps] lemma local_triv_coe : ⇑(Z.local_triv i) = Z.local_triv_ext i := rfl
-
-@[simp, mfld_simps] lemma local_triv_source :
-  (Z.local_triv i).source = (Z.local_triv_ext i).source := rfl
+@[simp, mfld_simps] lemma local_triv_as_local_equiv_coe :
+  ⇑(Z.local_triv_as_local_equiv i) = Z.local_triv i := rfl
 
-@[simp, mfld_simps] lemma local_triv_target :
-  (Z.local_triv i).target = (Z.local_triv_ext i).target := rfl
+@[simp, mfld_simps] lemma local_triv_as_local_equiv_source :
+  (Z.local_triv_as_local_equiv i).source = (Z.local_triv i).source := rfl
 
-@[simp, mfld_simps] lemma local_triv_symm :
-  (Z.local_triv i).symm = (Z.local_triv_ext i).to_local_homeomorph.symm := rfl
+@[simp, mfld_simps] lemma local_triv_as_local_equiv_target :
+  (Z.local_triv_as_local_equiv i).target = (Z.local_triv i).target := rfl
 
-@[simp, mfld_simps] lemma base_set_at : Z.base_set i = (Z.local_triv_ext i).base_set := rfl
+@[simp, mfld_simps] lemma local_triv_as_local_equiv_symm :
+  (Z.local_triv_as_local_equiv i).symm = (Z.local_triv i).to_local_equiv.symm := rfl
 
-@[simp, mfld_simps] lemma local_triv_ext_apply (p : Z.total_space) :
-  (Z.local_triv_ext i) p = ⟨p.1, Z.coord_change (Z.index_at p.1) i p.1 p.2⟩ := rfl
+@[simp, mfld_simps] lemma base_set_at : Z.base_set i = (Z.local_triv i).base_set := rfl
 
-@[simp, mfld_simps] lemma local_triv_ext_symm_apply (p : B × F) :
-  (Z.local_triv' i).symm p = ⟨p.1, Z.coord_change i (Z.index_at p.1) p.1 p.2⟩ := rfl
+@[simp, mfld_simps] lemma local_triv_apply (p : Z.total_space) :
+  (Z.local_triv i) p = ⟨p.1, Z.coord_change (Z.index_at p.1) i p.1 p.2⟩ := rfl
 
-@[simp, mfld_simps] lemma mem_local_triv_ext_source (p : Z.total_space) :
-  p ∈ (Z.local_triv_ext i).source ↔ p.1 ∈ (Z.local_triv_ext i).base_set := iff.rfl
+@[simp, mfld_simps] lemma mem_local_triv_source (p : Z.total_space) :
+  p ∈ (Z.local_triv i).source ↔ p.1 ∈ (Z.local_triv i).base_set := iff.rfl
 
-@[simp, mfld_simps] lemma mem_local_triv_ext_target (p : B × F) :
-  p ∈ (Z.local_triv_ext i).target ↔ p.1 ∈ (Z.local_triv_ext i).base_set :=
+@[simp, mfld_simps] lemma mem_local_triv_target (p : B × F) :
+  p ∈ (Z.local_triv i).target ↔ p.1 ∈ (Z.local_triv i).base_set :=
 bundle_trivialization.mem_target _
 
-@[simp, mfld_simps] lemma local_triv_ext_symm_fst (p : B × F) :
-  (Z.local_triv_ext i).to_local_homeomorph.symm p =
+@[simp, mfld_simps] lemma local_triv_symm_fst (p : B × F) :
+  (Z.local_triv i).to_local_homeomorph.symm p =
     ⟨p.1, Z.coord_change i (Z.index_at p.1) p.1 p.2⟩ := rfl
 
 @[simp, mfld_simps] lemma local_triv_at_apply (b : B) (a : F) :
-  ((Z.local_triv_at_ext b) ⟨b, a⟩) = ⟨b, a⟩ :=
-by { rw [local_triv_at_ext, local_triv_ext_apply, coord_change_self], exact Z.mem_base_set_at b }
+  ((Z.local_triv_at b) ⟨b, a⟩) = ⟨b, a⟩ :=
+by { rw [local_triv_at, local_triv_apply, coord_change_self], exact Z.mem_base_set_at b }
 
-@[simp, mfld_simps] lemma mem_local_triv_at_ext_base_set (b : B) :
-  b ∈ (Z.local_triv_at_ext b).base_set :=
-by { rw [local_triv_at_ext, ←base_set_at], exact Z.mem_base_set_at b, }
+@[simp, mfld_simps] lemma mem_local_triv_at_base_set (b : B) :
+  b ∈ (Z.local_triv_at b).base_set :=
+by { rw [local_triv_at, ←base_set_at], exact Z.mem_base_set_at b, }
 
 open bundle
 
@@ -1108,17 +1032,18 @@ lemma continuous_total_space_mk (b : B) : continuous (λ a, total_space_mk Z.fib
 begin
   rw [continuous_iff_le_induced, topological_fiber_bundle_core.to_topological_space],
   apply le_induced_generate_from,
-  simp only [total_space_mk, mem_Union, mem_singleton_iff, local_triv'_source, local_triv'_coe],
+  simp only [total_space_mk, mem_Union, mem_singleton_iff, local_triv_as_local_equiv_source,
+    local_triv_as_local_equiv_coe],
   rintros s ⟨i, t, ht, rfl⟩,
-  rw [←(local_homeomorph.source_inter_preimage_target_inter (Z.local_triv i) t),
-    preimage_inter, ←preimage_comp, local_triv_source, bundle_trivialization.source_eq],
+  rw [←((Z.local_triv i).source_inter_preimage_target_inter t), preimage_inter, ←preimage_comp,
+    bundle_trivialization.source_eq],
   apply is_open.inter,
   { simp only [bundle.proj, proj, ←preimage_comp],
-    by_cases (b ∈ (Z.local_triv_ext i).base_set),
+    by_cases (b ∈ (Z.local_triv i).base_set),
     { rw preimage_const_of_mem h, exact is_open_univ, },
     { rw preimage_const_of_not_mem h, exact is_open_empty, }},
   { simp only [function.comp, local_triv_apply],
-    rw [preimage_comp, local_triv_target],
+    rw [preimage_inter, preimage_comp],
     by_cases (b ∈ Z.base_set i),
     { have hc : continuous (λ (x : Z.fiber b), (Z.coord_change (Z.index_at b) i b) x) := begin
         rw continuous_iff_continuous_on_univ,
@@ -1127,8 +1052,8 @@ begin
             exact mk_preimage_prod_right (mem_inter (Z.mem_base_set_at b) h), }) end,
       exact hc.is_open_preimage _ ((continuous.prod.mk b).is_open_preimage _
         ((Z.local_triv i).open_target.inter ht)), },
-    { rw [(Z.local_triv_ext i).target_eq, preimage_inter, ←base_set_at,
-        mk_preimage_prod_right_eq_empty h, empty_inter, preimage_empty],
+    { rw [(Z.local_triv i).target_eq, ←base_set_at, mk_preimage_prod_right_eq_empty h,
+        preimage_empty, empty_inter],
       exact is_open_empty, }}
 end
 
diff --git a/src/topology/vector_bundle.lean b/src/topology/vector_bundle.lean
index b272000b59727..eb36c077068c5 100644
--- a/src/topology/vector_bundle.lean
+++ b/src/topology/vector_bundle.lean
@@ -49,6 +49,9 @@ with a topology and a topological vector bundle structure.
 Similar constructions can be done for tensor products of topological vector bundles, exterior
 algebras, and so on, where the topology can be defined using a norm on the fiber model if this
 helps.
+
+## Tags
+Vector bundle
 -/
 
 noncomputable theory
@@ -338,13 +341,10 @@ variables {ι} (b : B) (a : F)
 /-- Extended version of the local trivialization of a fiber bundle constructed from core,
 registering additionally in its type that it is a local bundle trivialization. -/
 def local_triv (i : ι) : topological_vector_bundle.trivialization R F Z.fiber :=
-{ linear := λ x hx, { map_add := λ v w, by simp only [topological_fiber_bundle_core.local_triv_ext,
-      local_homeomorph.to_fun_eq_coe, coe_fst, coe_snd_map_apply,
-      topological_fiber_bundle_core.local_triv_apply, linear_map.map_add, coe_cord_change],
-  map_smul := λ r v, by simp only [topological_fiber_bundle_core.local_triv_ext, coe_fst,
-    local_homeomorph.to_fun_eq_coe, topological_fiber_bundle_core.local_triv_apply, coe_cord_change,
-    coe_snd_map_smul, linear_map.map_smul] },
-  ..topological_fiber_bundle_core.local_triv_ext ↑Z i }
+{ linear := λ x hx,
+  { map_add := λ v w, by simp only [linear_map.map_add] with mfld_simps,
+    map_smul := λ r v, by simp only [linear_map.map_smul] with mfld_simps},
+  ..topological_fiber_bundle_core.local_triv ↑Z i }
 
 @[simp, mfld_simps] lemma mem_local_triv_source (i : ι) (p : total_space Z.fiber) :
   p ∈ (Z.local_triv i).source ↔ p.1 ∈ Z.base_set i :=