feat: tangentMap(Within)_snd (leanprover-community#34369)

From fpvandoorn and my LeanCourse25.

Author: grunweg

Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

@@ -835,10 +835,17 @@ theorem tangentMapWithin_proj {p : TangentBundle I M} :
     (tangentMapWithin I I' f s p).proj = f p.proj :=
   rfl
 
+@[simp, mfld_simps]
+lemma tangentMapWithin_snd {X : TangentSpace I x} :
+    (tangentMapWithin I I' f s X).2 = (mfderivWithin I I' f s x) X := rfl
+
 @[simp, mfld_simps]
 theorem tangentMap_proj {p : TangentBundle I M} : (tangentMap I I' f p).proj = f p.proj :=
   rfl
 
+@[simp, mfld_simps]
+lemma tangentMap_snd {X : TangentSpace I x} : (tangentMap I I' f X).2 = (mfderiv I I' f x) X := rfl
+
 /-- If two sets coincide locally around `x`, except maybe at a point `y`, then their
 preimage under `extChartAt x` coincide locally, except maybe at `extChartAt I x x`. -/
 theorem preimage_extChartAt_eventuallyEq_compl_singleton (y : M) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :