no goals
α : Type u_1
E : Type u_2
F : Type ?u.689528
G : Type ?u.689531
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
hμs_ne_zero : ↑↑μ s ≠ 0
⊢ ‖indicatorConstLp ⊤ hs hμs c‖ = ‖c‖
rw [Lp.norm_def, snorm_congr_ae indicatorConstLp_coeFn,
  snorm_indicator_const' hs hμs_ne_zero ENNReal.top_ne_zero, ENNReal.top_toReal, _root_.div_zero,
  ENNReal.rpow_zero, mul_one, ENNReal.coe_toReal, coe_nnnorm]