Mathlib already has the 'implicit derivative from G ∘ T = F' lemma: HasDerivAt.of_comp_left

If you have T with G (T y) = F y (e.g. a monotone transport map T = G⁻¹∘F chosen via IVT), don't hand-roll a slope argument. Mathlib/Analysis/Calculus/Deriv/Inverse.lean has HasDerivAt.of_comp_left (hst : ContinuousAt g a) (hf : HasDerivAt f f' (g a)) (hh : HasDerivAt h h' a) (hf' : f' ≠ 0) (hcomp : f ∘ g =ᶠ[𝓝 a] h) : HasDerivAt g (h' / f') a. It needs no injectivity of g, and the equality only has to hold near a. Usage: HasDerivAt.of_comp_left hT.continuousAt hG hF hg0 (Filter.Eventually.of_forall hGT). Lesson: before claiming a lemma is missing, grep the file where it would naturally live (here Deriv/Inverse.lean, next to of_local_left_inverse).