α : Type u_1
β : Type ?u.3499198
γ : Type ?u.3499201
δ : Type ?u.3499204
ι : Type ?u.3499207
R : Type ?u.3499210
R' : Type ?u.3499213
m m0 : MeasurableSpace α
μ✝ : Measure α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ↑↑(Measure.restrict (trim μ hm) s) t = ↑↑(trim (Measure.restrict μ s) hm) t
α : Type u_1
β : Type ?u.3499198
γ : Type ?u.3499201
δ : Type ?u.3499204
ι : Type ?u.3499207
R : Type ?u.3499210
R' : Type ?u.3499213
m m0 : MeasurableSpace α
μ✝ : Measure α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
⊢ Measure.restrict (trim μ hm) s = trim (Measure.restrict μ s) hm
refine @Measure.ext _ m _ _ (fun t ht => ?_)
no goals
α : Type u_1
β : Type ?u.3499198
γ : Type ?u.3499201
δ : Type ?u.3499204
ι : Type ?u.3499207
R : Type ?u.3499210
R' : Type ?u.3499213
m m0 : MeasurableSpace α
μ✝ : Measure α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ↑↑(Measure.restrict (trim μ hm) s) t = ↑↑(trim (Measure.restrict μ s) hm) t
rw [@Measure.restrict_apply α m _ _ _ ht, trim_measurableSet_eq hm ht,
  Measure.restrict_apply (hm t ht),
  trim_measurableSet_eq hm (@MeasurableSet.inter α m t s ht hs)]