no goals
ι : Type ?u.9934822
𝕜 : Type ?u.9934825
E : Type u_1
F : Type ?u.9934831
A : Type ?u.9934834
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : MeasureTheory.Measure ℝ
h : b ≤ a
⊢ (∫ (x : ℝ) in a..b, f x ∂μ) = -∫ (x : ℝ) in Ioc b a, f x ∂μ
simp only [integral_symm b, integral_of_le h]