Merge master into nightly-testing

leanprover-community · Dec 17, 2023 · 922483d · 922483d
2 parents c557306 + b835302
commit 922483d
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/Mathlib/Geometry/Manifold/MFDeriv.lean b/Mathlib/Geometry/Manifold/MFDeriv.lean
@@ -821,6 +821,13 @@ theorem MDifferentiable.prod_mk_space {f : M → E'} {g : M → E''} (hf : MDiff
 
 /-! ### Congruence lemmas for derivatives on manifolds -/
 
+theorem HasMFDerivAt.congr_mfderiv (h : HasMFDerivAt I I' f x f') (h' : f' = f₁') :
+    HasMFDerivAt I I' f x f₁' :=
+  h' ▸ h
+
+theorem HasMFDerivWithinAt.congr_mfderiv (h : HasMFDerivWithinAt I I' f s x f') (h' : f' = f₁') :
+    HasMFDerivWithinAt I I' f s x f₁' :=
+  h' ▸ h
 
 theorem HasMFDerivWithinAt.congr_of_eventuallyEq (h : HasMFDerivWithinAt I I' f s x f')
     (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : HasMFDerivWithinAt I I' f₁ s x f' := by