feat(analysis/calculus/deriv): add `has_deriv_at.tendsto_punctured_nh…

…ds` (#10877)

src/analysis/calculus/deriv.lean

@@ -1728,6 +1728,11 @@ lemma has_deriv_at.eventually_ne (h : has_deriv_at f f' x) (hf' : f' ≠ 0) :
 (has_deriv_at_iff_has_fderiv_at.1 h).eventually_ne
   ⟨∥f'∥⁻¹, λ z, by field_simp [norm_smul, mt norm_eq_zero.1 hf']⟩
 
+lemma has_deriv_at.tendsto_punctured_nhds (h : has_deriv_at f f' x) (hf' : f' ≠ 0) :
+  tendsto f (𝓝[≠] x) (𝓝[≠] (f x)) :=
+tendsto_nhds_within_of_tendsto_nhds_of_eventually_within _
+  h.continuous_at.continuous_within_at (h.eventually_ne hf')
+
 theorem not_differentiable_within_at_of_local_left_inverse_has_deriv_within_at_zero
   {f g : 𝕜 → 𝕜} {a : 𝕜} {s t : set 𝕜} (ha : a ∈ s) (hsu : unique_diff_within_at 𝕜 s a)
   (hf : has_deriv_within_at f 0 t (g a)) (hst : maps_to g s t) (hfg : f ∘ g =ᶠ[𝓝[s] a] id) :

src/analysis/special_functions/trigonometric/complex_deriv.lean

@@ -39,9 +39,7 @@ begin
   simp only [tan_eq_sin_div_cos, ← norm_eq_abs, normed_field.norm_div],
   have A : sin x ≠ 0 := λ h, by simpa [*, sq] using sin_sq_add_cos_sq x,
   have B : tendsto cos (𝓝[≠] (x)) (𝓝[≠] 0),
-  { refine tendsto_inf.2 ⟨tendsto.mono_left _ inf_le_left, tendsto_principal.2 _⟩,
-    exacts [continuous_cos.tendsto' x 0 hx,
-      hx ▸ (has_deriv_at_cos _).eventually_ne (neg_ne_zero.2 A)] },
+    from hx ▸ (has_deriv_at_cos x).tendsto_punctured_nhds (neg_ne_zero.2 A),
   exact continuous_sin.continuous_within_at.norm.mul_at_top (norm_pos_iff.2 A)
     (tendsto_norm_nhds_within_zero.comp B).inv_tendsto_zero,
 end