Clean-up

Author: grunweg

Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative.lean

@@ -594,6 +594,23 @@ lemma differenceAux_tensorial (cov cov' : CovariantDerivative I F V) [T2Space M]
       rw [cov.addσ, cov'.addσ] <;> try assumption
       abel
 
+omit [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] in
+/-- A scalar product `f • s` of a smooth bump function `f` with a section `s` is smooth
+when `s` is smooth on some open set `a` such that `tsupport f ⊆ a`.
+This is a more global version of `contMDiff_of_tsupport` (which does not apply, as it assumes the
+co-domain has a zero: the total space of a vector bundle has none). -/
+lemma ContMDiff.of_contMDiffOn_smul_bump_function [T2Space M] [IsManifold I ∞ M]
+    {s : (x : M) → V x} {a : Set M} (ha : IsOpen a) (hn : n ≤ ∞)
+    (hs : ContMDiffOn I (I.prod 𝓘(ℝ, F)) n (fun x' ↦ TotalSpace.mk' F x' (s x')) a)
+    {ψ : SmoothBumpFunction I x} (hψ : tsupport ψ ⊆ a) :
+    ContMDiff I (I.prod 𝓘(ℝ, F)) n (fun x' ↦ TotalSpace.mk' F x' (ψ x' • s x')) := by
+  refine contMDiff_of_contMDiffOn_union_of_isOpen ?_ ?_ ?_ ha (t := (tsupport ψ)ᶜ) ?_
+  · exact contMDiffOn_smul_section hs (ψ.contMDiff.of_le hn).contMDiffOn
+  · apply (contMDiff_zeroSection _ _).contMDiffOn.congr fun y hy ↦ ?_
+    simpa [extend, zeroSection] using Or.inl <| image_eq_zero_of_notMem_tsupport hy
+  · exact Set.compl_subset_iff_union.mp <| Set.compl_subset_compl.mpr hψ
+  · exact isOpen_compl_iff.mpr <| isClosed_tsupport ψ
+
 -- TODO: either change `localFrame` to make sure it is everywhere smooth
 -- or introduce a cut-off here. First option is probaly better.
 -- TODO: comment why we chose the second option in the end, and adapt the definition accordingly
@@ -646,16 +663,8 @@ lemma contMDiff_extend [IsManifold I ∞ M] [FiniteDimensional ℝ F] [T2Space M
   -- XXX: extract ψ and hψ as helper declarations, perhaps private to prevent API leakage?
   let hψ :=
     Classical.choose_spec <| (SmoothBumpFunction.nhds_basis_support (I := I) ht).mem_iff.1 ht
-  -- XXX: can a version for a bump function make this result easier to use?
-  refine contMDiff_of_contMDiffOn_union_of_isOpen ?_ ?_ ?_ t.open_baseSet (t := (tsupport ψ)ᶜ) ?_
-  · apply contMDiffOn_smul_section ?_ ψ.contMDiff.contMDiffOn
-    exact contMDiffOn_localExtensionOn F (FiberBundle.mem_baseSet_trivializationAt' x) σ₀
-  · apply (contMDiff_zeroSection _ _).contMDiffOn.congr fun y hy ↦ ?_
-    simpa [extend, zeroSection] using Or.inl <| image_eq_zero_of_notMem_tsupport hy
-  · exact Set.compl_subset_iff_union.mp <| Set.compl_subset_compl.mpr hψ.1
-  · exact isOpen_compl_iff.mpr <| isClosed_tsupport ψ
-
-#exit
+  apply ContMDiff.of_contMDiffOn_smul_bump_function _ t.open_baseSet le_rfl ?_ hψ.1
+  exact contMDiffOn_localExtensionOn F (FiberBundle.mem_baseSet_trivializationAt' x) σ₀
 
 /-- The difference of two covariant derivatives, as a tensorial map -/
 noncomputable def difference [FiniteDimensional ℝ F] [T2Space M] [FiniteDimensional ℝ E] [IsManifold I 1 M]
@@ -705,8 +714,8 @@ noncomputable def endomorph_of_trivial_aux [FiniteDimensional ℝ E] [FiniteDime
       cov (extend 𝓘(ℝ, E) E X (x := x)) (extend 𝓘(ℝ, E) E' y (x := x)) x +
         cov (extend 𝓘(ℝ, E) E X (x := x)) (extend 𝓘(ℝ, E) E' y' (x := x)) x := by
       apply cov.addσ
-      · exact (contMDiff_extend _ _).mdifferentiableAt (n := 1) (hn := by norm_num)
-      · apply (contMDiff_extend _ _).mdifferentiableAt (n := 1) (hn := by norm_num)
+      · exact (contMDiff_extend _ _).mdifferentiableAt (n := ∞) (hn := by norm_num)
+      · apply (contMDiff_extend _ _).mdifferentiableAt (n := ∞) (hn := by norm_num)
     simp [A, B]
     module
   map_smul' a v := by