Lean: use Continuous.tendsto' when the limit point is not syntactically f x

(continuous_exp.comp continuous_neg).tendsto 0 gives Tendsto (rexp ∘ fun a => -a) _ (𝓝 ((rexp ∘ fun a => -a) 0)). Neither exact nor simpa closes a goal stated with 𝓝 1, and convert leaves both the function goal and an awkward point goal, where simp makes no progress on the composition. Use (hf.tendsto' 0 1 (by simp)).mono_left nhdsWithin_le_nhds. Continuous.tendsto' (hf) x y (h : f x = y) fixes the limit point up front, and the composed function is accepted by defeq.