refactor(topology/vector_bundle/hom): fibres of hom-bundle carry strong topology (#19107)

Currently, the "hom-bundle" between two vector bundles `E₁` and `E₂` has fibre over `x` which is a type synonym of `E₁ x →SL[σ] E₂ x`, but which carries a topology produced by the hom-bundle construction (using the identification by trivializations withe the model fibre `F₁ →SL[σ] F₂`).  This was needed when this bundle was made (#14541) because at that time, `F₁ →SL[σ] F₂` (continuous linear maps between normed spaces) carried a topology in mathlib but `E₁ x →SL[σ] E₂ x` (continuous linear maps between topological vector spaces) did not.

As of #16053, continuous linear maps between topological vector spaces do carry a topology, the strong topology.  So we can kill the old topology on the type synonym and just use the default one, which should avoid annoying issues later.

A few minor changes are needed to make this go through:
- we revert #14377: the question is whether the "vector prebundle" construction, whose canonical use is for the hom-bundle, should or should not require a topology on the fibres.  Now that in applications it could happen either way (fibres do or don't come with a topology), it will be more convenient to assume that they do carry a topology, and put the "artificial" topology on the fibres if they happen to not.
- some assumptions need to change from `[add_comm_monoid]` to `[add_comm_group]`, this is mathematically harmless since they are also modules over a field.
- generalize the construction `continuous_linear_equiv.arrow_congrSL` from normed spaces to topological vector spaces

Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

Author: hrmacbeth

src/analysis/convolution.lean

@@ -1497,7 +1497,9 @@ begin
     simp only [ef, eg, comp_app, continuous_linear_equiv.apply_symm_apply, coe_comp',
       continuous_linear_equiv.prod_apply, continuous_linear_equiv.map_sub,
       continuous_linear_equiv.arrow_congr, continuous_linear_equiv.arrow_congrSL_symm_apply,
-      continuous_linear_equiv.coe_coe, comp_app, continuous_linear_equiv.apply_symm_apply] },
+      continuous_linear_equiv.coe_coe, comp_app, continuous_linear_equiv.apply_symm_apply,
+      linear_equiv.inv_fun_eq_symm, continuous_linear_equiv.arrow_congrₛₗ_symm_apply,
+      eq_self_iff_true] },
   simp_rw [this] at A,
   exact A,
 end

src/analysis/normed_space/operator_norm.lean

@@ -1715,46 +1715,6 @@ begin
         (λ y, homothety_inverse _ hx _ (to_span_nonzero_singleton_homothety 𝕜 x h) _)
 end
 
