α : Type u_1
α' : Type ?u.4489185
β : Type u_2
β' : Type ?u.4489191
γ : Type ?u.4489194
E : Type ?u.4489197
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
y : β
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ↑↑(map (fun x => (x, y)) μ) (s ×ˢ t) = ↑↑μ s * ↑↑(dirac y) t
α : Type u_1
α' : Type ?u.4489185
β : Type u_2
β' : Type ?u.4489191
γ : Type ?u.4489194
E : Type ?u.4489197
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
y : β
⊢ Measure.prod μ (dirac y) = map (fun x => (x, y)) μ
refine' prod_eq fun s t hs ht => _
no goals
α : Type u_1
α' : Type ?u.4489185
β : Type u_2
β' : Type ?u.4489191
γ : Type ?u.4489194
E : Type ?u.4489197
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
y : β
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ↑↑(map (fun x => (x, y)) μ) (s ×ˢ t) = ↑↑μ s * ↑↑(dirac y) t
simp_rw [map_apply measurable_prod_mk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
  dirac_apply' _ ht, ← indicator_mul_right _ fun _ => μ s, Pi.one_apply, mul_one]