MeasureTheory.eLorentzNorm'_indicator_const'

lemma eLorentzNorm'_indicator_const' {a : ε} {s : Set α} (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤)  (q_ne_zero : q ≠ 0) (q_ne_top : q ≠ ⊤) :    eLorentzNorm' (s.indicator (Function.const α a)) p q μ      = (p / q) ^ q.toReal⁻¹ * μ s ^ p.toReal⁻¹ * ‖a‖ₑ := by  rw [eLorentzNorm'_eq p_ne_zero p_ne_top]  simp_rw [rearrangement_indicator_const]  rw [eLpNorm_eq_lintegral_rpow_enorm_toReal q_ne_zero q_ne_top]  simp only [ENNReal.toReal_inv, enorm_eq_self, one_div]  conv in (_ * _) ^ _ => rw [ENNReal.mul_rpow_of_nonneg _ _ ENNReal.toReal_nonneg,    Set.comp_indicator (fun t ↦ t ^ q.toReal),    ENNReal.zero_rpow_of_pos (ENNReal.toReal_pos q_ne_zero q_ne_top),    Function.comp_const, Function.const_zero, Set.piecewise_eq_indicator,    ← Set.indicator_mul_right _ (fun t ↦ (t ^ p.toReal⁻¹) ^ q.toReal) _,    ← Set.indicator_comp_right]  rw [lintegral_indicator (by measurability)]  simp only [Function.const_apply, Function.comp_apply]  rw [lintegral_mul_const _ (by fun_prop),    ENNReal.mul_rpow_of_nonneg _ _ (by simp),    ENNReal.rpow_rpow_inv (ENNReal.toReal_ne_zero.mpr ⟨q_ne_zero, q_ne_top⟩)]  congr  rw [setLIntegral_withDensity_eq_lintegral_mul₀ (by fun_prop) (by fun_prop) (by measurability)]  simp only [Pi.mul_apply]  simp_rw [← ENNReal.rpow_neg_one, ← ENNReal.rpow_mul]  rw [← lintegral_indicator (by measurability), lintegral_nnreal_eq_lintegral_toNNReal_Ioi]  simp_rw [← Set.indicator_comp_right]  rw [setLIntegral_indicator (by measurability)]  have : ENNReal.ofNNReal ∘ Real.toNNReal = ENNReal.ofReal := rfl  rw [← Set.preimage_comp, this]  simp only [Function.comp_apply]  have : ((μ s ^ p.toReal⁻¹) ^ q.toReal) ^ q.toReal⁻¹ = μ s ^ p.toReal⁻¹:= by    apply ENNReal.rpow_rpow_inv (ENNReal.toReal_ne_zero.mpr ⟨q_ne_zero, q_ne_top⟩)  rw [← this, ← ENNReal.mul_rpow_of_nonneg _ _ (by simp), ← ENNReal.rpow_mul]  congr  calc _    _ = ∫⁻ (a : ℝ) in ENNReal.ofReal ⁻¹' Set.Iio (μ s) ∩ Set.Ioi 0,          ENNReal.ofReal (a ^ (p.toReal⁻¹ * q.toReal - 1)) := by      apply setLIntegral_congr_fun (by measurability)      intro x hx      simp only      rw [← ENNReal.rpow_add _ _        (by simp only [ne_eq, ENNReal.coe_eq_zero, Real.toNNReal_eq_zero, not_le]; exact hx.2)        (by simp)]      ring_nf      rw [← ENNReal.ofReal_rpow_of_pos hx.2]      congr  rw [ENNReal.ofReal_Iio_eq]  have hpq : 0 < p.toReal⁻¹ * q.toReal := by    apply mul_pos    · rw [inv_pos]      exact ENNReal.toReal_pos p_ne_zero p_ne_top    · exact ENNReal.toReal_pos q_ne_zero q_ne_top  split_ifs with h h  · simp only [Set.empty_inter, Measure.restrict_empty, lintegral_zero_measure, zero_eq_mul,    ENNReal.div_eq_zero_iff, ENNReal.rpow_eq_zero_iff]    right    left    use h, hpq  · rw [Set.univ_inter]    rw [lintegral_rpow_Ioi_top]    rw [h, ENNReal.top_rpow_of_pos hpq, ENNReal.mul_top]    simp only [ne_eq, ENNReal.div_eq_zero_iff, not_or]    use p_ne_zero, q_ne_top  · rw [Set.Iio_inter_Ioi, lintegral_rpow_of_gt ENNReal.toReal_nonneg (by simpa)]    simp only [sub_add_cancel]    rw [ENNReal.ofReal_div_of_pos hpq, ENNReal.ofReal_mul (by simp),        ENNReal.ofReal_inv_of_pos (ENNReal.toReal_pos p_ne_zero p_ne_top),        ENNReal.ofReal_toReal p_ne_top, ENNReal.ofReal_toReal q_ne_top, ← ENNReal.div_eq_inv_mul,        ← ENNReal.div_mul _ (by left; assumption) (by left; assumption), ENNReal.mul_comm_div,        mul_comm, ← ENNReal.ofReal_rpow_of_nonneg ENNReal.toReal_nonneg (by positivity),        ENNReal.ofReal_toReal h]