enorm_integral_norm_eq_integral_enorm

lemma enorm_integral_norm_eq_integral_enorm {α 𝕜 : Type*} [MeasurableSpace α] [RCLike 𝕜]    {μ : Measure α} {f : α → 𝕜} (hf : Integrable f μ) : ‖∫ x, ‖f x‖ ∂μ‖ₑ = ∫⁻ x, ‖f x‖ₑ ∂μ := by  simp_rw [enorm_eq_nnnorm]  rw [lintegral_coe_eq_integral]  · simp only [coe_nnnorm, ENNReal.ofReal, ENNReal.coe_inj]    have : |∫ (a : α), ‖f a‖ ∂μ| = ∫ (a : α), ‖f a‖ ∂μ :=      abs_eq_self.2 (integral_nonneg (fun _ ↦ by positivity))    aesop  · simpa only [coe_nnnorm] using hf.norm