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

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