no goals
α : Type u_1
β : Type ?u.276999
γ : Type ?u.277002
δ : Type ?u.277005
ι : Type ?u.277008
R : Type ?u.277011
R' : Type ?u.277014
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
h : MeasurableSet s
⊢ ↑(restrict μ s) = ↑(OuterMeasure.restrict s) ↑μ
simp_rw [restrict, restrictₗ, liftLinear, LinearMap.coe_mk, AddHom.coe_mk,
  toMeasure_toOuterMeasure, OuterMeasure.restrict_trim h, μ.trimmed]