α : Type u_1
α' : Type ?u.4497375
β : Type u_2
β' : Type ?u.4497381
γ : Type ?u.4497384
E : Type ?u.4497387
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_1
α' : Type ?u.4497375
β : Type u_2
β' : Type ?u.4497381
γ : Type ?u.4497384
E : Type ?u.4497387
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_1
α' : Type ?u.4497375
β : Type u_2
β' : Type ?u.4497381
γ : Type ?u.4497384
E : Type ?u.4497387
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, right_distrib]