α : Type ?u.157549
β : Type ?u.157552
γ : Type ?u.157555
δ : Type ?u.157558
ι : Type ?u.157561
R : Type ?u.157564
R' : Type ?u.157567
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
⊢ inst✝ ≤ ⊤
α : Type ?u.157549
β : Type ?u.157552
γ : Type ?u.157555
δ : Type ?u.157558
ι : Type ?u.157561
R : Type ?u.157564
R' : Type ?u.157567
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
⊢ inst✝ ≤ OuterMeasure.caratheodory ⊤
rw [OuterMeasure.top_caratheodory]
no goals
α : Type ?u.157549
β : Type ?u.157552
γ : Type ?u.157555
δ : Type ?u.157558
ι : Type ?u.157561
R : Type ?u.157564
R' : Type ?u.157567
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
⊢ inst✝ ≤ ⊤
exact le_top
no goals
α : Type u_1
β : Type ?u.157552
γ : Type ?u.157555
δ : Type ?u.157558
ι : Type ?u.157561
R : Type ?u.157564
R' : Type ?u.157567
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ ↑↑⊤ s ≤ ↑↑(OuterMeasure.toMeasure ⊤ (_ : inst✝ ≤ OuterMeasure.caratheodory ⊤)) s
cases' s.eq_empty_or_nonempty with h h <;>
  simp [h, toMeasure_apply ⊤ _ hs, OuterMeasure.top_apply]