α : Type u_1
α' : Type ?u.4491225
β : Type u_2
β' : Type ?u.4491231
γ : Type ?u.4491234
E : Type ?u.4491237
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
x : α
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ↑↑(map (Prod.mk x) ν) (s ×ˢ t) = ↑↑(dirac x) s * ↑↑ν t
α : Type u_1
α' : Type ?u.4491225
β : Type u_2
β' : Type ?u.4491231
γ : Type ?u.4491234
E : Type ?u.4491237
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
x : α
⊢ Measure.prod (dirac x) ν = map (Prod.mk x) ν
refine' prod_eq fun s t hs ht => _
no goals
α : Type u_1
α' : Type ?u.4491225
β : Type u_2
β' : Type ?u.4491231
γ : Type ?u.4491234
E : Type ?u.4491237
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
x : α
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ↑↑(map (Prod.mk x) ν) (s ×ˢ t) = ↑↑(dirac x) s * ↑↑ν t
simp_rw [map_apply measurable_prod_mk_left (hs.prod ht), mk_preimage_prod_right_eq_if, measure_if,
  dirac_apply' _ hs, ← indicator_mul_left _ _ fun _ => ν t, Pi.one_apply, one_mul]