no goals
ι : Type ?u.15374404
𝕜 : Type ?u.15374407
E : Type u_1
F : Type ?u.15374413
A : Type ?u.15374416
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
⊢ ((∫ (x : ℝ) in a..b, f x ∂μ) + ∫ (x : ℝ) in b..c, f x ∂μ) = ∫ (x : ℝ) in a..c, f x ∂μ
rw [← add_neg_eq_zero, ← integral_symm, integral_add_adjacent_intervals_cancel hab hbc]