case h
α : Type u_2
β : Type u_1
γ : Type ?u.911558
δ : Type ?u.911561
ι : Type ?u.911564
R : Type ?u.911567
R' : Type ?u.911570
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : MeasureTheory.Measure β
t : Set β
ht : MeasurableSet t
⊢ ↑↑(Measure.map f (Measure.comap f μ)) t = ↑↑(Measure.restrict μ (range f)) t
α : Type u_2
β : Type u_1
γ : Type ?u.911558
δ : Type ?u.911561
ι : Type ?u.911564
R : Type ?u.911567
R' : Type ?u.911570
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : MeasureTheory.Measure β
⊢ Measure.map f (Measure.comap f μ) = Measure.restrict μ (range f)
ext1 t ht
no goals
case h
α : Type u_2
β : Type u_1
γ : Type ?u.911558
δ : Type ?u.911561
ι : Type ?u.911564
R : Type ?u.911567
R' : Type ?u.911570
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : MeasureTheory.Measure β
t : Set β
ht : MeasurableSet t
⊢ ↑↑(Measure.map f (Measure.comap f μ)) t = ↑↑(Measure.restrict μ (range f)) t
rw [hf.map_apply, comap_apply f hf.injective hf.measurableSet_image' _ (hf.measurable ht),
  image_preimage_eq_inter_range, Measure.restrict_apply ht]