no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1014989
δ : Type ?u.1014992
ι : Type ?u.1014995
R : Type ?u.1014998
R' : Type ?u.1015001
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : MeasureTheory.Measure β
s : Set α
⊢ ↑↑(Measure.comap f μ) s = ↑↑(Measure.comap f μ) (f ⁻¹' (f '' s))
rw [hf.injective.preimage_image]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1014989
δ : Type ?u.1014992
ι : Type ?u.1014995
R : Type ?u.1014998
R' : Type ?u.1015001
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : MeasureTheory.Measure β
s : Set α
⊢ ↑↑(Measure.map f (Measure.comap f μ)) (f '' s) = ↑↑μ (f '' s)
rw [hf.map_comap, restrict_apply' hf.measurableSet_range,
  inter_eq_self_of_subset_left (image_subset_range _ _)]