no goals
α : Type u_1
β : Type u_2
γ : Type ?u.212187
δ : Type ?u.212190
ι : Type ?u.212193
R : Type ?u.212196
R' : Type ?u.212199
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
f : α → β
hf : AEMeasurable f
s : Set β
hs : MeasurableSet s
⊢ ↑↑(map f μ) s = ↑↑μ (f ⁻¹' s)
simpa only [mapₗ, hf.measurable_mk, hs, dif_pos, liftLinear_apply, OuterMeasure.map_apply,
  ← mapₗ_mk_apply_of_aemeasurable hf] using
  measure_congr (hf.ae_eq_mk.symm.preimage s)