no goals
α : Type u_1
α' : Type ?u.4493213
β : Type u_2
β' : Type ?u.4493219
γ : Type ?u.4493222
E : Type ?u.4493225
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
x : α
y : β
⊢ Measure.prod (dirac x) (dirac y) = dirac (x, y)
rw [prod_dirac, map_dirac measurable_prod_mk_right]