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