∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : TopologicalSpace β] [MeasurableSingletonClass α] {a : α}
  {f : α → β}, MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.dirac a)