no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.214987
ι : Type ?u.214990
R : Type ?u.214993
R' : Type ?u.214996
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
g : β → γ
f : α → β
hg : Measurable g
hf : Measurable f
s : Set γ
hs : MeasurableSet s
⊢ ↑↑(map g (map f μ)) s = ↑↑(map (g ∘ f) μ) s
simp [hf, hg, hs, hg hs, hg.comp hf, ← preimage_comp]