E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ (x : ℝ), x ∈ Ici a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ici a
⊢ ContinuousWithinAt f (Ici a) x
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ (x : ℝ), x ∈ Ici a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
⊢ (∫ (x : ℝ) in Ioi a, f' x) = m - f a
refine integral_Ioi_of_hasDerivAt_of_tendsto (fun x hx ↦ ?_) (fun x hx => hderiv x hx.out.le)
  f'int hf
no goals
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ (x : ℝ), x ∈ Ici a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ici a
⊢ ContinuousWithinAt f (Ici a) x
exact (hderiv x hx).continuousAt.continuousWithinAt