no goals
α : Type u_1
α' : Type ?u.5370740
β : Type u_2
β' : Type ?u.5370746
γ : Type ?u.5370749
E : Type ?u.5370752
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
ρ : Measure (α × β)
s : Set α
hs : MeasurableSet s
⊢ ↑↑(fst ρ) s = ↑↑ρ (Prod.fst ⁻¹' s)
rw [fst, Measure.map_apply measurable_fst hs]