MeasureTheory.wnorm_const_smul_le'

lemma wnorm_const_smul_le' [IsBoundedSMul 𝕜 E] (hp : p ≠ 0) {f : α → E} (k : 𝕜) :    wnorm (k • f) p μ ≤ ‖k‖ₑ * wnorm f p μ := by  by_cases ptop : p = ⊤  · simp only [ptop, wnorm_top]    apply eLpNormEssSup_const_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 knorm_ne_zero : ‖k‖₊ ≠ 0 := nnnorm_ne_zero_iff.mpr k_zero  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 knorm_ne_zero]    simp only [coe_mul, mul_assoc]    congr    exact coe_div knorm_ne_zero  erw [this]  apply le_iSup_of_le (↑t / ↑‖k‖₊)  apply le_of_eq  congr <;> exact (coe_div knorm_ne_zero).symm