intro x _
case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∀ x ∈ s, HasDerivWithinAt (fun u => k * u) k s x
case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
x : ℝ
a✝ : x ∈ s
⊢ HasDerivWithinAt (fun u => k * u) k s x