no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.54421
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
g : β → γ
f : α → β
hg : MeasurePreserving g
hf : MeasurePreserving f
⊢ map (g ∘ f) μa = μc
rw [← map_map hg.1 hf.1, hf.2, hg.2]