. intro x _
  simp [mul_comm k]
  exact HasDerivAt.hasDerivWithinAt (hasDerivAt_mul_const k)
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
⊢ Set.InjOn (fun u => k * u) s

k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)
case hf
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Set.InjOn (fun u => k * u) s

k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)