fix(topology/fiber_bundle/basic): rename field of fiber_bundle_core (#17679)

* Also add a `simps` attribute on one construction.

Author: fpvandoorn

src/geometry/manifold/tangent_bundle.lean

@@ -196,7 +196,7 @@ def to_vector_bundle_core : vector_bundle_core 𝕜 M F (atlas H M) :=
     { simp only [hx1] with mfld_simps },
     { simp only [hx1, hx2, hx3] with mfld_simps }
   end,
-  coord_change_continuous := λ i j, begin
+  continuous_on_coord_change := λ i j, begin
     refine ((Z.coord_change_continuous i j).comp' i.1.continuous_on).mono _,
     rintros p ⟨hp₁, hp₂⟩,
     refine ⟨hp₁, i.1.maps_to hp₁, _⟩,

src/topology/fiber_bundle/basic.lean

@@ -328,7 +328,7 @@ structure fiber_bundle_core (ι : Type*) (B : Type*) [topological_space B]
 (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)
+(continuous_on_coord_change : ∀ i j, continuous_on (λp : B × F, coord_change i j p.1 p.2)
                                                (((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 j k x) (coord_change i j x v) = coord_change i k x v)
@@ -395,9 +395,9 @@ def triv_change (i j : ι) : local_homeomorph (B × F) (B × F) :=
   open_target :=
     (is_open.inter (Z.is_open_base_set i) (Z.is_open_base_set j)).prod is_open_univ,
   continuous_to_fun  :=
-    continuous_on.prod continuous_fst.continuous_on (Z.coord_change_continuous i j),
+    continuous_on.prod continuous_fst.continuous_on (Z.continuous_on_coord_change i j),
   continuous_inv_fun := by simpa [inter_comm]
-    using continuous_on.prod continuous_fst.continuous_on (Z.coord_change_continuous j i) }
+    using continuous_on.prod continuous_fst.continuous_on (Z.continuous_on_coord_change j i) }
 
 @[simp, mfld_simps] lemma mem_triv_change_source (i j : ι) (p : B × F) :
   p ∈ (Z.triv_change i j).source ↔ p.1 ∈ Z.base_set i ∩ Z.base_set j :=
@@ -623,7 +623,7 @@ begin
     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),
-        from (Z.coord_change_continuous (Z.index_at b) i).comp_continuous
+        from (Z.continuous_on_coord_change (Z.index_at b) i).comp_continuous
           (continuous_const.prod_mk continuous_id) (λ x, ⟨⟨Z.mem_base_set_at b, h⟩, mem_univ x⟩),
       exact (((Z.local_triv i).open_target.inter ht).preimage (continuous.prod.mk b)).preimage hc },
     { rw [(Z.local_triv i).target_eq, ←base_set_at, mk_preimage_prod_right_eq_empty h,

src/topology/vector_bundle/basic.lean

@@ -458,7 +458,7 @@ structure vector_bundle_core (ι : Type*) :=
 (mem_base_set_at   : ∀ x, x ∈ base_set (index_at x))
 (coord_change      : ι → ι → B → (F →L[R] F))
 (coord_change_self : ∀ i, ∀ x ∈ base_set i, ∀ v, coord_change i i x v = v)
-(coord_change_continuous : ∀ i j, continuous_on (coord_change i j) (base_set i ∩ base_set j))
+(continuous_on_coord_change : ∀ i j, continuous_on (coord_change i j) (base_set i ∩ base_set j))
 (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)
 
@@ -473,7 +473,7 @@ def trivial_vector_bundle_core (ι : Type*) [inhabited ι] :
   coord_change := λ i j x, continuous_linear_map.id R F,
   coord_change_self := λ i x hx v, rfl,
   coord_change_comp := λ i j k x hx v, rfl,
-  coord_change_continuous := λ i j, continuous_on_const }
+  continuous_on_coord_change := λ i j, continuous_on_const }
 
 instance (ι : Type*) [inhabited ι] : inhabited (vector_bundle_core R B F ι) :=
 ⟨trivial_vector_bundle_core R B F ι⟩
@@ -483,10 +483,10 @@ namespace vector_bundle_core
 variables {R B F} {ι : Type*} (Z : vector_bundle_core R B F ι)
 
 /-- Natural identification to a `fiber_bundle_core`. -/
-def to_fiber_bundle_core : fiber_bundle_core ι B F :=
+@[simps (mfld_cfg)] def to_fiber_bundle_core : fiber_bundle_core ι B F :=
 { coord_change := λ i j b, Z.coord_change i j b,
-  coord_change_continuous := λ i j, is_bounded_bilinear_map_apply.continuous.comp_continuous_on
-      ((Z.coord_change_continuous i j).prod_map continuous_on_id),
+  continuous_on_coord_change := λ i j, is_bounded_bilinear_map_apply.continuous.comp_continuous_on
+      ((Z.continuous_on_coord_change i j).prod_map continuous_on_id),
   ..Z }
 
 instance to_fiber_bundle_core_coe : has_coe (vector_bundle_core R B F ι)
@@ -625,7 +625,7 @@ instance vector_bundle : vector_bundle R F Z.fiber :=
   end,
   continuous_on_coord_change' := begin
     rintros _ _ ⟨i, rfl⟩ ⟨i', rfl⟩,
-    refine (Z.coord_change_continuous i i').congr (λ b hb, _),
+    refine (Z.continuous_on_coord_change i i').congr (λ b hb, _),
     ext v,
     exact Z.local_triv_coord_change_eq i i' hb v,
   end }