∀ (α : Type u_1) {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  (b : β), MeasureTheory.AEEqFun.const α b = MeasureTheory.AEEqFun.mk (fun x => b) ⋯