{α : Type u_1} →
  {m0 : MeasurableSpace α} →
    [inst : TopologicalSpace α] →
      {μ : MeasureTheory.Measure α} →
        {motive : MeasureTheory.IsLocallyFiniteMeasure μ → Sort u} →
          (t : MeasureTheory.IsLocallyFiniteMeasure μ) →
            ((finiteAtNhds : ∀ (x : α), μ.FiniteAtFilter (nhds x)) → motive ⋯) → motive t