more

SphereEversion/ToMathlib/Unused/GeometryManifoldMisc.lean

@@ -35,7 +35,7 @@ theorem Filter.EventuallyEq.nhdsWithin_preimage_fst {z : α × β} {s : Set α}
 
 theorem eventually_mem_nhds_within' {α} [TopologicalSpace α] {s t : Set α} {a : α} :
     (∀ᶠ x in 𝓝[s] a, t ∈ 𝓝[s] x) ↔ t ∈ 𝓝[s] a :=
-  eventually_nhdsWithin_nhdsWithin
+  eventually_eventually_nhdsWithin
 
 theorem eventually_mem_nhds_within'' {α} [TopologicalSpace α] {s t : Set α} {a : α} :
     (∀ᶠ x in 𝓝 a, t ∈ 𝓝[s] x) ↔ t ∈ 𝓝[s] a :=
@@ -61,18 +61,17 @@ variable {𝕜 B F M : Type*} {E : B → Type*} [NontriviallyNormedField 𝕜] [
 
 theorem VectorBundleCore.smoothAt_coordChange {ι} (Z : VectorBundleCore 𝕜 B F ι) [Z.IsSmooth IB]
     (i j : ι) {x₀ : B} (hx₀ : x₀ ∈ Z.baseSet i ∩ Z.baseSet j) :
-    SmoothAt IB 𝓘(𝕜, F →L[𝕜] F) (Z.coordChange i j) x₀ :=
-  sorry -- proof was:
-  -- (/-Z.-/smoothOn_coordChangeL IB i j).SmoothAt <|
-  --  ((Z.isOpen_baseSet i).inter (Z.isOpen_baseSet j)).mem_nhds hx₀ -/
+    ContMDiffAt IB 𝓘(𝕜, F →L[𝕜] F) ⊤ (Z.coordChange i j) x₀ :=
+  (Z.contMDiffOn_coordChange IB i j).contMDiffAt <|
+    ((Z.isOpen_baseSet i).inter (Z.isOpen_baseSet j)).mem_nhds hx₀
 
 variable (IB)
-variable [SmoothManifoldWithCorners IB B] [SmoothVectorBundle F E IB]
+variable [SmoothVectorBundle F E IB]
 
 theorem smoothAt_coord_change (e e' : Trivialization F (π F E)) {x₀ : B}
     (hx₀ : x₀ ∈ e.baseSet ∩ e'.baseSet) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] :
-    SmoothAt IB 𝓘(𝕜, F →L[𝕜] F) (fun b : B ↦ (e.coordChangeL 𝕜 e' b : F →L[𝕜] F)) x₀ :=
-  sorry -- was: (smoothOn_coordChangeL e e').SmoothAt <| (e.open_baseSet.inter e'.open_baseSet).mem_nhds hx₀
+    ContMDiffAt IB 𝓘(𝕜, F →L[𝕜] F) ⊤ (fun b : B ↦ (e.coordChangeL 𝕜 e' b : F →L[𝕜] F)) x₀ :=
+  (contMDiffOn_coordChangeL e e').contMDiffAt <| (e.open_baseSet.inter e'.open_baseSet).mem_nhds hx₀
 
 variable {IB}
 
@@ -103,15 +102,15 @@ variable [SmoothManifoldWithCorners IB B] [SmoothVectorBundle F E IB]
 
 theorem Trivialization.smoothAt (e : Trivialization F (π F E)) [MemTrivializationAtlas e]
     {x₀ : TotalSpace F E} (hx₀ : x₀.proj ∈ e.baseSet) :
-    SmoothAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) e x₀ := by
+    ContMDiffAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) ⊤ e x₀ := by
   rw [smoothAt_prod]
-  refine ⟨(smoothAt_proj E).congr_of_eventuallyEq ?_, ?_⟩
+  refine ⟨(contMDiffAt_proj E).congr_of_eventuallyEq ?_, ?_⟩
   · exact eventually_of_mem (e.open_source.mem_nhds <| e.mem_source.mpr hx₀) fun x hx ↦ e.coe_fst hx
-  simp_rw [SmoothAt, contMDiffAt_iff_source_of_mem_source (mem_chart_source _ _)]
+  simp_rw [contMDiffAt_iff_source_of_mem_source (mem_chart_source _ _)]
   simp only [FiberBundle.extChartAt, Function.comp, prod_univ, mfld_simps]
   let e' := trivializationAt F E x₀.proj
   let c := (extChartAt IB x₀.proj).symm
-  have h0 := (extChartAt IB x₀.proj).left_inv (mem_extChartAt_source IB x₀.proj)
+  have h0 := (extChartAt IB x₀.proj).left_inv (mem_extChartAt_source x₀.proj)
   have : ContMDiffWithinAt 𝓘(𝕜, EB × F) 𝓘(𝕜, F) ⊤
       (fun x : EB × F ↦ e'.coordChangeL 𝕜 e (c x.1) x.2)
       (Prod.fst ⁻¹' range IB) (extChartAt IB x₀.proj x₀.proj, (e' x₀).2) := by
@@ -147,13 +146,14 @@ theorem Trivialization.smoothOn (e : Trivialization F (π F E)) [MemTrivializati
 
 theorem smoothAt_trivializationAt {x₀ : B} {x : TotalSpace F E}
     (hx : x.proj ∈ (trivializationAt F E x₀).baseSet) :
-    SmoothAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) (trivializationAt F E x₀) x :=
+    ContMDiffAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) ⊤ (trivializationAt F E x₀) x :=
   (trivializationAt F E x₀).smoothAt IB hx
 
+omit [SmoothManifoldWithCorners IB B] in
 theorem smoothOn_trivializationAt (x₀ : B) :
-    SmoothOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) (trivializationAt F E x₀)
+    ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) ⊤ (trivializationAt F E x₀)
       (trivializationAt F E x₀).source :=
-  (trivializationAt F E x₀).smoothOn IB
+  (trivializationAt F E x₀).contMDiffOn
 
 end VectorBundle