no goals
α : Type u_1
E : Type ?u.5056591
F : Type u_2
G : Type u_3
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
⊢ essSup (fun x => ↑(c * ‖g x‖₊)) μ = essSup (fun x => ↑c * ↑‖g x‖₊) μ
simp_rw [ENNReal.coe_mul]