@[simp]

theorem MeasureTheory.Measure.dirac_real_apply' {α : Type u_1} [MeasurableSpace α] {s : Set α} (a : α) (hs : MeasurableSet s) : (dirac a).real s = s.indicator 1 a