intervalIntegrable_local_quotient_of_differentiableAt

theorem intervalIntegrable_local_quotient_of_differentiableAt    {f : ℝ → E} {x R : ℝ} (hR : 0 < R)    (hf_cont : ContinuousOn f (Set.Icc (x - R) (x + R)))    (hf_diff : DifferentiableAt ℝ f x) :    IntervalIntegrable      (fun u : ℝ =>        if u = 0 then 0 else (1 / (π * u) : ℂ) • (f (x - u) - f x))      volume (-R) R := by  let qds : ℝ → E := fun u => (-1 / π : ℂ) • dslope f x (x - u)  have hmem : Set.Icc (x - R) (x + R) ∈ nhds x := by    exact Icc_mem_nhds (by linarith) (by linarith)  have hds : ContinuousOn (dslope f x) (Set.Icc (x - R) (x + R)) :=    (continuousOn_dslope hmem).2 ⟨hf_cont, hf_diff⟩  have hmap : MapsTo (fun u : ℝ => x - u) (Set.Icc (-R) R) (Set.Icc (x - R) (x + R)) := by    intro u hu    rw [Set.mem_Icc] at hu ⊢    constructor <;> linarith  have hcomp : ContinuousOn (fun u : ℝ => dslope f x (x - u)) (Set.Icc (-R) R) := by    exact hds.comp (by fun_prop) hmap  have hqds_cont : ContinuousOn qds (Set.Icc (-R) R) :=    hcomp.const_smul (-1 / π : ℂ)  have hle : -R ≤ R := by linarith  have hqds_int : IntervalIntegrable qds volume (-R) R :=    ContinuousOn.intervalIntegrable_of_Icc hle hqds_cont  refine hqds_int.congr_ae ?_  rw [Filter.EventuallyEq]  rw [ae_restrict_iff' measurableSet_uIoc]  filter_upwards [show ∀ᵐ u : ℝ, u ≠ 0 by simp [ae_iff, measure_singleton]]    with u hu _hu_mem  dsimp [qds]  exact local_quotient_eq_dslope (E := E) f x hu