Theorem: Measure.prod_volume (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✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
⊢ Measure.prod volume volume = volume
Tactic:
sorry_proof
State after:
no goals