rw [@integral_image_eq_integral_abs_deriv_smul _ _ _ _ _ (fun _ => k : ℝ → ℝ) hs]
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in (fun u => k * u) '' s, DiracSeq 1 x
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
⊢ ∀ 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