α : Type u_1
β : Type ?u.3497107
γ : Type ?u.3497110
δ : Type ?u.3497113
ι : Type ?u.3497116
R : Type ?u.3497119
R' : Type ?u.3497122
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
⊢ ↑↑μ s ≤ ↑↑(OuterMeasure.toMeasure ↑μ (_ : m ≤ OuterMeasure.caratheodory ↑μ)) s
α : Type u_1
β : Type ?u.3497107
γ : Type ?u.3497110
δ : Type ?u.3497113
ι : Type ?u.3497116
R : Type ?u.3497119
R' : Type ?u.3497122
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
⊢ ↑↑μ s ≤ ↑↑(trim μ hm) s
simp_rw [Measure.trim]
no goals
α : Type u_1
β : Type ?u.3497107
γ : Type ?u.3497110
δ : Type ?u.3497113
ι : Type ?u.3497116
R : Type ?u.3497119
R' : Type ?u.3497122
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
⊢ ↑↑μ s ≤ ↑↑(OuterMeasure.toMeasure ↑μ (_ : m ≤ OuterMeasure.caratheodory ↑μ)) s
exact @le_toMeasure_apply _ m _ _ _