no goals
ι : Type ?u.1680719
𝕜 : Type ?u.1680722
E : Type u_1
F : Type ?u.1680728
A : Type ?u.1680731
inst✝⁴ : NormedAddCommGroup E
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c ca cb : E
l l' la la' lb lb' : Filter ℝ
lt : Filter ι
a b z : ℝ
u v ua ub va vb : ι → ℝ
inst✝¹ : FTCFilter a la la'
inst✝ : FTCFilter b lb lb'
hf : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter f (𝓝 a)
ha : Tendsto f (𝓝 a ⊓ Measure.ae volume) (𝓝 c)
⊢ HasStrictDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-c) a
simpa only [← integral_symm] using
  (integral_hasStrictDerivAt_of_tendsto_ae_right hf.symm hmeas ha).neg