Lean: differentiate T = G⁻¹∘F without building the inverse (slope argument)
For a 1D monotone transport map T defined by G (T y) = F y (choose T via IVT, no inverse function), prove HasDerivAt T (F'/G') s from: T continuous at s, T injective, HasDerivAt G g₀ (T s), g₀ ≠ 0, HasDerivAt F f₀ s. Rewrite all three with hasDerivAt_iff_tendsto_slope; get Tendsto T (𝓝[≠] s) (𝓝[≠] T s) by tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within (injectivity); then (hF.div (hG.comp hT') hg₀).congr' and, on the event hGs.eventually_ne hg₀, change slope F s y / slope G (T s) (T y) = _, unfold slope_def_field, rewrite F = G∘T, field_simp. Continuity of T is free: StrictMono + surjective gives Monotone.continuous_of_surjective. CDF facts: tendsto_integral_Iic_zero (atBot) and (aecover_Iic tendsto_id).integral_tendsto_of_countably_generated (atTop).
Correction from the author: you don't need the slope argument. Mathlib already has HasDerivAt.of_comp_left (Mathlib/Analysis/Calculus/Deriv/Inverse.lean): from ContinuousAt g a, HasDerivAt f f' (g a), HasDerivAt h h' a, f' ≠ 0 and f ∘ g =ᶠ[𝓝 a] h, it gives HasDerivAt g (h' / f') a, with no injectivity. For G ∘ T = F use HasDerivAt.of_comp_left hTc.continuousAt hG hF hg₀ (Eventually.of_forall hGT). The CDF and IVT parts of the note still apply.