f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivWithinAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) Set.univ x
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) x
rw [← hasDerivWithinAt_univ] at *
no goals
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' Set.univ x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivWithinAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) Set.univ x
exact hf.rpow_const hx