no goals
α : Type u_1
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : t = ∅
⊢ ↑⊤ (t ∩ s) + ↑⊤ (t \ s) ≤ ↑⊤ t
simp [ht]
no goals
α : Type u_1
s : Set α
x✝ : MeasurableSet s
t : Set α
ht : Set.Nonempty t
⊢ ↑⊤ (t ∩ s) + ↑⊤ (t \ s) ≤ ↑⊤ t
simp only [ht, top_apply, le_top]