no goals
α : Type u_1
β : Type ?u.1634475
E : Type u_2
F : Type ?u.1634481
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hs : MeasurableSet s
⊢ Integrable (indicator s f) ↔ IntegrableOn f s
simp [IntegrableOn, Integrable, HasFiniteIntegral, nnnorm_indicator_eq_indicator_nnnorm,
  ENNReal.coe_indicator, lintegral_indicator _ hs, aestronglyMeasurable_indicator_iff hs]