fix(topology/fiber_bundle/basic): make argument of fiber_bundle_core.…

…to_topological_space implicit (#17678)

`ι` already occurs in the type of `Z`

src/geometry/manifold/tangent_bundle.lean

@@ -550,7 +550,7 @@ end
 variable (M)
 
 instance : topological_space TM :=
-(tangent_bundle_core I M).to_vector_bundle_core.to_topological_space (atlas H M)
+(tangent_bundle_core I M).to_vector_bundle_core.to_topological_space
 
 instance : charted_space (model_prod H E) TM :=
 (tangent_bundle_core I M).to_charted_space

src/topology/fiber_bundle/basic.lean

@@ -464,15 +464,13 @@ begin
     simp only [Z.coord_change_comp, hx, mem_inter_iff, and_self, mem_base_set_at], }
 end
 
-variable (ι)
-
 /-- Topological structure on the total space of a fiber bundle created from core, designed so
 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_as_local_equiv i).source ∩ (Z.local_triv_as_local_equiv i) ⁻¹' s}
 
-variables {ι} (b : B) (a : F)
+variables (b : B) (a : F)
 
 lemma open_source' (i : ι) : is_open (Z.local_triv_as_local_equiv i).source :=
 begin

src/topology/vector_bundle/basic.lean

@@ -537,14 +537,12 @@ fiber_bundle_core.triv_change ↑Z i j
   p ∈ (Z.triv_change i j).source ↔ p.1 ∈ Z.base_set i ∩ Z.base_set j :=
 fiber_bundle_core.mem_triv_change_source ↑Z i j p
 
-variable (ι)
-
 /-- Topological structure on the total space of a vector bundle created from core, designed so
 that all the local trivialization are continuous. -/
 instance to_topological_space : topological_space Z.total_space :=
-fiber_bundle_core.to_topological_space ι ↑Z
+Z.to_fiber_bundle_core.to_topological_space
 
-variables {ι} (b : B) (a : F)
+variables (b : B) (a : F)
 
 @[simp, mfld_simps] lemma coe_coord_change (i j : ι) :
   Z.to_fiber_bundle_core.coord_change i j b = Z.coord_change i j b := rfl