no goals
α : Type u_2
β✝ : Type ?u.252454
γ : Type ?u.252457
δ : Type ?u.252460
ι : Type ?u.252463
R : Type ?u.252466
R' : Type ?u.252469
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
s : Set β
hf : Injective f
hf' : Measurable f
h : ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t)
hs : MeasurableSet s
⊢ ↑↑(comap f μ) (f ⁻¹' s) = ↑↑μ (s ∩ range f)
rw [comap_apply₀ _ _ hf h (hf' hs).nullMeasurableSet, image_preimage_eq_inter_range]