MeasureTheory.wnorm_const_smul_le

lemma wnorm_const_smul_le (hp : p ≠ 0) {f : α → ε'} (k : ℝ≥0) :    wnorm (k • f) p μ ≤ ‖k‖ₑ * wnorm f p μ := by  by_cases ptop : p = ⊤  · simp only [ptop, wnorm_top]    apply eLpNormEssSup_const_nnreal_smul_le  simp only [wnorm, ptop, ↓reduceIte, wnorm', iSup_le_iff]  by_cases k_zero : k = 0  · simp [distribution, k_zero, toReal_pos hp ptop]  simp only [distribution_smul_left k_zero]  intro t  rw [ENNReal.mul_iSup]  have : t * distribution f (t / ‖k‖ₑ) μ ^ p.toReal⁻¹ =      ‖k‖ₑ * ((t / ‖k‖ₑ) * distribution f (t / ‖k‖ₑ) μ ^ p.toReal⁻¹) := by    nth_rewrite 1 [← mul_div_cancel₀ t k_zero]    simp only [coe_mul, mul_assoc]    congr    exact coe_div k_zero  rw [this]  apply le_iSup_of_le (↑t / ↑‖k‖₊)  apply le_of_eq  congr <;> exact (coe_div k_zero).symm