f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y => Real.log (f y)) (f' / f x) Set.univ x
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0
⊢ HasDerivAt (fun y => Real.log (f y)) (f' / f x) x
rw [← hasDerivWithinAt_univ] at *
no goals
f : ℝ → ℝ
x f' : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y => Real.log (f y)) (f' / f x) Set.univ x
exact hf.log hx