simp [Function.Injective]
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ Function.Injective fun u => k * u
case hf.h
k : ℝ
hk : 0 < k
s : Set ℝ
hs : MeasurableSet s
⊢ ∀ ⦃a₁ a₂ : ℝ⦄, a₁ = a₂ ∨ k = 0 → a₁ = a₂