no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.379755
δ' : Type ?u.379758
ι : Sort uι
s✝ t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (g ∘ f '' s)
rwa [image_comp, hg.measurableSet_image, hf.measurableSet_image]