no goals
α : Type u_1
β : Type u_2
γ : Type ?u.271138
δ : Type ?u.271141
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
f : α → β
hf : MeasurePreserving f
inst✝ : SigmaFinite μb
⊢ SigmaFinite (map f μa)
rwa [hf.map_eq]