no goals
α : Type u_1
β : Type ?u.3764222
E : Type u_2
F : Type ?u.3764228
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : MeasureTheory.Measure α
a b : α
hb : ↑↑μ {b} ≠ ⊤
⊢ IntegrableOn f (Iic b) ↔ IntegrableOn f (Iio b)
rw [← Iio_union_right, integrableOn_union,
  eq_true (integrableOn_singleton_iff.mpr <| Or.inr hb.lt_top), and_true_iff]