simp [← integral_union, hab, Integrable.integrableOn, hf]
f : ℝ → ℝ
hf : Integrable f
a b : ℝ
hab : a ≤ b
⊢ ∫ (x : ℝ), f x = ((∫ (x : ℝ) in Set.Iic a, f x) + ∫ (x : ℝ) in Set.Ioc a b, f x) + ∫ (x : ℝ) in Set.Ioi b, f x
no goals