Theorem: Measure.restrict_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
inst✝ : MeasurableSpace X
μ : Measure X
A B : Set X
⊢ (μ.restrict A).restrict B = μ.restrict (A ∩ B)
Tactic:
sorry_proof
State after:
no goals