α : Type u_1
α' : Type ?u.4487971
β : Type u_2
β' : Type ?u.4487977
γ : Type ?u.4487980
E : Type ?u.4487983
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set α
t : Set β
s' : Set α
t' : Set β
hs' : MeasurableSet s'
ht' : MeasurableSet t'
⊢ ↑↑(restrict (Measure.prod μ ν) (s ×ˢ t)) (s' ×ˢ t') = ↑↑(restrict μ s) s' * ↑↑(restrict ν t) t'
α : Type u_1
α' : Type ?u.4487971
β : Type u_2
β' : Type ?u.4487977
γ : Type ?u.4487980
E : Type ?u.4487983
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set α
t : Set β
⊢ Measure.prod (restrict μ s) (restrict ν t) = restrict (Measure.prod μ ν) (s ×ˢ t)
refine' prod_eq fun s' t' hs' ht' => _
no goals
α : Type u_1
α' : Type ?u.4487971
β : Type u_2
β' : Type ?u.4487977
γ : Type ?u.4487980
E : Type ?u.4487983
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
s : Set α
t : Set β
s' : Set α
t' : Set β
hs' : MeasurableSet s'
ht' : MeasurableSet t'
⊢ ↑↑(restrict (Measure.prod μ ν) (s ×ˢ t)) (s' ×ˢ t') = ↑↑(restrict μ s) s' * ↑↑(restrict ν t) t'
rw [restrict_apply (hs'.prod ht'), prod_inter_prod, prod_prod, restrict_apply hs',
  restrict_apply ht']