α : Type u_2
α' : Type ?u.4494925
β : Type u_3
β' : Type ?u.4494931
γ : Type ?u.4494934
E : Type ?u.4494937
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) = ↑↑(sum μ) s * ↑↑ν t
α : Type u_2
α' : Type ?u.4494925
β : Type u_3
β' : Type ?u.4494931
γ : Type ?u.4494934
E : Type ?u.4494937
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_2
α' : Type ?u.4494925
β : Type u_3
β' : Type ?u.4494931
γ : Type ?u.4494934
E : Type ?u.4494937
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) = ↑↑(sum μ) s * ↑↑ν t
simp_rw [sum_apply _ (hs.prod ht), sum_apply _ hs, prod_prod, ENNReal.tsum_mul_right]