Theorem: Measure.prod_restrict (test/integral/has_deriv_under_integral.lean)

State before:
R : Type
inst✝³ : RealScalar R
inst✝² : MeasureSpace R
t w : R
X : Type u_1
Y : Type u_2
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace Y
μ : Measure X
ν : Measure Y
A : Set X
B : Set Y
⊢ Measure.prod (μ.restrict A) (ν.restrict B) = (Measure.prod μ ν).restrict (A ×ˢ B)
Tactic:
sorry_proof
State after:
no goals