no goals
α : Type u_1
E : Type ?u.5974976
F : Type u_2
G : Type ?u.5974982
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
𝕜 : Type u_3
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : MulActionWithZero 𝕜 E
inst✝² : Module 𝕜 F
inst✝¹ : BoundedSMul 𝕜 E
inst✝ : BoundedSMul 𝕜 F
c : 𝕜
f : α → F
⊢ snormEssSup (c • f) μ = ↑‖c‖₊ * snormEssSup f μ
simp_rw [snormEssSup, Pi.smul_apply, nnnorm_smul, ENNReal.coe_mul, ENNReal.essSup_const_mul]