feat: differentiable_of_subsingleton (leanprover-community#34831)

and move a lemma to a better location.

From the path towards immersions, submanifolds and the regular value theorem.

Author: grunweg

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

@@ -270,6 +270,9 @@ protected theorem HasFDerivWithinAt.empty : HasFDerivWithinAt f f' ∅ x := by
 protected theorem DifferentiableWithinAt.empty : DifferentiableWithinAt 𝕜 f ∅ x :=
   ⟨0, .empty⟩
 
+@[fun_prop]
+theorem differentiableOn_empty : DifferentiableOn 𝕜 f ∅ := fun _ => False.elim
+
 theorem HasFDerivWithinAt.of_finite [T1Space E] (h : s.Finite) : HasFDerivWithinAt f f' s x := by
   induction s, h using Set.Finite.induction_on with
   | empty => exact .empty

Mathlib/Analysis/Calculus/FDeriv/Const.lean

@@ -294,14 +294,23 @@ theorem hasFDerivWithinAt_singleton (f : E → F) (x : E) :
   simp only [HasFDerivWithinAt, nhdsWithin_singleton, hasFDerivAtFilter_iff_isLittleO,
     isLittleO_pure, ContinuousLinearMap.zero_apply, sub_self]
 
+@[fun_prop]
+theorem hasFDerivWithinAt_of_subsingleton [h : Subsingleton E] (f : E → F) (s : Set E) (x : E) :
+    HasFDerivWithinAt f (0 : E →L[𝕜] F) s x := by
+  by_cases hs : s = ∅
+  · simp [hs]
+  · obtain ⟨a, rfl⟩ := exists_eq_singleton_iff_nonempty_subsingleton (s := s)|>.mpr
+      ⟨by rwa [nonempty_iff_ne_empty], subsingleton_of_subsingleton⟩
+    exact HasFDerivWithinAt.singleton
+
 @[fun_prop]
 theorem hasFDerivAt_of_subsingleton [h : Subsingleton E] (f : E → F) (x : E) :
     HasFDerivAt f (0 : E →L[𝕜] F) x := by
   rw [← hasFDerivWithinAt_univ, subsingleton_univ.eq_singleton_of_mem (mem_univ x)]
   exact hasFDerivWithinAt_singleton f x
 
-@[fun_prop]
-theorem differentiableOn_empty : DifferentiableOn 𝕜 f ∅ := fun _ => False.elim
+theorem differentiable_of_subsingleton [Subsingleton E] {f : E → F} : Differentiable 𝕜 f :=
+  fun x ↦ (hasFDerivAt_of_subsingleton f x (𝕜 := 𝕜)).differentiableAt
 
 @[fun_prop]
 theorem differentiableOn_singleton : DifferentiableOn 𝕜 f {x} :=