rw [← integral_add_compl hs hf]
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ), f x
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Ioi 0, f x ∂volume + ∫ (x : ℝ) in (Set.Ioi 0)ᶜ, f x ∂volume