no goals
ι : Type ?u.16082722
𝕜 : Type ?u.16082725
E : Type u_1
F : Type ?u.16082731
A : Type ?u.16082734
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b c d : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
hab : IntervalIntegrable f μ a b
hcd : IntervalIntegrable f μ c d
hac : IntervalIntegrable f μ a c
⊢ ((∫ (x : ℝ) in a..b, f x ∂μ) - ∫ (x : ℝ) in c..d, f x ∂μ) = (∫ (x : ℝ) in d..b, f x ∂μ) - ∫ (x : ℝ) in c..a, f x ∂μ
rw [integral_interval_sub_interval_comm hab hcd hac, integral_symm b d, integral_symm a c,
  sub_neg_eq_add, sub_eq_neg_add]