Extension smoothness is sorry-free

Author: grunweg

Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative.lean

@@ -196,7 +196,8 @@ end contMDiff_union
 section contMDiff_addsmulfinsum_section
 
 -- Proofs taken from SmoothSection: TODO golf those with these lemmas!
--- XXX: also add sub, neg, nsmul, zsmul lemmas? contMDiffWithinAt, contMDiffOn versions?
+-- XXX: also add sub, neg, nsmul, zsmul lemmas?
+-- TODO: add remaining contMDiffWithinAt, contMDiffOn versions
 
 variable {I F n V}
 
@@ -221,6 +222,22 @@ lemma contMDiff_add_section {s t : Π x : M, V x}
     ContMDiff I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x ((s + t) x)) :=
   fun x₀ ↦ contMDiffAt_add_section (hs x₀) (ht x₀)
 
+omit [IsManifold I 0 M] [∀ (x : M), IsTopologicalAddGroup (V x)]
+  [∀ (x : M), ContinuousSMul 𝕜 (V x)] in
+lemma contMDiffWithinAt_smul_section {f : M → 𝕜} {s : Π x : M, V x} {t : Set M} {x₀ : M}
+    (hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) t x₀)
+    (hf : ContMDiffWithinAt I 𝓘(𝕜) n f t x₀) :
+    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (f x • s x)) t x₀ := by
+  rw [contMDiffWithinAt_section] at hs ⊢
+  set e := trivializationAt F V x₀
+  refine (hf.smul hs).congr_of_eventuallyEq ?_ ?_
+  · apply eventually_of_mem (U := e.baseSet)
+    · exact mem_nhdsWithin_of_mem_nhds <|
+        (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀)
+    · intro x hx
+      apply (e.linear 𝕜 hx).2
+  · apply (e.linear 𝕜 (FiberBundle.mem_baseSet_trivializationAt' x₀)).2
+
 omit [IsManifold I 0 M] [∀ (x : M), IsTopologicalAddGroup (V x)]
   [∀ (x : M), ContinuousSMul 𝕜 (V x)] in
 lemma contMDiffAt_smul_section {f : M → 𝕜} {s : Π x : M, V x} {x₀ : M}
@@ -240,7 +257,7 @@ lemma contMDiffOn_smul_section {f : M → 𝕜} {s : Π x : M, V x} {t : Set M}
     (hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) t)
     (hf : ContMDiffOn I 𝓘(𝕜) n f t) :
     ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (f x • s x)) t :=
-  sorry -- fun x₀ ↦ contMDiffAt_smul_section (hs x₀) (hf x₀)
+  fun x₀ hx₀ ↦ contMDiffWithinAt_smul_section (hs x₀ hx₀) (hf x₀ hx₀)
 
 omit [IsManifold I 0 M] [∀ (x : M), IsTopologicalAddGroup (V x)]
   [∀ (x : M), ContinuousSMul 𝕜 (V x)] in