case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ ↑↑(join (map (map f) μ)) s = ↑↑(map f (join μ)) s
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
⊢ join (map (map f) μ) = map f (join μ)
ext1 s hs
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ (∫⁻ (a : Measure α), ↑↑(map f a) s ∂μ) = ∫⁻ (μ : Measure α), ↑↑μ (f ⁻¹' s) ∂μ
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ ↑↑(join (map (map f) μ)) s = ↑↑(map f (join μ)) s
rw [join_apply hs, map_apply hf hs, join_apply (hf hs),
  lintegral_map (measurable_coe hs) (measurable_map f hf)]
no goals
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ (∫⁻ (a : Measure α), ↑↑(map f a) s ∂μ) = ∫⁻ (μ : Measure α), ↑↑μ (f ⁻¹' s) ∂μ
simp_rw [map_apply hf hs]