no goals
α : Type u_1
β : Type ?u.1870561
γ : Type ?u.1870564
δ : Type ?u.1870567
ι : Type ?u.1870570
R : Type ?u.1870573
R' : Type ?u.1870576
inst✝ : MeasureSpace α
s t : Set α
hs : NullMeasurableSet s
ht : MeasurableSet t
⊢ ↑↑volume (Subtype.val ⁻¹' t) = ↑↑volume (t ∩ s)
rw [volume_set_coe_def,
  comap_apply₀ _ _ Subtype.coe_injective
    (fun h => MeasurableSet.nullMeasurableSet_subtype_coe hs)
    (measurable_subtype_coe ht).nullMeasurableSet,
  image_preimage_eq_inter_range, Subtype.range_coe]