no goals
α : Type u_1
β : Type ?u.88337
R : Type ?u.88340
R' : Type ?u.88343
ms : Set (OuterMeasure α)
m : OuterMeasure α
a : ℝ≥0∞
b : α
s : Set α
⊢ ↑(a • dirac b) s = indicator s (fun x => a) b
simp only [smul_apply, smul_eq_mul, dirac_apply, ← indicator_mul_right _ fun _ => a, mul_one]