no goals
α : Type u_1
β : Type ?u.124154
R : Type ?u.124157
R' : Type ?u.124160
ms : Set (OuterMeasure α)
m : OuterMeasure α
s : Set α
h : Set.Nonempty s
a : α
as : a ∈ s
⊢ ⊤ ≤ ↑(⊤ • dirac a) s
simp [smul_dirac_apply, as]