. apply Function.Injective.injOn
  simp [Function.Injective]
  intro u v
  intro h
  cases h with
  | inl h => exact h
  | inr h => exfalso; exact hk.ne' h
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)
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∫ (x : ℝ) in s, DiracSeq k x = ∫ (x : ℝ) in s, |k| • DiracSeq 1 (k * x)