α : Type u_1
α' : Type ?u.5352062
β : Type u_2
β' : Type ?u.5352068
γ : Type ?u.5352071
E : Type ?u.5352074
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
f : α × β → ℝ≥0∞
hf : AEMeasurable f
⊢ (∫⁻ (z : β × α), f (Prod.swap z) ∂Measure.prod ν μ) = ∫⁻ (z : α × β), f z ∂Measure.prod μ ν
α : Type u_1
α' : Type ?u.5352062
β : Type u_2
β' : Type ?u.5352068
γ : Type ?u.5352071
E : Type ?u.5352074
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
f : α × β → ℝ≥0∞
hf : AEMeasurable f
⊢ (∫⁻ (z : β × α), f (Prod.swap z) ∂Measure.prod ν μ) = ∫⁻ (z : α × β), f z ∂Measure.prod μ ν
rw [← prod_swap] at hf
no goals
α : Type u_1
α' : Type ?u.5352062
β : Type u_2
β' : Type ?u.5352068
γ : Type ?u.5352071
E : Type ?u.5352074
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
f : α × β → ℝ≥0∞
hf : AEMeasurable f
⊢ (∫⁻ (z : β × α), f (Prod.swap z) ∂Measure.prod ν μ) = ∫⁻ (z : α × β), f z ∂Measure.prod μ ν
rw [← lintegral_map' hf measurable_swap.aemeasurable, prod_swap]