α : Type u_3
α' : Type ?u.4493903
β : Type u_2
β' : Type ?u.4493909
γ : Type ?u.4493912
E : Type ?u.4493915
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MeasurableSpace α'
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace β'
inst✝⁵ : MeasurableSpace γ
μ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SigmaFinite ν✝
inst✝² : SigmaFinite μ
ι : Type u_1
inst✝¹ : Finite ι
ν : ι → Measure β
inst✝ : ∀ (i : ι), SigmaFinite (ν i)
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ↑↑(sum fun i => Measure.prod μ (ν i)) (s ×ˢ t) = ↑↑μ s * ↑↑(sum ν) t
α : Type u_3
α' : Type ?u.4493903
β : Type u_2
β' : Type ?u.4493909
γ : Type ?u.4493912
E : Type ?u.4493915
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MeasurableSpace α'
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace β'
inst✝⁵ : MeasurableSpace γ
μ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SigmaFinite ν✝
inst✝² : SigmaFinite μ
ι : Type u_1
inst✝¹ : Finite ι
ν : ι → Measure β
inst✝ : ∀ (i : ι), SigmaFinite (ν i)
⊢ Measure.prod μ (sum ν) = sum fun i => Measure.prod μ (ν i)
refine' prod_eq fun s t hs ht => _
no goals
α : Type u_3
α' : Type ?u.4493903
β : Type u_2
β' : Type ?u.4493909
γ : Type ?u.4493912
E : Type ?u.4493915
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MeasurableSpace α'
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace β'
inst✝⁵ : MeasurableSpace γ
μ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SigmaFinite ν✝
inst✝² : SigmaFinite μ
ι : Type u_1
inst✝¹ : Finite ι
ν : ι → Measure β
inst✝ : ∀ (i : ι), SigmaFinite (ν i)
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ↑↑(sum fun i => Measure.prod μ (ν i)) (s ×ˢ t) = ↑↑μ s * ↑↑(sum ν) t
simp_rw [sum_apply _ (hs.prod ht), sum_apply _ ht, prod_prod, ENNReal.tsum_mul_left]