-variables {𝕜} {𝕜₄ : Type*} [nontrivially_normed_field 𝕜₄]
-variables {H : Type*} [normed_add_comm_group H] [normed_space 𝕜₄ H] [normed_space 𝕜₃ G]
-variables {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
-variables {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃}
-variables {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄}
-variables [ring_hom_inv_pair σ₃₄ σ₄₃] [ring_hom_inv_pair σ₄₃ σ₃₄]
-variables [ring_hom_comp_triple σ₂₁ σ₁₄ σ₂₄] [ring_hom_comp_triple σ₂₄ σ₄₃ σ₂₃]
-variables [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄]
-variables [ring_hom_isometric σ₁₄] [ring_hom_isometric σ₂₃]
-variables [ring_hom_isometric σ₄₃] [ring_hom_isometric σ₂₄]
-variables [ring_hom_isometric σ₁₃] [ring_hom_isometric σ₁₂]
-variables [ring_hom_isometric σ₃₄]
-
-include σ₂₁ σ₃₄ σ₁₃ σ₂₄
-
-/-- A pair of continuous (semi)linear equivalences generates an continuous (semi)linear equivalence
-between the spaces of continuous (semi)linear maps. -/
-@[simps apply symm_apply]
-def arrow_congrSL (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) :
-  (E →SL[σ₁₄] H) ≃SL[σ₄₃] (F →SL[σ₂₃] G) :=
-{ -- given explicitly to help `simps`
-  to_fun := λ L, (e₄₃ : H →SL[σ₄₃] G).comp (L.comp (e₁₂.symm : F →SL[σ₂₁] E)),
-  -- given explicitly to help `simps`
-  inv_fun := λ L, (e₄₃.symm : G →SL[σ₃₄] H).comp (L.comp (e₁₂ : E →SL[σ₁₂] F)),
-  map_add' := λ f g, by rw [add_comp, comp_add],
-  map_smul' := λ t f, by rw [smul_comp, comp_smulₛₗ],
-  continuous_to_fun := (continuous_id.clm_comp_const _).const_clm_comp _,
-  continuous_inv_fun := (continuous_id.clm_comp_const _).const_clm_comp _,
-  .. e₁₂.arrow_congr_equiv e₄₃, }
-
-omit σ₂₁ σ₃₄ σ₁₃ σ₂₄
-
-/-- A pair of continuous linear equivalences generates an continuous linear equivalence between
-the spaces of continuous linear maps. -/
-def arrow_congr {F H : Type*} [normed_add_comm_group F] [normed_add_comm_group H]
-  [normed_space 𝕜 F] [normed_space 𝕜 G] [normed_space 𝕜 H]
-  (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) :
-  (E →L[𝕜] H) ≃L[𝕜] (F →L[𝕜] G) :=
-arrow_congrSL e₁ e₂
-
 end
 
 end continuous_linear_equiv

src/geometry/manifold/vector_bundle/basic.lean

@@ -394,7 +394,7 @@ end with_topology
 
 namespace vector_prebundle
 
-variables {F E}
+variables [∀ x, topological_space (E x)] {F E}
 
 /-- Mixin for a `vector_prebundle` stating smoothness of coordinate changes. -/
 class is_smooth (a : vector_prebundle 𝕜 F E) : Prop :=
@@ -438,7 +438,7 @@ variables (IB)
 /-- Make a `smooth_vector_bundle` from a `smooth_vector_prebundle`.  -/
 lemma smooth_vector_bundle :
   @smooth_vector_bundle _ _ F E _ _ _ _ _ _ IB _ _ _ _ _ _ _
-    a.total_space_topology a.fiber_topology a.to_fiber_bundle a.to_vector_bundle :=
+    a.total_space_topology _ a.to_fiber_bundle a.to_vector_bundle :=
 { smooth_on_coord_change := begin
     rintros _ _ ⟨e, he, rfl⟩ ⟨e', he', rfl⟩,
     refine (a.smooth_on_smooth_coord_change he he').congr _,

src/geometry/manifold/vector_bundle/hom.lean

@@ -23,15 +23,16 @@ open_locale manifold bundle
 variables {𝕜 B F F₁ F₂ M M₁ M₂ : Type*}
   {E : B → Type*} {E₁ : B → Type*} {E₂ : B → Type*}
   [nontrivially_normed_field 𝕜]
-  [∀ x, add_comm_monoid (E x)] [∀ x, module 𝕜 (E x)]
+  [∀ x, add_comm_group (E x)] [∀ x, module 𝕜 (E x)]
   [normed_add_comm_group F] [normed_space 𝕜 F]
   [topological_space (total_space E)] [∀ x, topological_space (E x)]
-  [∀ x, add_comm_monoid (E₁ x)] [∀ x, module 𝕜 (E₁ x)]
+  [∀ x, add_comm_group (E₁ x)] [∀ x, module 𝕜 (E₁ x)]
   [normed_add_comm_group F₁] [normed_space 𝕜 F₁]
   [topological_space (total_space E₁)] [∀ x, topological_space (E₁ x)]
-  [∀ x, add_comm_monoid (E₂ x)] [∀ x, module 𝕜 (E₂ x)]
+  [∀ x, add_comm_group (E₂ x)] [∀ x, module 𝕜 (E₂ x)]
   [normed_add_comm_group F₂] [normed_space 𝕜 F₂]
   [topological_space (total_space E₂)] [∀ x, topological_space (E₂ x)]
+  [_i₁ : ∀ x, topological_add_group (E₂ x)] [_i₂ : ∀ x, has_continuous_smul 𝕜 (E₂ x)]
 
   {EB : Type*} [normed_add_comm_group EB] [normed_space 𝕜 EB]
   {HB : Type*} [topological_space HB] (IB : model_with_corners 𝕜 EB HB)
@@ -67,10 +68,11 @@ begin
   { intros b hb, ext L v,
     simp only [continuous_linear_map_coord_change, continuous_linear_equiv.coe_coe,
       continuous_linear_equiv.arrow_congrSL_apply, comp_apply, function.comp, compL_apply,
-      flip_apply, continuous_linear_equiv.symm_symm] },
+      flip_apply, continuous_linear_equiv.symm_symm, linear_equiv.to_fun_eq_coe,
+      continuous_linear_equiv.arrow_congrₛₗ_apply, continuous_linear_map.coe_comp'] },
 end
 
-variables [∀ x, has_continuous_add (E₂ x)] [∀ x, has_continuous_smul 𝕜 (E₂ x)]
+include _i₁ _i₂
 
 lemma hom_chart (y₀ y : LE₁E₂) :
   chart_at (model_prod HB (F₁ →L[𝕜] F₂)) y₀ y =
@@ -107,15 +109,6 @@ instance bundle.continuous_linear_map.vector_prebundle.is_smooth :
       continuous_linear_map_coord_change_apply (ring_hom.id 𝕜) e₁ e₁' e₂ e₂'⟩
   end }
 
-/-- Todo: remove this definition. It is probably needed because of the type-class pi bug
-https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/vector.20bundles.20--.20typeclass.20inference.20issue
--/
-@[reducible]
-def smooth_vector_bundle.continuous_linear_map.aux (x) :
-  topological_space (bundle.continuous_linear_map (ring_hom.id 𝕜) F₁ E₁ F₂ E₂ x) :=
-by apply_instance
-local attribute [instance, priority 1] smooth_vector_bundle.continuous_linear_map.aux
-
 instance smooth_vector_bundle.continuous_linear_map :
   smooth_vector_bundle (F₁ →L[𝕜] F₂) (bundle.continuous_linear_map (ring_hom.id 𝕜) F₁ E₁ F₂ E₂)
     IB :=

src/topology/algebra/module/strong_topology.lean

@@ -227,3 +227,86 @@ continuous_linear_map.has_basis_nhds_zero_of_basis (𝓝 0).basis_sets
 end bounded_sets
 
 end continuous_linear_map
+
+open continuous_linear_map
+
+namespace continuous_linear_equiv
+
+section semilinear
+
+variables {𝕜 : Type*} {𝕜₂ : Type*} {𝕜₃ : Type*} {𝕜₄ : Type*}
+  {E : Type*} {F : Type*} {G : Type*} {H : Type*}
+  [add_comm_group E] [add_comm_group F] [add_comm_group G] [add_comm_group H]
+  [nontrivially_normed_field 𝕜] [nontrivially_normed_field 𝕜₂] [nontrivially_normed_field 𝕜₃]
+    [nontrivially_normed_field 𝕜₄]
+  [module 𝕜 E] [module 𝕜₂ F] [module 𝕜₃ G] [module 𝕜₄ H]
+  [topological_space E] [topological_space F] [topological_space G] [topological_space H]
+  [topological_add_group G] [topological_add_group H]
+  [has_continuous_const_smul 𝕜₃ G] [has_continuous_const_smul 𝕜₄ H]
+  {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄}
+    {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄}
+  [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] [ring_hom_inv_pair σ₃₄ σ₄₃]
+    [ring_hom_inv_pair σ₄₃ σ₃₄]
+  [ring_hom_comp_triple σ₂₁ σ₁₄ σ₂₄] [ring_hom_comp_triple σ₂₄ σ₄₃ σ₂₃]
+    [ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃] [ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄]
+
+include σ₁₄ σ₂₄ σ₁₃ σ₃₄ σ₂₁ σ₂₃
+
+/-- A pair of continuous (semi)linear equivalences generates a (semi)linear equivalence between the
+spaces of continuous (semi)linear maps. -/
+@[simps] def arrow_congrₛₗ (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) :
+  (E →SL[σ₁₄] H) ≃ₛₗ[σ₄₃] (F →SL[σ₂₃] G) :=
+{ -- given explicitly to help `simps`
+  to_fun := λ L, (e₄₃ : H →SL[σ₄₃] G).comp (L.comp (e₁₂.symm : F →SL[σ₂₁] E)),
+  -- given explicitly to help `simps`
+  inv_fun := λ L, (e₄₃.symm : G →SL[σ₃₄] H).comp (L.comp (e₁₂ : E →SL[σ₁₂] F)),
+  map_add' := λ f g, by rw [add_comp, comp_add],
+  map_smul' := λ t f, by rw [smul_comp, comp_smulₛₗ],
+  .. e₁₂.arrow_congr_equiv e₄₃, }
+
+variables [ring_hom_isometric σ₂₁]
+
+lemma arrow_congrₛₗ_continuous (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) :
+  continuous (id (e₁₂.arrow_congrₛₗ e₄₃ : (E →SL[σ₁₄] H) ≃ₛₗ[σ₄₃] (F →SL[σ₂₃] G))) :=
+begin
+  apply continuous_of_continuous_at_zero,
+  show filter.tendsto _ _ _,
+  simp_rw [(e₁₂.arrow_congrₛₗ e₄₃).map_zero],
+  rw continuous_linear_map.has_basis_nhds_zero.tendsto_iff
+    continuous_linear_map.has_basis_nhds_zero,
+  rintros ⟨sF, sG⟩ ⟨h1 : bornology.is_vonN_bounded 𝕜₂ sF, h2 : sG ∈ nhds (0:G)⟩,
+  dsimp,
+  refine ⟨(e₁₂.symm '' sF, e₄₃ ⁻¹' sG), ⟨h1.image (e₁₂.symm : F →SL[σ₂₁] E), _⟩,
+    λ _ h _ hx, h _ (set.mem_image_of_mem _ hx)⟩,
+  apply e₄₃.continuous.continuous_at,
+  simpa using h2,
+end
+
+variables [ring_hom_isometric σ₁₂]
+
+/-- A pair of continuous (semi)linear equivalences generates an continuous (semi)linear equivalence
+between the spaces of continuous (semi)linear maps. -/
+@[simps] def arrow_congrSL (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) :
+  (E →SL[σ₁₄] H) ≃SL[σ₄₃] (F →SL[σ₂₃] G) :=
+{ continuous_to_fun := e₁₂.arrow_congrₛₗ_continuous e₄₃,
+  continuous_inv_fun := e₁₂.symm.arrow_congrₛₗ_continuous e₄₃.symm,
+  .. e₁₂.arrow_congrₛₗ e₄₃, }
+
+end semilinear
+
+section linear
+variables {𝕜 : Type*} {E : Type*} {F : Type*} {G : Type*} {H : Type*}
+  [add_comm_group E] [add_comm_group F] [add_comm_group G] [add_comm_group H]
+  [nontrivially_normed_field 𝕜] [module 𝕜 E] [module 𝕜 F] [module 𝕜 G] [module 𝕜 H]
+  [topological_space E] [topological_space F] [topological_space G] [topological_space H]
+  [topological_add_group G] [topological_add_group H]
+  [has_continuous_const_smul 𝕜 G] [has_continuous_const_smul 𝕜 H]
+
+/-- A pair of continuous linear equivalences generates an continuous linear equivalence between
+the spaces of continuous linear maps. -/
+def arrow_congr (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) : (E →L[𝕜] H) ≃L[𝕜] (F →L[𝕜] G) :=
+e₁.arrow_congrSL e₂
+
+end linear
+
+end continuous_linear_equiv

src/topology/constructions.lean

@@ -680,6 +680,14 @@ lemma inducing.prod_mk {f : α → β} {g : γ → δ} (hf : inducing f) (hg : i
 ⟨by rw [prod.topological_space, prod.topological_space, hf.induced, hg.induced,
          induced_compose, induced_compose, induced_inf, induced_compose, induced_compose]⟩
 
+@[simp] lemma inducing_const_prod {a : α} {f : β → γ} : inducing (λ x, (a, f x)) ↔ inducing f :=
+by simp_rw [inducing_iff, prod.topological_space, induced_inf, induced_compose, function.comp,
+    induced_const, top_inf_eq]
+
+@[simp] lemma inducing_prod_const {b : β} {f : α → γ} : inducing (λ x, (f x, b)) ↔ inducing f :=
+by simp_rw [inducing_iff, prod.topological_space, induced_inf, induced_compose, function.comp,
+    induced_const, inf_top_eq]
+
 lemma embedding.prod_mk {f : α → β} {g : γ → δ} (hf : embedding f) (hg : embedding g) :
   embedding (λx:α×γ, (f x.1, g x.2)) :=
 { inj := assume ⟨x₁, x₂⟩ ⟨y₁, y₂⟩, by simp; exact assume h₁ h₂, ⟨hf.inj h₁, hg.inj h₂⟩,

src/topology/fiber_bundle/basic.lean

@@ -705,6 +705,7 @@ end fiber_bundle_core
 /-! ### Prebundle construction for constructing fiber bundles -/
 
 variables (F) (E : B → Type*) [topological_space B] [topological_space F]
+  [Π x, topological_space (E x)]
 
 /-- This structure permits to define a fiber bundle when trivializations are given as local
 equivalences but there is not yet a topology on the total space. The total space is hence given a
@@ -718,6 +719,7 @@ structure fiber_prebundle :=
 (pretrivialization_mem_atlas : ∀ x : B, pretrivialization_at x ∈ pretrivialization_atlas)
 (continuous_triv_change : ∀ e e' ∈ pretrivialization_atlas,
   continuous_on (e ∘ e'.to_local_equiv.symm) (e'.target ∩ (e'.to_local_equiv.symm ⁻¹' e.source)))
+(total_space_mk_inducing : ∀ (b : B), inducing ((pretrivialization_at b) ∘ (total_space_mk b)))
 
 namespace fiber_prebundle
 
@@ -799,19 +801,27 @@ begin
   exact a.mem_base_pretrivialization_at b,
 end
 
-/-- Topology on the fibers `E b` induced by the map `E b → E.total_space`. -/
-def fiber_topology (b : B) : topological_space (E b) :=
-topological_space.induced (total_space_mk b) a.total_space_topology
-
-@[continuity] lemma inducing_total_space_mk (b : B) :
-  @inducing _ _ (a.fiber_topology b) a.total_space_topology (total_space_mk b) :=
-by { letI := a.total_space_topology, letI := a.fiber_topology b, exact ⟨rfl⟩ }
-
 @[continuity] lemma continuous_total_space_mk (b : B) :
-  @continuous _ _ (a.fiber_topology b) a.total_space_topology (total_space_mk b) :=
+  @continuous _ _ _ a.total_space_topology (total_space_mk b) :=
 begin
-  letI := a.total_space_topology, letI := a.fiber_topology b,
-  exact (a.inducing_total_space_mk b).continuous
+  letI := a.total_space_topology,
+  let e := a.trivialization_of_mem_pretrivialization_atlas (a.pretrivialization_mem_atlas b),
+  rw e.to_local_homeomorph.continuous_iff_continuous_comp_left
+    (a.total_space_mk_preimage_source b),
+  exact continuous_iff_le_induced.mpr (le_antisymm_iff.mp (a.total_space_mk_inducing b).induced).1,
+end
+
+lemma inducing_total_space_mk_of_inducing_comp (b : B)
+  (h : inducing ((a.pretrivialization_at b) ∘ (total_space_mk b))) :
+  @inducing _ _ _ a.total_space_topology (total_space_mk b) :=
+begin
+  letI := a.total_space_topology,
+  rw ←restrict_comp_cod_restrict (a.mem_trivialization_at_source b) at h,
+  apply inducing.of_cod_restrict (a.mem_trivialization_at_source b),
+  refine inducing_of_inducing_compose _ (continuous_on_iff_continuous_restrict.mp
+    (a.trivialization_of_mem_pretrivialization_atlas
+    (a.pretrivialization_mem_atlas b)).continuous_to_fun) h,
+  exact (a.continuous_total_space_mk b).cod_restrict (a.mem_trivialization_at_source b),
 end
 
 /-- Make a `fiber_bundle` from a `fiber_prebundle`.  Concretely this means
@@ -821,8 +831,9 @@ establishes that for the topology constructed on the sigma-type using
 `fiber_prebundle.total_space_topology`, these "pretrivializations" are actually
 "trivializations" (i.e., homeomorphisms with respect to the constructed topology). -/
 def to_fiber_bundle :
-  @fiber_bundle B F _ _ E a.total_space_topology a.fiber_topology :=
-{ total_space_mk_inducing := a.inducing_total_space_mk,
+  @fiber_bundle B F _ _ E a.total_space_topology _ :=
+{ total_space_mk_inducing := λ b, a.inducing_total_space_mk_of_inducing_comp b
+    (a.total_space_mk_inducing b),
   trivialization_atlas := {e | ∃ e₀ (he₀ : e₀ ∈ a.pretrivialization_atlas),
     e = a.trivialization_of_mem_pretrivialization_atlas he₀},
   trivialization_at := λ x, a.trivialization_of_mem_pretrivialization_atlas
@@ -833,7 +844,6 @@ def to_fiber_bundle :
 lemma continuous_proj : @continuous _ _ a.total_space_topology _ (π E) :=
 begin
   letI := a.total_space_topology,
-  letI := a.fiber_topology,
   letI := a.to_fiber_bundle,
   exact continuous_proj F E,
 end

src/topology/vector_bundle/basic.lean

@@ -733,7 +733,7 @@ end
 
 section
 variables [nontrivially_normed_field R] [∀ x, add_comm_monoid (E x)] [∀ x, module R (E x)]
-  [normed_add_comm_group F] [normed_space R F] [topological_space B]
+  [normed_add_comm_group F] [normed_space R F] [topological_space B] [∀ x, topological_space (E x)]
 
 open topological_space
 
@@ -760,6 +760,7 @@ structure vector_prebundle :=
   continuous_on f (e.base_set ∩ e'.base_set) ∧
   ∀ (b : B) (hb : b ∈ e.base_set ∩ e'.base_set) (v : F),
     f b v = (e' (total_space_mk b (e.symm b v))).2)
+(total_space_mk_inducing : ∀ (b : B), inducing ((pretrivialization_at b) ∘ (total_space_mk b)))
 
 namespace vector_prebundle
 
@@ -845,21 +846,13 @@ a.to_fiber_prebundle.mem_trivialization_at_source b x
   (total_space_mk b) ⁻¹' (a.pretrivialization_at b).source = univ :=
 a.to_fiber_prebundle.total_space_mk_preimage_source b
 
-/-- Topology on the fibers `E b` induced by the map `E b → E.total_space`. -/
-def fiber_topology (b : B) : topological_space (E b) :=
-a.to_fiber_prebundle.fiber_topology b
-
-@[continuity] lemma inducing_total_space_mk (b : B) :
-  @inducing _ _ (a.fiber_topology b) a.total_space_topology (total_space_mk b) :=
-a.to_fiber_prebundle.inducing_total_space_mk b
-
 @[continuity] lemma continuous_total_space_mk (b : B) :
-  @continuous _ _ (a.fiber_topology b) a.total_space_topology (total_space_mk b) :=
+  @continuous _ _ _ a.total_space_topology (total_space_mk b) :=
 a.to_fiber_prebundle.continuous_total_space_mk b
 
 /-- Make a `fiber_bundle` from a `vector_prebundle`; auxiliary construction for
 `vector_prebundle.vector_bundle`. -/
-def to_fiber_bundle : @fiber_bundle B F _ _ _ a.total_space_topology a.fiber_topology :=
+def to_fiber_bundle : @fiber_bundle B F _ _ _ a.total_space_topology _ :=
 a.to_fiber_prebundle.to_fiber_bundle
 
 /-- Make a `vector_bundle` from a `vector_prebundle`.  Concretely this means
@@ -869,7 +862,7 @@ establishes that for the topology constructed on the sigma-type using
 `vector_prebundle.total_space_topology`, these "pretrivializations" are actually
 "trivializations" (i.e., homeomorphisms with respect to the constructed topology). -/
 lemma to_vector_bundle :
-  @vector_bundle R _ F E _ _ _ _ _ _ a.total_space_topology a.fiber_topology a.to_fiber_bundle :=
+  @vector_bundle R _ F E _ _ _ _ _ _ a.total_space_topology _ a.to_fiber_bundle :=
 { trivialization_linear' := begin
     rintros _ ⟨e, he, rfl⟩,
     apply linear_of_mem_pretrivialization_atlas,
@@ -895,7 +888,7 @@ variables [normed_space 𝕜₁ F] [Π x, module 𝕜₁ (E x)] [topological_spa
 variables {F' : Type*} [normed_add_comm_group F'] [normed_space 𝕜₂ F']
   {E' : B' → Type*} [Π x, add_comm_monoid (E' x)] [Π x, module 𝕜₂ (E' x)]
   [topological_space (total_space E')]
-variables [Π x, topological_space (E x)] [fiber_bundle F E] [vector_bundle 𝕜₁ F E]
+variables [fiber_bundle F E] [vector_bundle 𝕜₁ F E]
 variables [Π x, topological_space (E' x)] [fiber_bundle F' E'] [vector_bundle 𝕜₂ F' E']
 variables (F E F' E')