no goals
α : Type ?u.49835
inst✝² : TopologicalSpace α
E : Type ?u.49841
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → ℂ
s : Set ℝ
x : ℝ
f' : ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivWithinAt (fun t => log (f t)) (f' / f x) s x
simpa only [div_eq_inv_mul] using
  (hasStrictFDerivAt_log_real h₂).hasFDerivAt.comp_hasDerivWithinAt x h₁