ext x
case e_f
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ (fun x => f x) = fun x => f (-x)
case e_f.h
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
x : ℝ
⊢ f x = f (-x)