theorem MeasureTheory.IntegrableAtFilter.congr'_enorm {α : Type u_1} {ε : Type u_3} {ε' : Type u_4} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace ε] [TopologicalSpace ε'] [ContinuousENorm ε] [ContinuousENorm ε'] {l : Filter α} {f : α → ε} {g : α → ε'} (hf : IntegrableAtFilter f l μ) (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ) : IntegrableAtFilter g l μ