Clean-up

Author: grunweg

Mathlib/Geometry/Manifold/ContMDiff/Basic.lean

@@ -272,7 +272,9 @@ end const
 /-- `f` is continuously differentiable if it is cont. differentiable at
 each `x ∈ mulTSupport f`. -/
 @[to_additive "`f` is continuously differentiable if it is continuously
-differentiable at each `x ∈ tsupport f`."]
+differentiable at each `x ∈ tsupport f`.
+See also `ContMDiff.of_contMDiffOn_smul_bump_function` for the analogous result applying
+to sections of vector bundles (whose co-domain has no zero)."]
 theorem contMDiff_of_mulTSupport [One M'] {f : M → M'}
     (hf : ∀ x ∈ mulTSupport f, ContMDiffAt I I' n f x) : ContMDiff I I' n f := by
   intro x

Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative.lean

@@ -171,26 +171,6 @@ lemma contMDiff_of_contMDiffOn_iUnion_of_isOpen {ι : Type*} {s : ι → Set M}
   rw [← contMDiffOn_univ, ← hs']
   exact ContMDiffOn.iUnion_of_isOpen hf hs
 
-/-- A section is `C^n` whenever it is `C^n` on its support.
-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): in return for the additional
-generality, we need to add a hypothesis about the zero section being smooth. -/
-lemma ContMDiff.of_contMDiffOn_smul_bump_function [SMul 𝕜 M'] (hf : ContMDiffOn I I' n f s)
-    (hs : IsOpen s) {ψ : M → 𝕜} (hψ : ContMDiff I 𝓘(𝕜) n ψ) (hψ' : tsupport ψ ⊆ s)
-    -- XXX: is there a better abstraction of "the zero section"?
-    (hzero : ContMDiff I I' n (fun x ↦ (0 : 𝕜) • f x)) : ContMDiff I I' n (ψ • f) := by
-  apply contMDiff_of_contMDiffOn_union_of_isOpen ?_ ?_ ?_ hs
-    (isOpen_compl_iff.mpr <| isClosed_tsupport ψ)
-  · -- TODO: impose further typeclasses to make this true...
-    sorry -- scalar multiplication is C^n, for sections: will be done for local frames as well
-  · apply (hzero.contMDiffOn (s := (tsupport ψ)ᶜ)).congr
-    intro y hy
-    simp [image_eq_zero_of_notMem_tsupport hy]
-  · exact Set.compl_subset_iff_union.mp <| Set.compl_subset_compl.mpr hψ'
-
--- See also `ContMDiff.of_contMDiffOn_smul_bump_function` for the analogous result applying
--- to sections of vector bundles (whose co-domain has no zero).
-
 end contMDiff_union
 
 section contMDiff_addsmulfinsum_section