no goals
ι : Type u_2
𝕜 : Type ?u.504617
E : Type u_1
F : Type ?u.504623
A : Type ?u.504626
inst✝⁴ : NormedAddCommGroup E
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
c ca cb : E
l l' la la' lb lb' : Filter ℝ
lt : Filter ι
μ : MeasureTheory.Measure ℝ
u v ua va ub vb : ι → ℝ
inst✝¹ : IsMeasurablyGenerated l'
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l'
hf : Tendsto f (l' ⊓ Measure.ae μ) (𝓝 c)
hl : Measure.FiniteAtFilter μ l'
hu : Tendsto u lt l
hv : Tendsto v lt l
huv : v ≤ᶠ[lt] u
t : ι
⊢ -((∫ (x : ℝ) in v t..u t, f x ∂μ) - ENNReal.toReal (↑↑μ (Ioc (v t) (u t))) • c) =
    (∫ (x : ℝ) in u t..v t, f x ∂μ) + ENNReal.toReal (↑↑μ (Ioc (v t) (u t))) • c
simp [integral_symm (u t), add_comm]