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

Mainly redesigning the `simp` strategy.

src/data/equiv/local_equiv.lean

@@ -368,6 +368,10 @@ lemma source_inter_preimage_inv_preimage (s : set α) :
   e.source ∩ e ⁻¹' (e.symm ⁻¹' s) = e.source ∩ s :=
 set.ext $ λ x, and.congr_right_iff.2 $ λ hx, by simp only [mem_preimage, e.left_inv hx]
 
+lemma source_inter_preimage_target_inter (s : set β) :
+  e.source ∩ (e ⁻¹' (e.target ∩ s)) = e.source ∩ (e ⁻¹' s) :=
+ext $ λ x, ⟨λ hx, ⟨hx.1, hx.2.2⟩, λ hx, ⟨hx.1, e.map_source hx.1, hx.2⟩⟩
+
 lemma target_inter_inv_preimage_preimage (s : set β) :
   e.target ∩ e.symm ⁻¹' (e ⁻¹' s) = e.target ∩ s :=
 e.symm.source_inter_preimage_inv_preimage _

src/data/set/basic.lean

@@ -1206,11 +1206,11 @@ rfl
 
 @[simp] theorem preimage_id' {s : set α} : (λ x, x) ⁻¹' s = s := rfl
 
-theorem preimage_const_of_mem {b : β} {s : set β} (h : b ∈ s) :
+@[simp] theorem preimage_const_of_mem {b : β} {s : set β} (h : b ∈ s) :
   (λ (x : α), b) ⁻¹' s = univ :=
 eq_univ_of_forall $ λ x, h
 
-theorem preimage_const_of_not_mem {b : β} {s : set β} (h : b ∉ s) :
+@[simp] theorem preimage_const_of_not_mem {b : β} {s : set β} (h : b ∉ s) :
   (λ (x : α), b) ⁻¹' s = ∅ :=
 eq_empty_of_subset_empty $ λ x hx, h hx
 

src/geometry/manifold/basic_smooth_bundle.lean

@@ -169,7 +169,7 @@ 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.base_set i = i.1.source := rfl
+  (Z.to_topological_fiber_bundle_core.local_triv_ext 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) :
@@ -500,7 +500,7 @@ them, noting in particular that the tangent bundle is a smooth manifold. -/
 variable (M)
 
 instance : topological_space (tangent_bundle I M) :=
-(tangent_bundle_core I M).to_topological_fiber_bundle_core.to_topological_space
+(tangent_bundle_core I M).to_topological_fiber_bundle_core.to_topological_space (atlas H M)
 
 instance : charted_space (model_prod H E) (tangent_bundle I M) :=
 (tangent_bundle_core I M).to_charted_space
@@ -554,7 +554,7 @@ begin
   { rintros ⟨x_fst, x_snd⟩,
     simp only [chart_at, basic_smooth_bundle_core.chart, tangent_bundle_core,
       continuous_linear_map.coe_id', basic_smooth_bundle_core.to_topological_fiber_bundle_core, A]
-      with mfld_simps},
+      with mfld_simps },
   show ((chart_at (model_prod H E) p).to_local_equiv).source = univ,
     by simp only [chart_at] with mfld_simps,
 end

src/topology/constructions.lean

@@ -131,6 +131,9 @@ continuous_snd.continuous_at
   (hf : continuous f) (hg : continuous g) : continuous (λx, (f x, g x)) :=
 continuous_inf_rng (continuous_induced_rng hf) (continuous_induced_rng hg)
 
+@[continuity] lemma continuous.prod.mk (a : α) : continuous (prod.mk a : β → α × β) :=
+continuous_const.prod_mk continuous_id'
+
 lemma continuous.prod_map {f : γ → α} {g : δ → β} (hf : continuous f) (hg : continuous g) :
   continuous (λ x : γ × δ, (f x.1, g x.2)) :=
 (hf.comp continuous_fst).prod_mk (hg.comp continuous_snd)

src/topology/continuous_on.lean

