∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] {f : α → ε},
  MeasureTheory.HasFiniteIntegral f μ → MeasureTheory.HasFiniteIntegral (fun x => ‖f x‖ₑ) μ