simp [mul_comm k]
case hf'
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
x : ℝ
a✝ : 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 => u * k) k s x