MeasureTheory.distribution_smul_left

lemma distribution_smul_left {f : α → ε'} {c : ℝ≥0} (hc : c ≠ 0) :    distribution (c • f) t μ = distribution f (t / ‖c‖ₑ) μ := by  have h₀ : ‖c‖ₑ ≠ 0 := by    have : ‖c‖ₑ = ‖(c : ℝ≥0∞)‖ₑ := rfl    rw [this, enorm_ne_zero]    exact ENNReal.coe_ne_zero.mpr hc  unfold distribution  congr with x  simp only [Pi.smul_apply]  rw [← @ENNReal.mul_lt_mul_iff_left (t / ‖c‖ₑ) _ (‖c‖ₑ) h₀ coe_ne_top,    enorm_smul_eq_mul (c := c) _, ENNReal.div_mul_cancel h₀ coe_ne_top, mul_comm]