chore(topology/topological_fiber_bundle): reorganizing the code (#7938)

What I do here:
 - Get rid of `local_triv`: it is not needed.
 - Change `local_triv_ext` to `local_triv`
 - Rename `local_triv'` as `local_triv_as_local_equiv` (name suggested by @sgouezel)
 - Improve type class inference by getting rid of `dsimp` in instances
 - Move results about `bundle` that do not need the topology in an appropriate file
 - Update docs accordingly.

Nothing else.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

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

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

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 }⟩