feat: drop an assumption in mfderivWithin_const (#19936)

Followup to #19694

Author: sgouezel

Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

@@ -693,11 +693,18 @@ protected theorem MDifferentiableAt.mfderiv (h : MDifferentiableAt I I' f x) :
 protected theorem HasMFDerivAt.mfderiv (h : HasMFDerivAt I I' f x f') : mfderiv I I' f x = f' :=
   (hasMFDerivAt_unique h h.mdifferentiableAt.hasMFDerivAt).symm
 
-theorem HasMFDerivWithinAt.mfderivWithin (h : HasMFDerivWithinAt I I' f s x f')
+protected theorem HasMFDerivWithinAt.mfderivWithin (h : HasMFDerivWithinAt I I' f s x f')
     (hxs : UniqueMDiffWithinAt I s x) : mfderivWithin I I' f s x = f' := by
   ext
   rw [hxs.eq h h.mdifferentiableWithinAt.hasMFDerivWithinAt]
 
+theorem HasMFDerivWithinAt.mfderivWithin_eq_zero (h : HasMFDerivWithinAt I I' f s x 0) :
+    mfderivWithin I I' f s x = 0 := by
+  simp only [mfld_simps, mfderivWithin, h.mdifferentiableWithinAt, ↓reduceIte]
+  simp only [HasMFDerivWithinAt, mfld_simps] at h
+  rw [fderivWithin, if_pos]
+  exact h.2
+
 theorem MDifferentiable.mfderivWithin (h : MDifferentiableAt I I' f x)
     (hxs : UniqueMDiffWithinAt I s x) : mfderivWithin I I' f s x = mfderiv I I' f x := by
   apply HasMFDerivWithinAt.mfderivWithin _ hxs

Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

@@ -198,9 +198,9 @@ theorem mfderiv_const :
     mfderiv I I' (fun _ : M => c) x = (0 : TangentSpace I x →L[𝕜] TangentSpace I' c) :=
   HasMFDerivAt.mfderiv (hasMFDerivAt_const c x)
 
-theorem mfderivWithin_const (hxs : UniqueMDiffWithinAt I s x) :
+theorem mfderivWithin_const :
     mfderivWithin I I' (fun _ : M => c) s x = (0 : TangentSpace I x →L[𝕜] TangentSpace I' c) :=
-  (hasMFDerivWithinAt_const _ _ _).mfderivWithin hxs
+  (hasMFDerivWithinAt_const _ _ _).mfderivWithin_eq_zero
 
 end Const