simp
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi (-0), f x = ∫ (x : ℝ) in Set.Ioi 0, f (-x)
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Ioi 0, f (-x)