feat: add Trivialization.tendsto_nhds_iff (#5489)

This lemma generalizes `FiberBundle.continuousWithinAt_totalSpace`.
Also add a version with equality of filters.

Mathlib/Topology/FiberBundle/Basic.lean

@@ -304,28 +304,16 @@ open Trivialization
 theorem continuousWithinAt_totalSpace (f : X → TotalSpace E) {s : Set X} {x₀ : X} :
     ContinuousWithinAt f s x₀ ↔
       ContinuousWithinAt (fun x => (f x).proj) s x₀ ∧
-        ContinuousWithinAt (fun x => ((trivializationAt F E (f x₀).proj) (f x)).2) s x₀ := by
-  refine' (and_iff_right_iff_imp.2 fun hf => _).symm.trans (and_congr_right fun hf => _)
-  · refine' (continuous_proj F E).continuousWithinAt.comp hf (mapsTo_image f s)
-  have h1 : (fun x => (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet ∈ 𝓝[s] x₀ :=
-    hf.preimage_mem_nhdsWithin ((open_baseSet _).mem_nhds (mem_baseSet_trivializationAt F E _))
-  have h2 : ContinuousWithinAt (fun x => (trivializationAt F E (f x₀).proj (f x)).1) s x₀ := by
-    refine'
-      hf.congr_of_eventuallyEq (eventually_of_mem h1 fun x hx => _) trivializationAt_proj_fst
-    simp_rw [coe_fst' _ hx]
-  rw [(trivializationAt F E (f x₀).proj).continuousWithinAt_iff_continuousWithinAt_comp_left]
-  · simp_rw [continuousWithinAt_prod_iff, Function.comp, Trivialization.coe_coe, h2, true_and_iff]
-  · apply mem_trivializationAt_proj_source
-  · rwa [source_eq, preimage_preimage]
+        ContinuousWithinAt (fun x => ((trivializationAt F E (f x₀).proj) (f x)).2) s x₀ :=
+  (trivializationAt F E (f x₀).proj).tendsto_nhds_iff mem_trivializationAt_proj_source
 #align fiber_bundle.continuous_within_at_total_space FiberBundle.continuousWithinAt_totalSpace
 
 /-- Characterization of continuous functions (at a point) into a fiber bundle. -/
 theorem continuousAt_totalSpace (f : X → TotalSpace E) {x₀ : X} :
     ContinuousAt f x₀ ↔
       ContinuousAt (fun x => (f x).proj) x₀ ∧
-        ContinuousAt (fun x => ((trivializationAt F E (f x₀).proj) (f x)).2) x₀ := by
-  simp_rw [← continuousWithinAt_univ]
-  exact continuousWithinAt_totalSpace F f
+        ContinuousAt (fun x => ((trivializationAt F E (f x₀).proj) (f x)).2) x₀ :=
+  (trivializationAt F E (f x₀).proj).tendsto_nhds_iff mem_trivializationAt_proj_source
 #align fiber_bundle.continuous_at_total_space FiberBundle.continuousAt_totalSpace
 
 end FiberBundle

Mathlib/Topology/FiberBundle/Trivialization.lean

@@ -455,6 +455,25 @@ theorem image_preimage_eq_prod_univ {s : Set B} (hb : s ⊆ e.baseSet) :
     ⟨e.invFun p, mem_preimage.mpr ((e.proj_symm_apply hp').symm ▸ hp.1), e.apply_symm_apply hp'⟩
 #align trivialization.image_preimage_eq_prod_univ Trivialization.image_preimage_eq_prod_univ
 
+theorem tendsto_nhds_iff {l : Filter α} {f : α → Z} {z : Z} (hz : z ∈ e.source) :
+    Tendsto f l (𝓝 z) ↔
+      Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x ↦ (e (f x)).2) l (𝓝 (e z).2) := by
+  rw [e.nhds_eq_comap_inf_principal hz, tendsto_inf, tendsto_comap_iff, Prod.tendsto_iff, coe_coe,
+    tendsto_principal, coe_fst _ hz]
+  by_cases hl : ∀ᶠ x in l, f x ∈ e.source
+  · simp only [hl, and_true]
+    refine (tendsto_congr' ?_).and Iff.rfl
+    exact hl.mono fun x ↦ e.coe_fst
+  · simp only [hl, and_false, false_iff, not_and]
+    rw [e.source_eq] at hl hz
+    exact fun h _ ↦ hl <| h <| e.open_baseSet.mem_nhds hz
+
+theorem nhds_eq_inf_comap {z : Z} (hz : z ∈ e.source) :
+    𝓝 z = comap proj (𝓝 (proj z)) ⊓ comap (Prod.snd ∘ e) (𝓝 (e z).2) := by
+  refine eq_of_forall_le_iff fun l ↦ ?_
+  rw [le_inf_iff, ← tendsto_iff_comap, ← tendsto_iff_comap]
+  exact e.tendsto_nhds_iff hz
+
 /-- The preimage of a subset of the base set is homeomorphic to the product with the fiber. -/
 def preimageHomeomorph {s : Set B} (hb : s ⊆ e.baseSet) : proj ⁻¹' s ≃ₜ s × F :=
   (e.toLocalHomeomorph.homeomorphOfImageSubsetSource (e.preimage_subset_source hb)