@@ -770,6 +770,13 @@ lemma continuous_on.preimage_open_of_open {f : α → β} {s : set α} {t : set
   (hf : continuous_on f s) (hs : is_open s) (ht : is_open t) : is_open (s ∩ f⁻¹' t) :=
 (continuous_on_open_iff hs).1 hf t ht
 
+lemma continuous_on.is_open_preimage {f : α → β} {s : set α} {t : set β} (h : continuous_on f s)
+  (hs : is_open s) (hp : f ⁻¹' t ⊆ s) (ht : is_open t) : is_open (f ⁻¹' t) :=
+begin
+  convert (continuous_on_open_iff hs).mp h t ht,
+  rw [inter_comm, inter_eq_self_of_subset_left hp],
+end
+
 lemma continuous_on.preimage_closed_of_closed {f : α → β} {s : set α} {t : set β}
   (hf : continuous_on f s) (hs : is_closed s) (ht : is_closed t) : is_closed (s ∩ f⁻¹' t) :=
 begin

src/topology/local_homeomorph.lean

@@ -209,6 +209,10 @@ lemma target_inter_inv_preimage_preimage (s : set β) :
   e.target ∩ e.symm ⁻¹' (e ⁻¹' s) = e.target ∩ s :=
 e.symm.source_inter_preimage_inv_preimage _
 
+lemma source_inter_preimage_target_inter (s : set β) :
+  e.source ∩ (e ⁻¹' (e.target ∩ s)) = e.source ∩ (e ⁻¹' s) :=
+e.to_local_equiv.source_inter_preimage_target_inter s
+
 /-- Two local homeomorphisms are equal when they have equal `to_fun`, `inv_fun` and `source`.
 It is not sufficient to have equal `to_fun` and `source`, as this only determines `inv_fun` on
 the target. This would only be true for a weaker notion of equality, arguably the right one,

src/topology/order.lean

@@ -270,6 +270,10 @@ lemma is_open_induced_iff [t : topological_space β] {s : set α} {f : α → β
   @is_open α (t.induced f) s ↔ (∃t, is_open t ∧ f ⁻¹' t = s) :=
 iff.rfl
 
+lemma is_open_induced_iff' [t : topological_space β] {s : set α} {f : α → β} :
+  (t.induced f).is_open s ↔ (∃t, is_open t ∧ f ⁻¹' t = s) :=
+iff.rfl
+
 lemma is_closed_induced_iff [t : topological_space β] {s : set α} {f : α → β} :
   @is_closed α (t.induced f) s ↔ (∃t, is_closed t ∧ f ⁻¹' t = s) :=
 begin
@@ -420,6 +424,15 @@ le_antisymm
   (coinduced_le_iff_le_induced.1 $ le_generate_from $ assume s hs,
     generate_open.basic _ $ mem_image_of_mem _ hs)
 
+lemma le_induced_generate_from {α β} [t : topological_space α] {b : set (set β)}
+  {f : α → β} (h : ∀ (a : set β), a ∈ b → is_open (f ⁻¹' a)) : t ≤ induced f (generate_from b) :=
+begin
+  rw induced_generate_from_eq,
+  apply le_generate_from,
+  simp only [mem_image, and_imp, forall_apply_eq_imp_iff₂, exists_imp_distrib],
+  exact h,
+end
+
 /-- This construction is left adjoint to the operation sending a topology on `α`
   to its neighborhood filter at a fixed point `a : α`. -/
 protected def topological_space.nhds_adjoint (a : α) (f : filter α) : topological_space α :=

src/topology/topological_fiber_bundle.lean

@@ -736,8 +736,14 @@ instance [inhabited B] [inhabited (E (default B))] :
 @[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`. -/
@@ -757,6 +763,16 @@ 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
@@ -781,8 +797,6 @@ structure topological_fiber_bundle_core (ι : Type*) (B : Type*) [topological_sp
 (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)
 
-attribute [simp, mfld_simps] topological_fiber_bundle_core.mem_base_set_at
-
 namespace topological_fiber_bundle_core
 
 variables [topological_space B] [topological_space F] (Z : topological_fiber_bundle_core ι B F)
@@ -872,56 +886,65 @@ def local_triv' (i : ι) : local_equiv Z.total_space (B × F) :=
     dsimp,
     rw [Z.coord_change_comp, Z.coord_change_self],
     { exact Z.mem_base_set_at _ },
-    { simp [hx] }
+    { simp only [hx, mem_inter_eq, and_self, mem_base_set_at] }
   end,
   right_inv' := begin
     rintros ⟨x, v⟩ hx,
     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 [hx] }
+    { simp only [hx, mem_inter_eq, and_self, mem_base_set_at]}
   end }
 
-@[simp, mfld_simps] lemma mem_local_triv'_source (i : ι) (p : Z.total_space) :
+variable (i : ι)
+
+lemma mem_local_triv'_source (p : Z.total_space) :
   p ∈ (Z.local_triv' i).source ↔ p.1 ∈ Z.base_set i :=
 iff.rfl
 
-@[simp, mfld_simps] lemma mem_local_triv'_target (i : ι) (p : B × F) :
-  p ∈ (Z.local_triv' i).target ↔ p.1 ∈ Z.base_set i :=
+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 }
 
-@[simp, mfld_simps] lemma local_triv'_apply (i : ι) (p : Z.total_space) :
+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 local_triv'_symm_apply (i : ι) (p : B × F) :
+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
 
 /-- 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 :=
 begin
   split,
-  { ext x, erw [mem_prod], simp [local_equiv.trans_source] },
+  { ext x,
+    erw [mem_prod],
+    simp only [mem_local_triv'_source, mem_local_triv'_target, local_triv'_symm_apply]
+      with mfld_simps, },
   { 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 [Z.coord_change_comp, hx], }
+    simp only [Z.coord_change_comp, hx, mem_inter_eq, and_self, mem_base_set_at], }
 end
 
+variable (ι)
+
 /-- Topological structure on the total space of a topological 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' i).source ∩ (Z.local_triv' i) ⁻¹' s}
 
+variable {ι}
+
 lemma open_source' (i : ι) : is_open (Z.local_triv' 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 with mfld_simps
+  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]
 end
 
 lemma open_target' (i : ι) : is_open (Z.local_triv' i).target :=
@@ -959,21 +982,28 @@ def local_triv (i : ι) : local_homeomorph Z.total_space (B × F) :=
   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. -/
 
-@[simp, mfld_simps] lemma mem_local_triv_source (i : ι) (p : Z.total_space) :
+lemma mem_local_triv_source (p : Z.total_space) :
   p ∈ (Z.local_triv i).source ↔ p.1 ∈ Z.base_set i :=
 iff.rfl
 
-@[simp, mfld_simps] lemma mem_local_triv_target (i : ι) (p : B × F) :
-  p ∈ (Z.local_triv i).target ↔ p.1 ∈ Z.base_set i :=
+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 }
 
-@[simp, mfld_simps] lemma local_triv_apply (i : ι) (p : Z.total_space) :
+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 local_triv_symm_fst (i : ι) (p : B × F) :
+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. -/
@@ -988,7 +1018,8 @@ def local_triv_ext (i : ι) : bundle_trivialization F Z.proj :=
   open_base_set := Z.is_open_base_set i,
   source_eq     := rfl,
   target_eq     := rfl,
-  proj_to_fun   := λp hp, by simp,
+  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 }
 
 /-- A topological fiber bundle constructed from core is indeed a topological fiber bundle. -/
@@ -1003,29 +1034,13 @@ Z.is_topological_fiber_bundle.continuous_proj
 lemma is_open_map_proj : is_open_map Z.proj :=
 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 local homeomorphism -/
-def local_triv_at (p : Z.total_space) :
-  local_homeomorph Z.total_space (B × F) :=
-Z.local_triv (Z.index_at (Z.proj p))
-
-@[simp, mfld_simps] lemma mem_local_triv_at_source (p : Z.total_space) :
-  p ∈ (Z.local_triv_at p).source :=
-by simp [local_triv_at]
-
-@[simp, mfld_simps] lemma local_triv_at_fst (p q : Z.total_space) :
-  ((Z.local_triv_at p) q).1 = q.1 := rfl
-
-@[simp, mfld_simps] lemma local_triv_at_symm_fst (p : Z.total_space) (q : B × F) :
-  ((Z.local_triv_at p).symm q).1 = q.1 := rfl
-
 /-- Preferred local trivialization of a fiber bundle constructed from core, at a given point, as
 a bundle trivialization -/
-def local_triv_at_ext (p : Z.total_space) : bundle_trivialization F Z.proj :=
-Z.local_triv_ext (Z.index_at (Z.proj p))
+def local_triv_at_ext (b : B) : bundle_trivialization F Z.proj :=
+Z.local_triv_ext (Z.index_at b)
 
-@[simp, mfld_simps] lemma local_triv_at_ext_to_local_homeomorph (p : Z.total_space) :
-  (Z.local_triv_at_ext p).to_local_homeomorph = Z.local_triv_at p := rfl
+@[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
 
 /-- 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
@@ -1044,10 +1059,79 @@ begin
     have : continuous_on (λ (y : B), v) (Z.base_set (Z.index_at x)) := continuous_on_const,
     apply (this.congr _).continuous_at A,
     assume y hy,
-    simp only [h, hy] with mfld_simps },
+    simp only [h, hy, mem_base_set_at] with mfld_simps },
   { 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_target :
+  (Z.local_triv i).target = (Z.local_triv_ext i).target := 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 base_set_at : Z.base_set i = (Z.local_triv_ext i).base_set := 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 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 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_ext_target (p : B × F) :
+  p ∈ (Z.local_triv_ext i).target ↔ p.1 ∈ (Z.local_triv_ext 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 =
+    ⟨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 }
+
+@[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, }
+
+open bundle
+
+/-- The inclusion of a fiber into the total space is a continuous map. -/
+lemma continuous_total_space_mk (b : B) : continuous (λ a, total_space_mk Z.fiber b a) :=
+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],
+  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],
+  apply is_open.inter,
+  { simp only [bundle.proj, proj, ←preimage_comp],
+    by_cases (b ∈ (Z.local_triv_ext 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],
+    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,
+        refine ((Z.coord_change_continuous (Z.index_at b) i).comp ((continuous_const).prod_mk
+          continuous_id).continuous_on) (by { convert (subset_univ univ),
+            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],
+      exact is_open_empty, }}
+end
+
 end topological_fiber_bundle_core
 
 variables (F) {Z : Type*} [topological_space B] [topological_space F] {proj : Z → B}