no goals
α : Type u_1
β : Type ?u.99043
R : Type ?u.99046
R' : Type ?u.99049
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
s t : Set α
m : OuterMeasure α
⊢ ↑(↑(restrict s) m) t = ↑m (t ∩ s)
simp [restrict]