case e_μ
α : Type u_2
β : Type u_1
γ : Type ?u.1148988
δ : Type ?u.1148991
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : AEMeasurable f
hg : AEMeasurable g
⊢ Measure.map g μ = Measure.map (AEMeasurable.mk g hg) μ
α : Type u_2
β : Type u_1
γ : Type ?u.1148988
δ : Type ?u.1148991
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : AEMeasurable f
hg : AEMeasurable g
⊢ (∫⁻ (a : β), AEMeasurable.mk f hf a ∂Measure.map g μ) =
    ∫⁻ (a : β), AEMeasurable.mk f hf a ∂Measure.map (AEMeasurable.mk g hg) μ
congr 1
no goals
case e_μ
α : Type u_2
β : Type u_1
γ : Type ?u.1148988
δ : Type ?u.1148991
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
hf : AEMeasurable f
hg : AEMeasurable g
⊢ Measure.map g μ = Measure.map (AEMeasurable.mk g hg) μ
exact Measure.map_congr hg.ae_eq_mk