α : Type u_1
β : Type ?u.151657
γ : Type ?u.151660
δ : Type ?u.151663
ι : Type ?u.151666
R : Type ?u.151669
R' : Type ?u.151672
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
m : Set (Measure α)
h : μ ∈ m
this : sInf (toOuterMeasure '' m) ≤ ↑μ
s : Set α
hs : MeasurableSet s
⊢ ↑(sInf (toOuterMeasure '' m)) s ≤ ↑↑μ s
α : Type u_1
β : Type ?u.151657
γ : Type ?u.151660
δ : Type ?u.151663
ι : Type ?u.151666
R : Type ?u.151669
R' : Type ?u.151672
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
m : Set (Measure α)
h : μ ∈ m
this : sInf (toOuterMeasure '' m) ≤ ↑μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑(sInf m) s ≤ ↑↑μ s
rw [sInf_apply hs]
no goals
α : Type u_1
β : Type ?u.151657
γ : Type ?u.151660
δ : Type ?u.151663
ι : Type ?u.151666
R : Type ?u.151669
R' : Type ?u.151672
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
m : Set (Measure α)
h : μ ∈ m
this : sInf (toOuterMeasure '' m) ≤ ↑μ
s : Set α
hs : MeasurableSet s
⊢ ↑(sInf (toOuterMeasure '' m)) s ≤ ↑↑μ s
exact this s