feat: sections of a fiber bundle with Subsingleton fiber are smooth and differentiable (leanprover-community#41027)

This will be used to prove that the Levi-Civita connection is smooth.
From the path towards the Levi-Civita connection and Riemannian geometry.

Author: grunweg

Mathlib/Geometry/Manifold/VectorBundle/Basic.lean

@@ -230,6 +230,8 @@ theorem contMDiffWithinAt_proj {s : Set (TotalSpace F E)} {p : TotalSpace F E} :
     ContMDiffWithinAt (IB.prod 𝓘(𝕜, F)) IB n (π F E) s p :=
   (contMDiffAt_proj E).contMDiffWithinAt
 
+section
+
 variable (𝕜) [∀ x, AddCommMonoid (E x)]
 variable [∀ x, Module 𝕜 (E x)] [VectorBundle 𝕜 F E]
 
@@ -253,6 +255,35 @@ theorem contMDiffWithinAt_zeroSection {t : Set B} {x : B} :
     ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) n (zeroSection F E) t x :=
   (contMDiff_zeroSection _ _ x).contMDiffWithinAt
 
+end
+
+variable {s : ∀ x, E x} {u : Set B} {x : B}
+
+@[nontriviality]
+lemma contMDiffWithinAt_section_of_subsingleton [Subsingleton F] :
+    ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) u x := by
+  rw [contMDiffWithinAt_section]
+  apply contMDiffWithinAt_const |>.congr
+  · intro y _
+    apply Subsingleton.elim
+  rfl
+
+@[nontriviality]
+lemma contMDiffAt_section_of_subsingleton [Subsingleton F] :
+    ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) x := by
+  rw [← contMDiffWithinAt_univ]
+  apply contMDiffWithinAt_section_of_subsingleton
+
+@[nontriviality]
+lemma contMDiffOn_section_of_subsingleton [Subsingleton F] :
+    ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) u :=
+  fun _x _hx ↦ contMDiffWithinAt_section_of_subsingleton ..
+
+@[nontriviality]
+lemma contMDiff_section_of_subsingleton [Subsingleton F] :
+    ContMDiff IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) :=
+  fun _x ↦ contMDiffAt_section_of_subsingleton ..
+
 end Bundle
 
 end

Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean

@@ -99,6 +99,8 @@ theorem mdifferentiableWithinAt_proj {s : Set (TotalSpace F E)} {p : TotalSpace
     MDiffAt[s] (π F E) p :=
   (mdifferentiableAt_proj E).mdifferentiableWithinAt
 
+section
+
 variable (𝕜) [∀ x, AddCommMonoid (E x)]
 variable [∀ x, Module 𝕜 (E x)] [VectorBundle 𝕜 F E]
 
@@ -121,6 +123,28 @@ theorem mdifferentiableWithinAt_zeroSection {t : Set B} {x : B} :
     MDiffAt[t] (zeroSection F E) x :=
   (mdifferentiable_zeroSection _ _ x).mdifferentiableWithinAt
 
+end
+
+variable {s : ∀ x, E x} {u : Set B} {x : B}
+
+@[nontriviality]
+lemma mdifferentiableWithinAt_section_of_subsingleton [Subsingleton F] :
+    MDiffAt[u] (T% s) x :=
+  (contMDiffWithinAt_section_of_subsingleton _).mdifferentiableWithinAt one_ne_zero
+
+@[nontriviality]
+lemma mdifferentiableAt_section_of_subsingleton [Subsingleton F] : MDiffAt (T% s) x := by
+  rw [← mdifferentiableWithinAt_univ]
+  apply mdifferentiableWithinAt_section_of_subsingleton
+
+@[nontriviality]
+lemma mdifferentiableOn_section_of_subsingleton [Subsingleton F] : MDiff[u] (T% s) :=
+  fun _x _hx ↦ mdifferentiableWithinAt_section_of_subsingleton ..
+
+@[nontriviality]
+lemma mdifferentiable_section_of_subsingleton [Subsingleton F] : MDiff (T% s) :=
+  fun _x ↦ mdifferentiableAt_section_of_subsingleton ..
+
 end Bundle
 
 section coordChange