α : Type u_1
α' : Type ?u.4456049
β : Type u_2
β' : Type ?u.4456055
γ : Type ?u.4456058
E : Type ?u.4456061
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
⊢ ∀ (s : Set β) (t : Set α),
    MeasurableSet s → MeasurableSet t → ↑↑(map Prod.swap (Measure.prod μ ν)) (s ×ˢ t) = ↑↑ν s * ↑↑μ t
α : Type u_1
α' : Type ?u.4456049
β : Type u_2
β' : Type ?u.4456055
γ : Type ?u.4456058
E : Type ?u.4456061
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
⊢ map Prod.swap (Measure.prod μ ν) = Measure.prod ν μ
refine' (prod_eq _).symm
α : Type u_1
α' : Type ?u.4456049
β : Type u_2
β' : Type ?u.4456055
γ : Type ?u.4456058
E : Type ?u.4456061
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set β
t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ↑↑(map Prod.swap (Measure.prod μ ν)) (s ×ˢ t) = ↑↑ν s * ↑↑μ t
α : Type u_1
α' : Type ?u.4456049
β : Type u_2
β' : Type ?u.4456055
γ : Type ?u.4456058
E : Type ?u.4456061
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
⊢ ∀ (s : Set β) (t : Set α),
    MeasurableSet s → MeasurableSet t → ↑↑(map Prod.swap (Measure.prod μ ν)) (s ×ˢ t) = ↑↑ν s * ↑↑μ t
intro s t hs ht
no goals
α : Type u_1
α' : Type ?u.4456049
β : Type u_2
β' : Type ?u.4456055
γ : Type ?u.4456058
E : Type ?u.4456061
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set β
t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ↑↑(map Prod.swap (Measure.prod μ ν)) (s ×ˢ t) = ↑↑ν s * ↑↑μ t
simp_rw [map_apply measurable_swap (hs.prod ht), preimage_swap_prod, prod_prod, mul_comm]