f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun y => Real.log (f y)) ((f x)⁻¹ * f') x
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun y => Real.log (f y)) (f' / f x) x
rw [div_eq_inv_mul]
no goals
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun y => Real.log (f y)) ((f x)⁻¹ * f') x
exact (hasStrictDerivAt_log hx).comp x hf