Theorem: SciLean.Measure.prod_restrict (SciLean/Core/Integral/Common.lean)

State before:
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