no goals
α : Type u_1
β : Type u_2
γ : Type ?u.655475
δ : Type ?u.655478
ι : Type ?u.655481
R : Type ?u.655484
R' : Type ?u.655487
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : IsProbabilityMeasure μ
f : α → β
hf : AEMeasurable f
⊢ ↑↑(Measure.map f μ) univ = 1
simp [map_apply_of_aemeasurable, hf]