no goals
α : Type u_2
β : Type u_1
E : Type u_3
F : Type ?u.1519544
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f✝ g : α → E
s✝ t : Set α
μ✝ ν : Measure α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
μ : Measure α
s : Set β
⊢ IntegrableOn f s ↔ IntegrableOn (f ∘ e) (e ⁻¹' s)
simp only [IntegrableOn, he.restrict_map, he.integrable_map_iff]