no goals
α : Type u_2
β : Type ?u.279314
E : Type u_1
F : Type ?u.279320
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : PartialOrder α
a b : α
inst✝ : NoAtoms μ
⊢ (∫ (t : α) in Icc a b, f t ∂μ) = ∫ (t : α) in Ico a b, f t ∂μ
rw [integral_Icc_eq_integral_Ico, integral_Ico_eq_integral_Ioo]