α : Type u_2
α' : Type ?u.4495945
β : Type u_1
β' : Type ?u.4495951
γ : Type ?u.4495954
E : Type ?u.4495957
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν'✝ : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : SigmaFinite μ
ν' : Measure β
inst✝ : SigmaFinite ν'
s : Set α
t : Set β
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ ↑↑(Measure.prod μ ν + Measure.prod μ ν') (s ×ˢ t) = ↑↑μ s * ↑↑(ν + ν') t
α : Type u_2
α' : Type ?u.4495945
β : Type u_1
β' : Type ?u.4495951
γ : Type ?u.4495954
E : Type ?u.4495957
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν'✝ : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : SigmaFinite μ
ν' : Measure β
inst✝ : SigmaFinite ν'
⊢ Measure.prod μ (ν + ν') = Measure.prod μ ν + Measure.prod μ ν'
refine' prod_eq fun s t _ _ => _
no goals
α : Type u_2
α' : Type ?u.4495945
β : Type u_1
β' : Type ?u.4495951
γ : Type ?u.4495954
E : Type ?u.4495957
inst✝⁸ : MeasurableSpace α
inst✝⁷ : MeasurableSpace α'
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace β'
inst✝⁴ : MeasurableSpace γ
μ μ' : Measure α
ν ν'✝ : Measure β
τ : Measure γ
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : SigmaFinite μ
ν' : Measure β
inst✝ : SigmaFinite ν'
s : Set α
t : Set β
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ ↑↑(Measure.prod μ ν + Measure.prod μ ν') (s ×ˢ t) = ↑↑μ s * ↑↑(ν + ν') t
simp_rw [add_apply, prod_prod, left_distrib]