no goals
α : Type u_2
E : Type u_1
F : Type ?u.687847
G : Type ?u.687850
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * ENNReal.toReal (↑↑μ s) ^ (1 / ENNReal.toReal p)
rw [Lp.norm_def, snorm_congr_ae indicatorConstLp_coeFn,
  snorm_indicator_const hs hp_ne_zero hp_ne_top, ENNReal.toReal_mul, ENNReal.toReal_rpow,
  ENNReal.coe_toReal, coe_nnnorm]