Theorem: integral_eq_add_Iic_Ioc_Ioi (ForML/Dirac.lean)

State before:
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
Tactic:
simp [← integral_union, hab, Integrable.integrableOn, hf]
State after:
no goals